Completeness results for omega-regular algebras (Q2347912)

A sound and complete axiomatization of the equational theory of \(\omega\)-regular expressions, i.e., expressions that denote regular languages of infinite words, has been given by \textit{K. Wagner} [Elektron. Informationsverarbeitung Kybernetik 12, 337--354 (1976; Zbl 0335.94028)]. In the present paper, which is a completed and extended version of a conference paper by the second and the third author [Lect. Notes Comput. Sci. 7560, 179--194 (2012; Zbl 1335.68158)], the authors present two sound and complete algebraic axiomatizations in which no rule involves side-conditions like the empty word property (ewp) check used in Wagner's axiomatization. The first axiomatization is for Wagner algebras; these are certain two-sorted module-like structures in which one sort corresponds to finite words and the other one to \(\omega\)-words. The use of ewp-conditions is avoided by considering Wagner algebras without a multiplicative unit, and the completeness is proved relative to Wagner's axiomatization. For each non-unital Wagner algebra, a unital Wagner algebra satisfying the same identities in which the unit symbol does not appear is constructed. The second axiomatization concerns so-called \(\omega\)-algebras, which are Kleene algebras extended by an operation of infinite iteration. These algebras are one-sorted, and in a standard word model the finite words and the \(\omega\)-words over the given alphabet form together the set of elements. In this case, completeness is proved by first considering 0-free \(\omega\)-algebras.