2026-07-21T03:13:39Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2858 2024-03-06T10:33:37Z ddc:004 open_access

ATL with Strategy Contexts: Expressiveness and Model Checking Da Costa, Arnaud Laroussinie, François Markey, Nicolas alternating temporal logic agent strategy quantifier We study the alternating-time temporal logics ATL and ATL* extended with strategy contexts: these make agents commit to their strategies during the evaluation of formulas, contrary to plain ATL and ATL* where strategy quantifiers reset previously selected strategies. We illustrate the important expressive power of strategy contexts by proving that they make the extended logics, namely ATLsc and ATLsc*, equally expressive: any formula in ATLsc* can be translated into an equivalent, linear-size ATLsc formula. Despite the high expressiveness of these logics, we~prove that their model-checking problems remain decidable by~designing a tree-automata-based algorithm for model-checking ATLsc* on the full class of $n$-player concurrent game structures. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Arnaud Da Costa and François Laroussinie and Nicolas Markey 2010 Is Part Of LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2010.120 urn:nbn:de:0030-drops-28589 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.120 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode