2019
[GBM19] Patrick Gardy, Patricia Bouyer, and Nicolas Markey. Dependences in Strategy Logic. Transactions on Computing Systems. Springer-Verlag, 2019.
Abstract

Strategy Logic (SL) is a very expressive temporal logic for specifying and verifying properties of multi-agent systems: in SL, one can quantify over strategies, assign them to agents, and express LTL properties of the resulting plays. Such a powerful framework has two drawbacks: first, model checking SL has non-elementary complexity; second, the exact semantics of SL is rather intricate, and may not correspond to what is expected. In this paper, we focus on strategy dependences in SL, by tracking how existentially-quantified strategies in a formula may (or may not) depend on other strategies selected in the formula, revisiting the approach of [Mogavero et al., Reasoning about strategies: On the model-checking problem, 2014]. We explain why elementary dependences, as defined by Mogavero et al., do not exactly capture the intended concept of behavioral strategies. We address this discrepancy by introducing timeline dependences, and exhibit a large fragment of SL for which model checking can be performed in 2EXPTIME under this new semantics.

@article{tocsys2019-GBM,
  author =              {Gardy, Patrick and Bouyer, Patricia and Markey,
                         Nicolas},
  title =               {Dependences in Strategy Logic},
  publisher =           {Springer-Verlag},
  journal =             {Transactions on Computing Systems},
  year =                {2019},
  doi =                 {10.1007/s00224-019-09926-y},
  abstract =            {Strategy Logic~(\textsf{SL}) is a very expressive
                         temporal logic for specifying and verifying
                         properties of multi-agent systems: in~\textsf{SL},
                         one can quantify over strategies, assign them to
                         agents, and express \textsf{LTL} properties of the
                         resulting plays. Such a powerful framework has two
                         drawbacks: first, model checking \textsf{SL} has
                         non-elementary complexity; second, the exact
                         semantics of \textsf{SL} is rather intricate, and
                         may not correspond to what is expected. In~this
                         paper, we~focus on \emph{strategy dependences}
                         in~\textsf{SL}, by tracking how
                         existentially-quantified strategies in a formula may
                         (or~may~not) depend on other strategies selected in
                         the formula, revisiting the approach of~[Mogavero
                         \emph{et~al.}, Reasoning about strategies: On~the
                         model-checking problem,~2014]. We~explain why
                         \emph{elementary} dependences, as defined by
                         Mogavero~\emph{et~al.}, do not exactly capture the
                         intended concept of behavioral strategies.
                         We~address this discrepancy by introducing
                         \emph{timeline} dependences, and exhibit a large
                         fragment of \textsf{SL} for which model checking can
                         be performed in \textsf{2EXPTIME} under this new
                         semantics.},
}
[BKM+19] Patricia Bouyer, Orna Kupferman, Nicolas Markey, Bastien Maubert, Aniello Murano, and Giuseppe Perelli. Reasoning about Quality and Fuzziness of Strategic Behaviours. In IJCAI'19. IJCAI organization, August 2019.
@inproceedings{ijcai2019-BKMMMP,
  author =              {Bouyer, Patricia and Kupferman, Orna and Markey,
                         Nicolas and Maubert, Bastien and Murano, Aniello and
                         Perelli, Giuseppe},
  title =               {Reasoning about Quality and Fuzziness of Strategic
                         Behaviours},
  editor =              {Kraus, Sarit},
  booktitle =           {{P}roceedings of the 28th {I}nternational {J}oint
                         {C}onference on {A}rtificial {I}ntelligence
                         ({IJCAI}'19)},
  acronym =             {{IJCAI}'19},
  publisher =           {IJCAI organization},
  year =                {2019},
  month =               aug,
}
[RSM19] Victor Roussanaly, Ocan Sankur, and Nicolas Markey. Abstraction Refinement Algorithms for Timed Automata. In CAV'19, Lecture Notes in Computer Science. Springer-Verlag, July 2019.
@inproceedings{cav2019-RSM,
  author =              {Roussanaly, Victor and Sankur, Ocan and Markey,
                         Nicolas},
  title =               {Abstraction Refinement Algorithms for Timed
                         Automata},
  editor =              {Dillig, I{\c s}il and Ta{\c s}iran, Serdar},
  booktitle =           {{P}roceedings of the 31st {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'19)},
  acronym =             {{CAV}'19},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  year =                {2019},
  month =               jul,
}