Characterization of properties and relations defined in monadic second order logic on the nodes of trees
Roderick Bloem, Joost Engelfriet · 1997
. A formula from monadic second order (mso) logic with one free variable can be used to define a property of the nodes of a tree. Similarly, an mso formula with two free variables can be used to define a binary relation between the nodes of a tree. It is proved that a node relation is mso definable iff it can be computed by a finite-state tree-walking automaton, provided the automaton can test mso definable properties of the nodes of the tree; if the relation is a function, the automaton is deterministic. It is also proved that a node property is mso definable iff it can be computed by an attribute grammar of which all attributes have finitely many values. mso definable node properties are computable in linear time, mso definable node relations in quadratic time, and mso definable node functions in linear time. 1 Introduction It is shown in [Buc, Elg] that a set of strings can be defined in monadic second order logic if and only if it can be recognized by a finite-state automaton. Th...