Fabio Mogavero ; Aniello Murano ; Giuseppe Perelli ; Moshe Y. Vardi - Reasoning about Strategies: on the Satisfiability Problem

lmcs:3204 - Logical Methods in Computer Science, March 17, 2017, Volume 13, Issue 1 - https://doi.org/10.23638/LMCS-13(1:9)2017
Reasoning about Strategies: on the Satisfiability Problem

Authors: Fabio Mogavero ; Aniello Murano ; Giuseppe Perelli ; Moshe Y. Vardi

    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*.

    Volume: Volume 13, Issue 1
    Published on: March 17, 2017
    Accepted on: March 17, 2017
    Submitted on: March 17, 2017
    Keywords: Computer Science - Logic in Computer Science,F.3.1,F.4.1

    Linked publications - datasets - softwares

    Source : ScholeXplorer IsReferencedBy ARXIV 1708.05849
    Source : ScholeXplorer IsReferencedBy DOI 10.1007/s00224-019-09926-y
    Source : ScholeXplorer IsReferencedBy DOI 10.4230/lipics.stacs.2018.34
    Source : ScholeXplorer IsReferencedBy DOI 10.48550/arxiv.1708.05849
    • 10.4230/lipics.stacs.2018.34
    • 10.1007/s00224-019-09926-y
    • 10.1007/s00224-019-09926-y
    • 10.1007/s00224-019-09926-y
    • 1708.05849
    • 10.48550/arxiv.1708.05849
    Dependences in Strategy Logic
    Gardy, Patrick ; Bouyer, Patricia ; Markey, Nicolas ;

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1177 times.
    This article's PDF has been downloaded 422 times.