LIPIcs.FSTTCS.2023.34.pdf
- Filesize: 1.46 MB
- 24 pages
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.
Feedback for Dagstuhl Publishing