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