Polynomial-Time Under-Approximation of Winning Regions in Parity Games

We propose a pattern for designing algorithms that run in polynomial time by construction and underapproximate the winning regions of both players in parity games. This approximation is achieved by the interaction of finitely many aspects governed by a common ranking function, where the choice of aspects and ranking function instantiates the design pattern. Each aspect attempts to improve the under-approximation of winning regions or decrease the rank function by simplifying the structure of the parity game. Our design pattern is incremental as aspects may operate on the residual game of yet undecided nodes. We present several aspects and one higher-order transformation of our algorithms — based on efficient, static analyses — and illustrate the benefit of their interaction as well as their relative precision within pattern instantiations. Instantiations of our design pattern can be applied for local model checking and as pre-processors for algorithms whose worst-case running time is exponential