2014/04/05 by Cong Tian, Zhenhua Duan, Tian, Cong +1
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic, programming, and type systems #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1404.1436
openalex publication_date 2014/04/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
By separating the principal acceptance mechanism from the concrete acceptance condition of a given Büchi automaton with n states,Schewe presented the construction of an equivalent deterministic Rabin transition automaton with o((1.65n)n) states via 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 12nn2n states). However, the price that is paid is the use of 2n-1 Rabin pairs (instead of n in Safra's construction). Further, by introducing the 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(n2(0.69n√(n))n) and index complexity being n.