Improving the determinization of Büchi automata

From LRDE

Abstract

Safra's algorithm is a well known construction method which produces a deterministic Rabin automaton from a non-deterministic Büchi automaton. A variant of this method creates deterministic automata with a parity acceptance. However, these methods produce automata with 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 2^{\mathcal{O}(n\log{}n)}} states. There already exist improvements that help reduce the number of states in many cases. In this paper we present two new strategies to help construct smaller deterministic automata. The first strategy uses the strongly connected components and tracks a different Safra run for each of these components separately. The second strategy uses the information that bisimulation gives us to help remove redundant states. This enables us to avoid searching multiples paths which are equivalent and hence reduces the final number of states. We show how these two strategies help reduce the resulting automaton and prove their correctness. We also provide some benchmarks to show that the resulting automata are almost always smaller. Finally, we compare our results to a tool called ltl2dstar which converts LTL formula to deterministic Rabin automaton.