Uniform Solving for omega-regular Games

We show that fixpoint equation systems over arbitrary finite lattices can be solved with a number of iterations that is quasipolynomial in the lattice height and the alternation-depth of the system. As a side-result, we obtain a highly generic progress measure algorithm that solves fixpoint equation systems over finite lattices and uses universal trees to measure progress. Since the winning regions of various kinds of finite-history omega-regular games can be specified by fixpoint equations, our algorithm instantiates to solving e. g. standard parity games, energy parity games, mean-payoff parity games and stochastic parity games (both qualitative and quantitative). The runtime complexities of the instances of the algorithm typically are quasipolynomial in the number of nodes, the number of priorities, and the maximal size of histories of winning strategies. This work is based on the paper “Quasipolynomial Computation of Nested Fixpoints”, which has been published as joint work with Lutz Schröder at TACAS 2021 (extended version available at https: //arxiv. org/pdf/1907. 07020. pdf).

Authors

• Daniel Hausmann

Keywords

No keywords are indexed for this paper.