Fourth International Conference on Application of Concurrency to System Design (ACSD'04)
Nested Emptiness Search for Generalized B?chi Automata
Hamilton, Ontario, Canada
June 16-June 18
ISBN: 0-7695-2077-4
We generalize the classic explicit state emptiness checking algorithm for B?chi word automata (the "nested depth-first search") into B?chi automata with multiple acceptance conditions. Bypassing an explicit acceptance condition reduction improves the algorithm's worst case memory requirements. The generalized algorithm is compatible with well-known probabilistic explicit state model checking techniques and model checking under fairness constraints.