Improving the determinization of Büchi automata

Authors

Alexandre Lewkowicz

Type

techreport

Year

2016

Number

1601

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 $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.