View Related Documents

Abstract

Emptiness check is a key operation in the automata-theoretic approach to LTL verification. However, it is usually done on Büchi automata with a single acceptance condition. We review existing on-the-fly emptiness-check algorithms for generalized Büchi automata (i.e., with multiple acceptance conditions) and show how they compete favorably with emptiness-checks for degeneralized automata, especially in presence of weak fairness assumptions. We also introduce a new emptiness-check algorithm, some heuristics to improve existing checks, and propose algorithms to compute accepting runs in the case of multiple acceptance conditions.

Fulltext Preview

Image of the first page of the fulltext document