Paths in infinite trees : logics and automata
Alexandra Spelten, Wolfgang H Thomas · RWTH Publications (RWTH Aachen) · 2013
In this thesis, several logical systems over infinite trees and infinite words are studied in their relation to finite automata. The first part addresses (over the infinite binary tree) “path logic” and “chain logic” as fragments of monadic second-order logic that allow quantification over paths, respectively subsets of paths of the binary tree. Many systems of branching-time logic are subsumed by chain logic. We introduce ranked alternating tree automata as a computation model that characterizes chain logic. The main idea is to associate ranks to states such that in an automaton run, starting from the root, the ranks have to decrease and are allowed to remain unchanged only in one direction (either in existential or universal branching). The second part of the thesis is motivated by chain logic over infinite-branching trees (where the successors of a node are indexed by natural numbers). A path through the N-branching tree is given by an omega-word over the infinite alphabet N. As a preparation for the study of path logics over such trees, we develop a theory of logics and automata over infinite alphabets, more precisely over alphabet frames (M,L), given by a relational structure M, supplying the alphabet, and a logic L that is used in specifying letter properties and automaton transitions. Two types of automata (and logics) for the specification of word properties are presented, depending whether or not relations between successive letters are included. We obtain results that clarify under which circumstances the nonemptiness problem is solvable, and we apply these results to show (un-)decidability results on path logics over infinitely-branching trees that result from given structures by weak and strong “tree iteration”.