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*
What Makes Atl* Decidable? A Decidable Fragment of Strategy Logic / Mogavero, Fabio; Murano, Aniello; Perelli, Giuseppe; M. Y., Vardi. - 7454:(2012), pp. 193-208. (Intervento presentato al convegno CONCUR 2012 tenutosi a Newcastle upon Tyne, UK nel September 4-7, 2012.) [10.1007/978-3-642-32940-1_15].
What Makes Atl* Decidable? A Decidable Fragment of Strategy Logic
MOGAVERO, FABIO;MURANO, ANIELLO;PERELLI, GIUSEPPE;
2012
Abstract
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*File | Dimensione | Formato | |
---|---|---|---|
concur12.pdf
solo utenti autorizzati
Tipologia:
Documento in Post-print
Licenza:
Accesso privato/ristretto
Dimensione
370.99 kB
Formato
Adobe PDF
|
370.99 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.