Solving 3-Color Parity Games in $ O(n^2) $ Time

TL;DR

This paper introduces a new polynomial-time algorithm for solving 3-color parity games, significantly improving efficiency and matching the best known times for simpler cases like B"uchi games, thus broadening practical applicability.

Contribution

The paper presents a novel $O(n^2)$ algorithm for 3-color parity games, improving over previous methods and demonstrating their computational tractability.

Findings

New $O(n^2)$ algorithm for 3-color parity games

Matches the best known times for B"uchi games

Shows 3-color parity games are not harder to solve than simpler cases

Abstract

Parity games are an expressive framework to consider realizability questions for omega-regular languages. However, it is open whether they can be solved in polynomial time, making them unamenable for practical usage. To overcome this restriction, we consider 3-color parity games, which can be solved in polynomial time. They still cover an expressive fragment of specifications, as they include the classical B\"uchi and co-B\"uchi winning conditions as well as their union and intersection. This already suffices to express many useful combinations of safety and liveness properties, as for example the family of GR(1). The best known algorithm for 3-color parity games solves a game with n vertices in $ O(n^{2}\sqrt{n}) $ time. We improve on this result by presenting a new algorithm, based on simple attractor constructions, which only needs time $ O(n^2) $. As a result, we match the best known running times for solving (co)-B\"uchi games, showing that 3-color parity games are not harder to solve in general.