Show simple item record

dc.contributor.authorMogavero, Fabio
Murano, Aniello
Perelli, Giuseppe
Vardi, Moshe Y.
dc.date.accessioned 2017-03-28T21:32:36Z
dc.date.available 2017-03-28T21:32:36Z
dc.date.issued 2017
dc.identifier.citation Mogavero, Fabio, Murano, Aniello, Perelli, Giuseppe, et al.. "Reasoning about Strategies: on the Satisfiability Problem." Logical Methods in Computer Science, 13, no. 1 (2017) Episciences: http://dx.doi.org/10.23638/LMCS-13(1:9)2017.
dc.identifier.urihttps://hdl.handle.net/1911/94043
dc.description.abstract 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*.
dc.language.iso eng
dc.publisher Episciences
dc.rights This work is licensed under the Creative Commons Attribution-NoDerivs License.
dc.rights.urihttps://creativecommons.org/licenses/by-nd/2.0/
dc.title Reasoning about Strategies: on the Satisfiability Problem
dc.type Journal article
dc.citation.journalTitle Logical Methods in Computer Science
dc.citation.volumeNumber 13
dc.citation.issueNumber 1
dc.type.dcmi Text
dc.identifier.doihttp://dx.doi.org/10.23638/LMCS-13(1:9)2017
dc.type.publication publisher version


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record