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

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