Infinite trees and automaton-definable relations over \(\omega\)-words (Q1199531): Difference between revisions

Relations over \(\omega\)-words, in short: \(\omega\)-relations, are studied using a representation by sets of infinite trees (``tree languages''). An \(\omega\)-word over an alphabet with \(k\) letters is considered as a path through the \(k\)-ary tree, an \(n\)-tuple of \(\omega\)-words as an \(n\)-tupe of paths (coded by an appropriate valuation of the \(k\)-ary tree by values in \(\{0,1\}^ n\)), and hence an \(\omega\)-relation as a tree language. In the first part of the paper we give a logical characterization of the ``Rabin recognizable relations'' (whose associated tree languages are recognized by Rabin tree automata) in terms of ``weak chain logic'', a restriction of monadic second-order logic over trees where set quantifiers range over finite subsets of paths only. This answers positively a question raised by \textit{H. Laeuchli} and \textit{C. Savioz} [J. Symb. Logic 52, 219-226 (1987; Zbl 0628.03005)], concerning reducibility of monadic second-order logig \(SkS\) to the weak monadic logic \(WSkS\) if sets of paths are to be defined. In the second part of the paper we extend chain logic by adjoining the ``equal level predicate'' \(E\) over trees, obtaining ``chain logic \(+E\)''. We characterize the \(\omega\)-relations which (in the tree language representation) are definable chain logic \(+E\): They are the \(\omega\)- relations recognized by sequential Büchi automata working synchronously on tuples of \(\omega\)-words. As a consequence, the theory of the \(k\)-ary tree in the language of chain logic \(+E\) is decidable. This logic covers tree properties which are not expressible in the monadic second-order logic \(SkS\). As an application it is shown that the correctness of finite-state programs is decidable with respect to specifications of path oriented logics (e.g., extended computation tree logic \(ECTL^*\)) even if the equal level predicate is added.