Deterministic ω automata vis-a-vis deterministic buchi automata

Abstract

ω-automata are finite state automata that accept infinite strings. The class of ω-regular languages is exactly the set accepted by nondeterministic Buchi and L-automata, and deterministic Muller, Rabln, and Streett automata. The languages accepted by deterministic Buchi automata (DBA) form a strict subset of the class of ω-regular languages. Landweber characterized deterministic ω-automata whose languages are realizable by DBA. We provide an alternative proof of Landweber’s theorem and give polynomial time algorithms to check if a language L specified as a deterministic Muller, L-, Streett, or Rabin automaton can be realized as a DBA. We identify a sub-class of deterministic Muller, L-, Streett, and Rabin automata, called Buchi-type automata, which can be converted to an equivalent DBA on the same transition structure in polynomial time. For this subset of ω-automata, our transformation yields the most efficient algorithms for checking language inclusion-important for computer verification of reactive systems. We prove that a deterministic L-(DLA) or Rabin automaton (DRA), unlike deterministic Muller or Streett automata, is Buchi.type if and only if its language is realizable as a DBA. Therefore, for languages that are realizable as DBA, DBA are as compact as DRA or DLA.