License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2022.21
URN: urn:nbn:de:0030-drops-170841
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/17084/
Go to the corresponding LIPIcs Volume Portal

Filiot, Emmanuel ; Hamel-de le Court, Edwin

Two-Player Boundedness Counter Games

pdf-format:
LIPIcs-CONCUR-2022-21.pdf (0.9 MB)

Abstract

We consider two-player zero-sum games with winning objectives beyond regular languages, expressed as a parity condition in conjunction with a Boolean combination of boundedness conditions on a finite set of counters which can be incremented, reset to 0, but not tested. A boundedness condition requires that a given counter is bounded along the play. Such games are decidable, though with non-optimal complexity, by an encoding into the logic WMSO with the unbounded and path quantifiers, which is known to be decidable over infinite trees. Our objective is to give tight or tighter complexity results for particular classes of counter games with boundedness conditions, and study their strategy complexity. In particular, counter games with conjunction of boundedness conditions are easily seen to be equivalent to Streett games, so, they are CoNP-c. Moreover, finite-memory strategies suffice for Eve and memoryless strategies suffice for Adam. For counter games with a disjunction of boundedness conditions, we prove that they are in solvable in NP∩CoNP, and in PTime if the parity condition is fixed. In that case memoryless strategies suffice for Eve while infinite memory strategies might be necessary for Adam. Finally, we consider an extension of those games with a max operation. In that case, the complexity increases: for conjunctions of boundedness conditions, counter games are EXPTIME-c.

BibTeX - Entry

@InProceedings{filiot_et_al:LIPIcs.CONCUR.2022.21,
  author =	{Filiot, Emmanuel and Hamel-de le Court, Edwin},
  title =	{{Two-Player Boundedness Counter Games}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{21:1--21:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/17084},
  URN =		{urn:nbn:de:0030-drops-170841},
  doi =		{10.4230/LIPIcs.CONCUR.2022.21},
  annote =	{Keywords: Controller synthesis, Game theory, Counter Games, Boundedness objectives}
}

Keywords: Controller synthesis, Game theory, Counter Games, Boundedness objectives
Collection: 33rd International Conference on Concurrency Theory (CONCUR 2022)
Issue Date: 2022
Date of publication: 06.09.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI