Reasoning about Strategies: on the Satisfiability Problem
| Autor: | Fabio Mogavero, Aniello Murano, Giuseppe Perelli, Moshe Y. Vardi |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: | |
| Zdroj: | Logical Methods in Computer Science, Vol Volume 13, Issue 1 (2017) |
| Druh dokumentu: | article |
| ISSN: | 1860-5974 48139955 |
| DOI: | 10.23638/LMCS-13(1:9)2017 |
| Popis: | 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*. |
| Databáze: | Directory of Open Access Journals |
| Externí odkaz: |
|