Nicolas Markey

Résumé

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.

@inproceedings{stacs2018-GBM,
  author =              {Gardy, Patrick and Bouyer, Patricia and Markey,
                         Nicolas},
  title =               {Dependences in Strategy Logic},
  editor =              {Niedermeier, Rolf and Vall{\'e}e, Brigitte},
  booktitle =           {{P}roceedings of the 35th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'18)},
  acronym =             {{STACS}'18},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {96},
  pages =               {34:1-34:14},
  year =                {2018},
  month =               feb,
  doi =                 {10.4230/LIPIcs.STACS.2018.34},
  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.},
}