Simulation Relations for Alternating Parity Automata and Parity Games

摘要

We adapt the notion of delayed simulation to alternating parity automata and parity games. On the positive side, we show that (ⅰ) the corresponding simulation relation can be computed in polynomial time and (ⅱ) delayed simulation implies language inclusion. On the negative side, we point out that quotienting with respect to delayed simulation does not preserve the language recognized, which means that delayed simulation cannot be used for state-space reduction via merging of simulation equivalent states. As a remedy, we introduce finer, so-called biased notions of delayed simulation where we show quotienting does preserve the language recognized. We propose a heuristic for reducing the size of alternating parity automata and parity games and, as an evidence for its usefulness, demonstrate that it is successful when applied to the Jurdzinski family of parity games.