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 2

ExpTime-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 2

ExpTime-complete

, as it is for

Atl

*.