Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata

Kousha Etessami, Thomas Wilke, Rebecca A. Schuller

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We give efficient algorithms, beating or matching 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 our main motivation is state space reduction, and for this purpose we introduce a new natural notion of simulation, called delayed simulation. We show that, unlike fair simulation, delayed simulation preserves the automaton language upon quotienting, and that it allows substantially better state reduction than direct simulation.We use the parity-game approach, based on a recent algorithm by Jurdzinski, to efficiently compute all the above simulation relations. In particular, we obtain an O(mn 3)-time and O(mn)-space algorithm for computing both the delayed and fair simulation relations. The best prior algorithm for fair simulation requires time O(n 6) ([HKR97]).

Our framework also allows one to compute bisimulations efficiently: 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 O(n 10) ([HR00]).
Original languageEnglish
Title of host publicationAutomata, Languages and Programming
Subtitle of host publication 28th International Colloquium, ICALP 2001, Crete, Greece, July 8-12, 2001, Proceedings
PublisherSpringer Berlin Heidelberg
Pages694-707
Number of pages14
Volume2076
ISBN (Electronic)978-3-540-48224-6
ISBN (Print)978-3-540-42287-7
DOIs
Publication statusPublished - 2001

Cite this