Languages of infinite traces and deterministic asynchronous automata

Abstract. In the theory of deterministic automata for languages of infinite words, a fundamental fact relates the family of infinitary limits of regular lan-guages and the family of ω-languages recognized by deterministic Büchi automata. With the known definitions of asynchronous automata, this observation does not extend to the context of traces. A major difficulty is posed by processes that stall after finitely many transitions. We introduce the family of deterministic, synchronization-aware asynchronous automata which – using as parameter the set of processes that stay live ad infinitum – allows us to settle an open ques-tion, namely, whether there exists a deterministic Büchi automaton recognizing precisely the infinitary limit of a regular trace language. Also, the corresponding class of unparameterized Muller automata captures all ω-regular trace languages.