Fair Omega-regular Games

Abstract

We consider two-player games over finite graphs in which both players are restricted by fairness constraints on their moves. Given a two player game graph G=(V,E) and a set of fair moves E_f a subset of E a player is said to play fair in G if they choose an edge e in E_f infinitely often whenever the source vertex of e is visited infinitely often. Otherwise, they play unfair. We equip such games with two omega-regular winning conditions alpha and beta deciding the winner of mutually fair and mutually unfair plays, respectively. Whenever one player plays fair and the other plays unfair, the fairly playing player wins the game. The resulting games are called fair alpha/beta games. We formalize fair alpha/beta games and show that they are determined. For fair parity/parity games, i.e., fair alpha/beta games where alpha and beta are given each by a parity condition over G, we provide a polynomial reduction to (normal) parity games via a gadget construction inspired by the reduction of stochastic parity games to parity games. We further give a direct symbolic fixpoint algorithm to solve fair parity/parity games. On a conceptual level, we illustrate the translation between the gadget-based reduction and the direct symbolic algorithm which uncovers the underlying similarities of solution algorithms for fair and stochastic parity games, as well as for the recently considered class of fair games in which only one player is restricted by fair moves.