Nested Emptiness Search for Generalized Büchi Automata

Abstract

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. Avoiding a degeneralization step improves the algorithm's worst-case memory requirements and reduces the worst-case number of state visits during the search. We give experimental results and discuss changes needed to make the generalized algorithmcompatible with well-known probabilistic explicit-state model checking techniques.