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.
翻译:本文讨论了高效求解一类奇偶博弈的问题,其中奇玩家必须遵循其顶点上的附加“强转移公平性约束”——给定一个奇玩家顶点v被无限频繁访问时,v的特定出边子集(称为活跃边)也需被无限频繁选取。此类博弈被称为“奇公平奇偶博弈”,源于信息物理系统在规划与控制中的抽象建模。本文提出了一种新的Zielonka型算法用于求解奇公平奇偶博弈。该算法不仅与(普通)奇偶博弈的Zielonka算法具有“相同的最坏时间复杂度”,还保留了Zielonka算法相较于其他指数时间复杂度的奇偶求解器所拥有的算法优势。此外,本文首次提出了此类博弈中奇玩家获胜策略的形式化描述——这一领域此前未有探索。该形式化具有双重作用:首先,它支撑了对我们提出的Zielonka型算法的证明;其次,它本身作为一项重要贡献,深化了对双人博弈中额外公平性假设的理解。