2026-07-25T12:24:46Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17261 2024-03-06T10:59:21Z ddc:004 open_access

Taming Strategy Logic: Non-Recurrent Fragments Benerecetti, Massimo Mogavero, Fabio Peron, Adriano Strategic Reasoning Multi-Agent Systems Temporal Logics Satisfiability Strategy Logic (SL for short) is one of the prominent languages for reasoning about the strategic abilities of agents in a multi-agent setting. This logic extends LTL with first-order quantifiers over the agent strategies and encompasses other formalisms, such as ATL* and CTL*. The model-checking problem for SL and several of its fragments have been extensively studied. On the other hand, the picture is much less clear on the satisfiability front, where the problem is undecidable for the full logic. In this work, we study two fragments of One-Goal SL, where the nesting of sentences within temporal operators is constrained. We show that the satisfiability problem for these logics, and for the corresponding fragments of ATL* and CTL*, is ExpSpace and PSpace-Complete, respectively. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Massimo Benerecetti and Fabio Mogavero and Adriano Peron 2022 Is Part Of LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TIME.2022.14 urn:nbn:de:0030-drops-172611 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.14 eng https://creativecommons.org/licenses/by/4.0/legalcode