Systolic tree omega-languages: the operational and the logical view

The class of omega-languages recognized by systolic (binary) tree automata is introduced. This class extends the class of Buchi omega-languages though maintaining the closure under union, intersection and complement and the d ecidability of emptiness. The class of systolic tree omega-languages is cha racterized in terms of a (suitable) concatenation of(finitary) systolic tre e languages, A generalization of Buchi Theorem is provided which establishe s a correspondence between systolic tree omega-languages and a suitable ext ension of the sequential calculus SIS. (C) 2000 Elsevier Science B.V. All r ights reserved.