Name
Abstract | ||
|---|---|---|
We propose and evaluate antichain algorithms to solve the universality and language inclusion problems for nondeterministic Buchi automata, and the emptiness problem for alternating Buchi automata. To obtain those algorithms, we establish the existence of simulation pre-orders that can be exploited to efficiently evaluate fixed points on the automata defined during the complementation step (that we keep implicit in our approach). We evaluate the performance of the algorithm to check the universality of Buchi automata using the random automaton model recently proposed by Tabakov and Vardi. We show that on the difficult instances of this probabilistic model, our algorithm outperforms the standard ones by several orders of magnitude. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.2168/LMCS-5(1:5)2009 | LOGICAL METHODS IN COMPUTER SCIENCE |
Keywords | Field | DocType |
alternating Buchi automata,nondeterministic Buchi automata,emptiness,universality,language inclusion,antichains | Discrete mathematics,Combinatorics,Antichain,Model checking,Nondeterministic algorithm,Automaton,Algorithm,Statistical model,Fixed point,Universality (philosophy),Mathematics,Büchi automaton | Journal |
Volume | Issue | ISSN |
5 | 1 | 1860-5974 |
Citations | PageRank | References |
27 | 1.32 | 18 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Laurent Doyen | 1 | 979 | 55.96 |
| Jean-François Raskin | 2 | 1735 | 100.15 |
| Orna Grumberg | 3 | 4361 | 351.99 |