Natural Colors of Infinite Words

TL;DR

This paper introduces a concept of natural color for infinite words in omega-regular languages, providing a canonical automaton form that simplifies analysis and recognition of these languages.

Contribution

It defines the natural color of an infinite word based on omega-regular languages and shows how to derive a streamlined automaton with a canonical form from any deterministic parity automaton.

Findings

Natural color can be traced from deterministic parity automata after simple transformations.

The streamlined automaton has a 'co-run' with the natural color, simplifying analysis.

It yields a canonical, minimal good-for-games co-Büchi automaton for each omega-regular language.

Abstract

While finite automata have minimal DFAs as a simple and natural normal form, deterministic omega-automata do not currently have anything similar. One reason for this is that a normal form for omega-regular languages has to speak about more than acceptance - for example, to have a normal form for a parity language, it should relate every infinite word to some natural color for this language. This raises the question of whether or not a concept such as a natural color of an infinite word (for a given language) exists, and, if it does, how it relates back to automata. We define the natural color of a word purely based on an omega-regular language, and show how this natural color can be traced back from any deterministic parity automaton after two cheap and simple automaton transformations. The resulting streamlined automaton does not necessarily accept every word with its natural color, but it has a 'co-run', which is like a run, but can once move to a language equivalent state, whose color is the natural color, and no co-run with a higher color exists. The streamlined automaton defines, for every color c, a good-for-games co-B\"uchi automaton that recognizes the words whose natural colors w.r.t. the represented language are at least c. This provides a canonical representation for every $\omega$-regular language, because good-for-games co-B\"uchi automata have a canonical minimal (and cheap to obtain) representation for every co-B\"uchi language.