Strength-based decomposition of Büchi automaton

From LRDE

The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

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.