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
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.
\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,
}