Ω-Automata: A Coalgebraic Perspective on Regular ω-Languages

In this work, we provide a simple coalgebraic characterisation of regular ω-languages based on languages of lassos, and prove a number of related mathematical results, framed into the theory of a new kind of automata called Ω-automata. In earlier work we introduced Ω-automata as two-sorted structures that naturally operate on lassos, pairs of words encoding ultimately periodic streams (infinite words). Here we extend the scope of these Ω-automata by proposing them as a new kind of acceptor for arbitrary streams. We prove that Ω-automata are expressively complete for the regular ω-languages. We show that, due to their coalgebraic nature, Ω-automata share some attractive properties with deterministic automata operating on finite words, properties that other types of stream automata lack. In particular, we provide a simple, coalgebraic definition of bisimilarity between Ω-automata that exactly captures language equivalence and allows for a simple minimization procedure. We also prove a coalgebraic Myhill-Nerode style theorem for lasso languages, and use this result, in combination with a closure property on stream languages called lasso determinacy, to give a characterization of regular ω-languages.