- Abstract:
-
We give efficient algorithms, improving optimal known bounds, for computing a variety of simulation relations on the state space of a Bchi 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).
- Links To Paper
- 1st Link
- Bibtex format
- @Article{EDI-INF-RR-0639,
- author = {
Kousha Etessami
and Thomas Wilke
and Rebecca Schuller
},
- title = {Fair-Simulation Relations, Parity Games, and State-Space Reduction for B"uchi Automata},
- journal = {SIAM Journal on Computing},
- publisher = {SIAM},
- year = 2005,
- volume = {34(5)},
- pages = {1159-1175},
- doi = {10.1137/S0097539703420675},
- url = {http://epubs.siam.org/sam-bin/dbq/article/42067},
- }
|
