A Parity Game Tale of Two Counters

TL;DR

This paper introduces the Two Counters parity game, establishing exponential lower bounds for several algorithms, thereby advancing understanding of the computational complexity involved in solving parity games.

Contribution

It presents the first exponential lower bounds for priority promotion with delayed promotion and tangle learning algorithms in parity game solving.

Findings

Provides exponential lower bounds for attractor-based algorithms.

First to establish such bounds for priority promotion with delayed promotion.

First to establish such bounds for tangle learning.

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.