A Decidable Fragment of Strategy Logic
Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y. Vardi

TL;DR
This paper introduces SL[1G], a syntactic fragment of Strategy Logic, which is more expressive than ATL* and has a decidable satisfiability problem, unlike the full logic.
Contribution
The paper defines SL[1G], a new fragment of Strategy Logic with a decidable satisfiability problem and bounded tree-model property, extending the applicability of strategic reasoning.
Findings
SL[1G] has an elementarily decidable model-checking problem.
SL[1G] satisfiability is decidable in 2ExpTime.
SL[1G] strictly subsumes ATL*.
Abstract
Strategy Logic (SL, for short) has been recently 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 to be very powerful, subsuming all major previously studied modal logics for strategic reasoning, including ATL, ATL*, and the like. Unfortunately, due to its expressiveness, SL has a non-elementarily decidable model-checking problem and a highly undecidable satisfiability problem, specifically, -Hard. In order to obtain a decidable sublogic, we introduce and study here One-Goal Strategy Logic (SL[1G], for short). This logic 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. SL[1G] is known to have an…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, Reasoning, and Knowledge · Logic, programming, and type systems
