Solving Odd-Fair Parity Games

TL;DR

This paper introduces a new Zielonka-type algorithm for efficiently solving Odd-fair parity games, which incorporate fairness constraints relevant to cyber-physical system planning, and formalizes winning strategies for the Odd player.

Contribution

It presents a novel algorithm for Odd-fair parity games with the same complexity as Zielonka's, and formalizes the Odd player's winning strategies under fairness constraints.

Findings

The algorithm matches Zielonka's worst-case time complexity.

It preserves Zielonka's advantage over other exponential-time solvers.

Formalization of Odd player strategies enhances understanding of fairness in two-player games.

Abstract

This paper discusses the problem of efficiently solving parity games where player Odd has to obey an additional 'strong transition fairness constraint' on its vertices -- given that a player Odd vertex $v$ is visited infinitely often, a particular subset of the outgoing edges (called live edges) of $v$ has to be taken infinitely often. Such games, which we call 'Odd-fair parity games', naturally arise from abstractions of cyber-physical systems for planning and control. In this paper, we present a new Zielonka-type algorithm for solving Odd-fair parity games. This algorithm not only shares 'the same worst-case time complexity' as Zielonka's algorithm for (normal) parity games but also preserves the algorithmic advantage Zielonka's algorithm possesses over other parity solvers with exponential time complexity. We additionally introduce a formalization of Odd player winning strategies in such games, which were unexplored previous to this work. This formalization serves dual purposes: firstly, it enables us to prove our Zielonka-type algorithm; secondly, it stands as a noteworthy contribution in its own right, augmenting our understanding of additional fairness assumptions in two-player games.