There are various types of automata on infinite words, differing in their acceptance conditions. The most classic ones are weak, Bu ̈chi, co-Bu ̈chi, parity, Rabin, Streett, and Muller. This is opposed to the case of automata on finite words, in which there is only one standard type. The natural question is why—Why not a single type? Why these particular types? Shall we further look into additional types?For answering these questions, we clarify the succinctness of the different automata types and the size blowup involved in performing boolean operations on them. To this end, we show that unifying or intersecting deterministic automata of the classic ω-regular- complete types, namely parity, Rabin, Streett, and Muller, involves an exponential size blowup.We argue that there are good reasons for the classic types, mainly in the case of nondeterministic and alternating automata. They admit good size and complexity bounds with respect to succinctness, boolean operations, and decision procedures, and they are closely connected to various logics.Yet, we also argue that there is place for additional types, especially in the case of deterministic automata. In particular, generalized-Rabin, which was recently introduced, as well as a disjunction of Streett conditions, which we call hyper-Rabin, where the latter further generalizes the former, are interesting to consider. They may be exponentially more succinct than the classic types, they allow for union and intersection with only a quadratic size blowup, and their nonemptiness can be checked in polynomial time.
Alternating Automata and Logics over Infinite Words
