Buchi Determinization Made Tighter

TL;DR

This paper presents a tighter determinization construction for Büchi automata, reducing the number of Rabin pairs and improving state complexity, with applications to parity automata.

Contribution

It improves Schewe's Büchi automaton determinization by reducing Rabin pairs and introduces a new parity automaton determinization method with better complexity.

Findings

Reduced Rabin pairs to 2^{ceil((n-1)/2)}

Achieved improved state complexity for parity automata

Provided a new determinization method with lower index complexity

Abstract

By separating the principal acceptance mechanism from the concrete acceptance condition of a given B\"{u}chi automaton with $n$ states,Schewe presented the construction of an equivalent deterministic Rabin transition automaton with $o((1.65n)^n)$ states via \emph{history trees}, which can be simply translated to a standard Rabin automaton with $o((2.26n)^n)$ states. Apart from the inherent simplicity, Schewe's construction improved Safra's construction (which requires $12^nn^{2n}$ states). However, the price that is paid is the use of $2^{n-1}$ Rabin pairs (instead of $n$ in Safra's construction). Further, by introducing the \emph{later introduction record} as a record tailored for ordered trees, deterministic automata with Parity acceptance condition is constructed which exactly resembles Piterman's determinization with Parity acceptance condition where the state complexity is $O((n!)^2)$ and the index complexity is $2n$.In this paper, we improve Schewe's construction to $2^{\lceil (n-1)/2\rceil}$ Rabin pairs with the same state complexity. Meanwhile, we give a new determinization construction of Parity automata with the state complexity being $o(n^2(0.69n\sqrt{n})^n)$ and index complexity being $n$.