Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata
Kousha Etessami, Thomas Wilke, Rebecca A. Schuller · SIAM Journal on Computing · 2005
We give efficient algorithms, improving optimal known bounds, for computing a variety of simulation relations on the state space of a Büchi 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 Jurdziński, 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 ).