| Summary: | 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 Sigma_1^1.
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*.
|
|---|