Weighted Strategy Logic with Boolean Goals Over One-Counter Games

Bouyer, Patricia; Gardy, Patrick; Markey, Nicolas

doi:10.4230/LIPIcs.FSTTCS.2015.69

Document

Weighted Strategy Logic with Boolean Goals Over One-Counter Games

Authors Patricia Bouyer, Patrick Gardy, Nicolas Markey

Part of: Volume: 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)
License: Creative Commons Attribution 3.0 Unported license
Publication Date: 2015-12-14

PDF

File

PDF

LIPIcs.FSTTCS.2015.69.pdf

Filesize: 0.6 MB
15 pages

Document Identifiers

DOI: 10.4230/LIPIcs.FSTTCS.2015.69
URN: urn:nbn:de:0030-drops-56537

Subject Classification

Keywords

Temporal logics
multi-player games
strategy logic
quantitative games

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

Abstract

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.

Cite As Get BibTex

Patricia Bouyer, Patrick Gardy, and Nicolas Markey. Weighted Strategy Logic with Boolean Goals Over One-Counter Games. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 69-83, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.FSTTCS.2015.69

Author Details

Patricia Bouyer

Patrick Gardy

Nicolas Markey

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail