Nested emptiness search for generalized Büchi automata

Abstract

We generalize the classic explicit state emptiness checking algorithm for Bchi word automata (the "nested depth-first search") into Bchi automata with multiple acceptance conditions. Bypassing an explicit acceptance condition reduction improves the algorithm's worst case memory requirements. The generalized algorithm handles multiple unconditional and weak fairness constraints directly and is compatible with well-known probabilistic explicit state model checking techniques.