Strategy Logic with Simple Goals: Tractable Reasoning about Strategies
Strategy Logic with Simple Goals: Tractable Reasoning about Strategies
Francesco Belardinelli, Wojciech Jamroga, Damian Kurpiewski, Vadim Malvone, Aniello Murano
Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence
Main track. Pages 88-94.
https://doi.org/10.24963/ijcai.2019/13
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.
Keywords:
Agent-based and Multi-agent Systems: Agent Theories and Models
Agent-based and Multi-agent Systems: Formal Verification, Validation and Synthesis