1988/01/01 by Muli Safra · 2 citations
Computer Science · Biochemistry, Genetics and Molecular Biology · Mathematics · #semigroups and automata theory #Chemical Synthesis and Analysis #Formal Methods in Verification #Nondeterministic algorithm #Büchi automaton #Automaton #Discrete mathematics #Automata theory #Computer science #Quantum finite automata #Successor cardinal #ω-automaton #Order (exchange) #Omega #Exponential function #Upper and lower bounds #Mathematics #Theoretical computer science #Combinatorics #Deterministic automaton
paper · doi:10.1109/sfcs.1988.21948
openalex publication_date 1988/01/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/29
Automata on infinite words were introduced by J.R. Buchi (1962) in order to give a decision procedure for S1S, the monadic second-order theory of one successor. D.E. Muller (1963) suggested deterministic omega -automata as a means of describing the behavior of nonstabilising circuits. R. McNaughton (1966) proved that classes of languages accepted by nondeterministic Buchi automata and by deterministic Muller automata are the same. His construction and its proof are quite complicated, and the blow-up of the construction is double exponential. The author presents a determinisation construction that is simpler and yields a single exponent upper bound for the general case. This construction is essentially optimal. It can also be used to obtain an improved complementation construction for Buchi automata that is also optimal. Both constructions can be used to improve the complexity of decision procedures that use automata-theoretic techniques.>