A Parity Game Tale of Two Counters

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

54 Downloads (Pure)

Abstract

Parity games are simple infinite games played on finite graphs with a winning condition that is expressive enough to capture nested least and greatest fixpoints. Through their tight relationship to the modal mu-calculus, they are used in practice for the model-checking and synthesis problems of the mu-calculus and related temporal logics like LTL and CTL. Solving parity games is a compelling complexity theoretic problem, as the problem lies in the intersection of UP and co-UP and is believed to admit a polynomial-time solution, motivating researchers to either find such a solution or to find superpolynomial lower bounds for existing algorithms to improve the understanding of parity games. We present a parameterized parity game called the Two Counters game, which provides an exponential lower bound for a wide range of attractor-based parity game solving algorithms. We are the first to provide an exponential lower bound to priority promotion with the delayed promotion policy, and the first to provide such a lower bound to tangle learning.
Original languageEnglish
Title of host publicationProceedings Tenth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2019
Subtitle of host publicationBordeaux, France, 2-3rd September 2019
EditorsJérôme Leroux, Jean-François Raskin
PublisherArXiv
Pages107-122
Number of pages16
DOIs
Publication statusPublished - 2019
Event10th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2019 - Bordeaux, France
Duration: 2 Sep 20193 Sep 2019
Conference number: 10

Publication series

NameElectronic Proceedings in Theoretical Computer Science (EPTCS)
PublisherarXiv
Volume305
ISSN (Electronic)2075-2180

Conference

Conference10th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2019
Abbreviated titleGandALF
CountryFrance
CityBordeaux
Period2/09/193/09/19

Fingerprint Dive into the research topics of 'A Parity Game Tale of Two Counters'. Together they form a unique fingerprint.

Cite this