The automata-theoretic approach for model checking of linear-time temporal
properties involves the emptiness check of a large Büchi automaton.
Specialized emptiness-check algorithms have been proposed for the cases where
the property is represented by a weak or terminal automaton.
When the property automaton does not fall into these categories, a
general emptiness check is required. This paper focuses on this class
of properties. We refine previous approaches by classifying
strongly-connected components rather than automata, and suggest a
decomposition of the property automaton into three smaller automata
capturing the terminal, weak, and the remaining strong behaviors of
the property. The three corresponding emptiness checks can be
performed independently, using the most appropriate algorithm.
Such a decomposition approach can be used with any automata-based
model checker. We illustrate the interest of this new approach using
explicit and symbolic LTL model checkers.