Reasoning about Strategies: on the Satisfiability Problem
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 fo...
| Main Authors: | , , , |
|---|---|
| Format: | Journal article |
| Published: |
IFCoLog: International Federation of Computational Logic
2017
|
| _version_ | 1797072058097598464 |
|---|---|
| author | Mogavero, F Murano, A Perelli, G Vardi, M |
| author_facet | Mogavero, F Murano, A Perelli, G Vardi, M |
| author_sort | Mogavero, F |
| collection | OXFORD |
| description | 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 Σ 1 1-hard. <br/>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. |
| first_indexed | 2024-03-06T23:02:08Z |
| format | Journal article |
| id | oxford-uuid:62817f3b-756b-42d6-9ae1-6616221cd77b |
| institution | University of Oxford |
| last_indexed | 2024-03-06T23:02:08Z |
| publishDate | 2017 |
| publisher | IFCoLog: International Federation of Computational Logic |
| record_format | dspace |
| spelling | oxford-uuid:62817f3b-756b-42d6-9ae1-6616221cd77b2022-03-26T18:06:39ZReasoning about Strategies: on the Satisfiability ProblemJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:62817f3b-756b-42d6-9ae1-6616221cd77bSymplectic Elements at OxfordIFCoLog: International Federation of Computational Logic2017Mogavero, FMurano, APerelli, GVardi, MStrategy 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 Σ 1 1-hard. <br/>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. |
| spellingShingle | Mogavero, F Murano, A Perelli, G Vardi, M Reasoning about Strategies: on the Satisfiability Problem |
| title | Reasoning about Strategies: on the Satisfiability Problem |
| title_full | Reasoning about Strategies: on the Satisfiability Problem |
| title_fullStr | Reasoning about Strategies: on the Satisfiability Problem |
| title_full_unstemmed | Reasoning about Strategies: on the Satisfiability Problem |
| title_short | Reasoning about Strategies: on the Satisfiability Problem |
| title_sort | reasoning about strategies on the satisfiability problem |
| work_keys_str_mv | AT mogaverof reasoningaboutstrategiesonthesatisfiabilityproblem AT muranoa reasoningaboutstrategiesonthesatisfiabilityproblem AT perellig reasoningaboutstrategiesonthesatisfiabilityproblem AT vardim reasoningaboutstrategiesonthesatisfiabilityproblem |