Simulation Relations for Alternating Parity Automata and Parity Games

Carsten Fritz, Thomas Wilke


Abstract

We adapt the notion of delayed simulation to alternating parity tree automata and parity games. On the positive side, we show that (i) the corresponding simulation relation can be computed in polynomial time and (ii) 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 tree 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.


Server START Conference Manager
Update Time 20 Feb 2006 at 20:05:03
Maintainer zdang@eecs.wsu.edu.
Start Conference Manager
Conference Systems