Emptiness checking is a key operation in the automata-theoretic model checking approach to LTL verification. Explicit state model checkers typically construct the automata on-the-fly and explore their states using depth-first search (DFS). We first cover the fundamentals of emptiness checking and summarize two important emptiness checking theorems for deciding the product automata nonempty. We then survey two classes of on-the-fly emptiness checking algorithms, one based on nested DFS (NDFS) and another based on strongly connected components (SCC). Both can be done on classic Büchi automaton with a single acceptance condition and transition-based generalized Büchi automaton with multiple acceptance conditions. We also highlight cases where both algorithms can be useful. Finally we outline some new achievements and areas that require further research.
展开▼
