Nested emptiness search for generalized Buchi automata
Heikki Tauriainen · 2004
We generalize the classic explicit state emptiness checking algorithm for Buchi word automata (the "nested depth-first search") into Buchi 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.