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 S L 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 un-decidable 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.
展开▼
