Reasoning about Strategies: on the Satisfiability Problem

Journal article

Strategy Logic (SL, for short) has been introduced by Mogavero, Murano, and Vardi as a useful formalism for reasoning explicitly about strategies, as first-order objects, in multi-agent concurrent games. This logic turns out to be very powerful, subsuming all major previously studied modal logics for strategic reasoning, including ATL, ATL⋆ , and the like. Unfortunately, due to its high expressiveness, SL has a non-elementarily decidable model-checking problem and the satisfiability question is undecidable, specifically Σ 1 1-hard.
In order to obtain a decidable sublogic, we introduce and study here One-Goal Strategy Logic (SL[1g], for short). This is a syntactic fragment of SL, strictly subsuming ATL⋆ , which encompasses formulas in prenex normal form having a single temporal goal at a time, for every strategy quantification of agents. We prove that, unlike SL, SL[1g] has the bounded tree-model property and its satisfiability problem is decidable in 2ExpTime, thus not harder than the one for ATL.

Authors: Mogavero, F; Murano, A; Perelli, G; Vardi, M

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: IFCoLog: International Federation of Computational Logic
• Journal: Logical Methods in Computer Science
• Volume: 13
• Issue: 1
• Pages: 1-9
• Publication date: 2017-03-17
• Acceptance date: 2016-01-01
• ISSN: 1860-5974
• Keywords: Multi-Agent Games; Bounded Tree-Model Property; Strategic Reasonings; Satisfiability problem; Strategy Logic; Alternating-Time Temporal Logic