Monadic second order logic on tree-like structures

Abstract

An operation M + constructing from a given structure M a tree-like structure which domain consists of the sequences of elements of M is considered. A notion of automata running on such tree-like structures is defined. This notion is parametrised by a set of basic formulas. It is shown that if basic formulas satisfy some conditions then the class of languages recognised by automata is closed under disjunction, complementation and projection. For one choice of basic formulas we obtain a characterisation of MSOL over tree-like structures. This characterisation allows us to show that MSOL theory of tree-like structures is effectively reducible to that of the original structures. For a different choice of basic formulas we obtain a characterisation of MSOL on trees of arbitrary degree and the proof that it is equivalent to the first order logic extended with the unary least fixpoint operator.