An efficient implementation of transition-based generalized Büchi automaton determinization

From LRDE

Abstract

Probabilistic model checkers usually rely on deterministic automata as the uniqueness of each path simplifies the probabilistic calculation. Unfortunatelythere are not many LTL translators that produce deterministic automata. Moreover, the automata produced by Spot, a model checker library, are not always deterministic. A classical powerset construction cannot always determinize Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \omega} -automata. However, by memorizing the accepting paths, Safra's construction is able to convert a nondeterministic Büchi automaton into a deterministic Rabin automaton. This change of acceptance condition is necessary as deterministic Büchi automata are less expressive than the nondeterministic version. By implementing this construction, Spot will be able to determinize any automata and compute its complement. In this report, we will see how to efficiently implement the Safra construction and how to expand it to also determinize transition-based generalized Büchi automata.