Strength-based decomposition of Büchi automaton

From LRDE

Abstract

Emptiness-checks enable to know if the language of an automaton is empty or not. These checks are often used in model checking: unfortunately, they are very expensiveparticularly if the automaton is neither weak nor terminal. In order to reduce this expensive check, this work implements an option that permits the extraction of three smaller automata capturing the terminal, weak, and remaining strong components from the original automaton, so that the three corresponding emptiness checks can be performed independently using the most appropriate algorithm.