Strategy Logic with Simple Goals: Tractable Reasoning About Strategies

Francesco Belardinelli, Wojciech Jamroga, Damian Kurpiewski, Vadim Malvone, Aniello Murano

IJCAI 2019 pp. 88-94

doi:10.24963/IJCAI.2019/13 /ijcai/2019/belardinelli2019ijcai-strategy/

Abstract

In this paper we introduce Strategy Logic with simple goals (SL[SG]), a fragment of Strategy Logic that strictly extends the well-known Alternating-time Temporal Logic ATL by introducing arbitrary quantification over the agents' strategies. Our motivation comes from game-theoretic applications, such as expressing Stackelberg equilibria in games, coercion in voting protocols, as well as module checking for simple goals. Most importantly, we prove that the model checking problem for SL[SG] is PTIME-complete, the same as ATL. Thus, the extra expressive power comes at no computational cost as far as verification is concerned.

PDF IJCAI Semantic Scholar

Cite

Text

Belardinelli et al. "Strategy Logic with Simple Goals: Tractable Reasoning About Strategies." International Joint Conference on Artificial Intelligence, 2019. doi:10.24963/IJCAI.2019/13

Markdown

[Belardinelli et al. "Strategy Logic with Simple Goals: Tractable Reasoning About Strategies." International Joint Conference on Artificial Intelligence, 2019.](https://mlanthology.org/ijcai/2019/belardinelli2019ijcai-strategy/) doi:10.24963/IJCAI.2019/13

BibTeX

@inproceedings{belardinelli2019ijcai-strategy,
  title     = {{Strategy Logic with Simple Goals: Tractable Reasoning About Strategies}},
  author    = {Belardinelli, Francesco and Jamroga, Wojciech and Kurpiewski, Damian and Malvone, Vadim and Murano, Aniello},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2019},
  pages     = {88-94},
  doi       = {10.24963/IJCAI.2019/13},
  url       = {https://mlanthology.org/ijcai/2019/belardinelli2019ijcai-strategy/}
}