Complementing deterministic Büchi automata in polynomial time

摘要

For any Buchi automaton Γ with n states which accepts the (ω-regular) language L(Γ), an explicit construction is given for a Büchi automaton Γ with 2n states which, when Γ is deterministic, accepts exactly the complementary language L(Γ)′. It follows that the nonemptiness of complement problem for deterministic Buchi automata (i.e., whether L(Γ)′ = ⊘) is solvable in polynomial time. The best previously known construction for complementing a deterministic Büchi automaton with n states has O(24n2) states; for nondeterministic Γ, determining whether L(Γ)′ = ⊘, is known to be PSPACE-complete. Interest in deterministic Büchi automata arises from the suitability of deterministic automata in general to describe properties of physical systems; such properties have been found to be more naturally expressible by deterministic automata than by nondeterministic automata. However, if Γ is nondeterministic, then Γ provides a “poor man's” approximate inverse to Γ in the following sense: L(Γ)′ ⊂ L(Γ), and as nondeterministic branches of T are removed, the two languages become closer. Hence, for example, given two nondeterministic Buchi automata Λ and Γ, one may test for containment of their associated languages through use of the corollary that L (Λ ∗ Γ = ⊘ ⇒ L (Λ) ⊂ L(Γ) (where Γ ∗ Γ is one of the standard constructions satisfying L (Λ ∗ Γ) = L (Λ) ∩ L(Γ)). The “error term” L = L(Γ) ⧹ L(Γ)′ may be deter exactly, and whether L = ⊘ may be determined in time O(e2), where e is the number of edges of Γ.