What makes ATL* decidable? A decidable fragment of strategy logic

Strategy Logic (SL, for short) has been recently introduced by Mogavero, Murano, and Vardi as a formalism for reasoning explicitly about strategies, as first-order objects, in multi-agent concurrent games. This logic turns out to be very powerful, strictly subsuming all major previously studied modal logics for strategic reasoning, including ATL, ATL*, and the like. The price that one has to pay for the expressiveness of SL is the lack of important model-theoretic properties and an increased complexity of decision problems. In particular, SL does not have the bounded-tree model property and the related satisfiability problem is highly undecidable while for ATL* it is 2ExpTime-complete. An obvious question that arises is then what makes ATL* decidable. Understanding this should enable us to identify decidable fragments of SL. We focus, in this work, on the limitation of ATL* to allow only one temporal goal for each strategic assertion and study the fragment of SL with the same restriction. Specifically, we introduce and study the syntactic fragment One-Goal Strategy Logic (SL[1g], for short), which consists of formulas in prenex normal form having a single temporal goal at a time for every strategy quantification of agents. We show that SL[1g] is strictly more expressive than ATL*. Our main result is that SL[1g] has the bounded tree-model property and its satisfiability problem is 2ExpTime-complete, as it is for ATL*. © 2012 Springer-Verlag