Fair simulation relations, parity games, and state space reduction for Buchi automata

We give efficient algorithms, improving optimal known bounds, for computing a variety of simulation relations on the state space of a Buchi automaton. Our algorithms are derived via a unified and simple parity-game framework. This framework incorporates previously studied notions like fair and direct simulation, but also a new natural notion of simulation called delayed simulation, which we introduce for the purpose of state space reduction. We show that delayed simulation-unlike fair simulation-preserves the automaton language upon quotienting and allows substantially better state space reduction than direct simulation. Using our parity-game approach, which relies on an algorithm by Jurdzinski, we give efficient algorithms for computing all of the above simulations. In particular, we obtain an O(mn(3))-time and O(mn)-space algorithm for computing both the delayed and the fair simulation relations. The best prior algorithm for fair simulation requires time and space O(n(6)). Our framework also allows one to compute bisimulations: we compute the fair bisimulation relation in O(mn(3)) time and O(mn) space, whereas the best prior algorithm for fair bisimulation requires time and space O(n(10)).