Strength-based decomposition of Büchi automaton

From LRDE

Revision as of 17:06, 9 January 2018 by Bot (talk | contribs) (Created page with "{{CSIReport | authors = Claire Parquier | title = Strength-based decomposition of Büchi automaton | year = 2015 | abstract = Emptiness-checks enable to know if the language o...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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.