Fair Simulation Relations, Parity Games, and State Space Reduction for Buchi Automata

(PREVIOUS TITLE: Faster Algorithms for Computing Fair Simulations and Related Notions, and How tu Use Them for State Space Reductions) We give improved algorithms for computing several variants of simulation relations incorporating fairness over the state space of a Buchi automaton. One such variant is [HKR97]'s fair simulation, for which they give an algorithm that in O(n sup 6) time computers whether a state q sup 1 simulates a state q. Our algorithms, based on a unified parity game framework, compute the entire relation in time O(mn sup 3) and space O(mn)where m is the number of transitions and n the number of states of the automaton. Our algorithms make use of a recent result by Jurdzinski [Jur00].