2026-07-23T00:23:02Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5653 2024-03-06T10:36:42Z ddc:004 open_access

Weighted Strategy Logic with Boolean Goals Over One-Counter Games Bouyer, Patricia Gardy, Patrick Markey, Nicolas Temporal logics multi-player games strategy logic quantitative games Strategy Logic is a powerful specification language for expressing non-zero-sum properties of multi-player games. SL conveniently extends the logic ATL with explicit quantification and assignment of strategies. In this paper, we consider games over one-counter automata, and a quantitative extension 1cSL of SL with assertions over the value of the counter. We prove two results: we first show that, if decidable, model checking the so-called Boolean-goal fragment of 1cSL has non-elementary complexity; we actually prove the result for the Boolean-goal fragment of SL over finite-state games, which was an open question in [Mogavero et al. Reasoning about strategies: On the model-checking problem. ACM ToCL 15(4),2014]. As a first step towards proving decidability, we then show that the Boolean-goal fragment of 1cSL over one-counter games enjoys a nice periodicity property. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Patricia Bouyer and Patrick Gardy and Nicolas Markey 2015 Is Part Of LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2015.69 urn:nbn:de:0030-drops-56537 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.69 eng https://creativecommons.org/licenses/by/3.0/legalcode