Nested emptiness search for generalized Buchi automata

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.