Infinite trees and automaton-definable relations over \(\omega\)-words
type: Item
instance of: scholarly article
title: Infinite trees and automaton-definable relations over \(\omega\)-words
zbMATH Open document ID: 0760.68043
DOI: 10.1016/0304-3975(92)90090-3
author: Wolfgang Thomas
published in: Theoretical Computer Science
publication date: 1993-01-16T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68Q45
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03D05
zbMATH DE Number: 94456
zbMATH Keywords: infinite words
zbMATH Keywords: monadic second-order logic
zbMATH Keywords: tree automata
zbMATH Keywords: Büchi automata
MaRDI profile type: Publication
full work available at URL: 0304-3975(92)90090-3
OpenAlex ID: W1570009926
cites work: Q3859267
cites work: Q5525343
cites work: Automatic verification of finite-state concurrent systems using temporal logic specifications
cites work: Decidability and undecidability of extensions of second (first) order theory of (generalized) successor
cites work: Uniform inevitability is tree automaton ineffable
cites work: Q4035657
cites work: Two decidability problems for infinite words
cites work: Relations rationnelles infinitaires
cites work: Q3768883
cites work: Languages that Capture Complexity Classes
cites work: Monadic second order definable relations on the binary tree
cites work: Concatenation as a basis for arithmetic
cites work: Decidability of Second-Order Theories and Automata on Infinite Trees
cites work: Q5541339
cites work: On the bounded monadic theory of well-ordered structures
cites work: Q4385530
cites work: Reasoning about infinite computations
description: scientific article; zbMATH DE number 94456