Regular sets over extended tree structures (Q764339)

From the text: ``[W]e exhibit labeled tree structures having a decidable MSO-theory, for which every satisfiable MSO-formula admits an MSO-definable model, and for which we can provide an automata-characterization of the definable sets. To achieve this goal, we introduce new theoretical objects. We define a class of word/tree automata with prefix-oracles (i.e., sets of words over the input alphabet) used to test the already processed prefixes of inputs. Forests recognized by prefix-oracles automata possess useful properties, in particular, Rabin's correspondence between regular forests and models of MSO-formulas over infinite trees can be extended to these languages: forests recognized by automata with oracles \(O_1,\dots,O_m\) are forests MSO-definable in a tree structure extended by unary relations \(O_1,\dots,O_m\). We establish MSO properties transfer theorems from a graph structure, toward a tree structure. This approach is common for transfer reducing decidability (for example, the reduction of decidability of the MSO-theory from a structure to its tree-like structure, etc.), or from a graph to its unfolding. We give a reduction which allows to obtain new decidability results which are not covered by the ones cited above. In addition, we give transfer theorems that apply to MSO definable sets in tree structures and to classes of automata recognizing them. In particular, we are interested in the selection property. This property ensures for a structure \({\mathcal S}\) that any satisfiable formula admits at least one model MSO-definable in \({\mathcal S}\). Some important structures satisfy the selection property. Let \(t\) be a labeled tree and \(\underline{t}\) be the structure associated with \(t\). For any monoid morphism \(\mu\), and under some simple hypothesis on the labeling of \(t\), we obtain the following main results: \(\bullet\) Transfer of decidability: if \(\mu(\underline{t})\) has a decidable MSO-theory, then \(\underline{t}\) has a decidable MSO-theory. \(\bullet\) Transfer of the selection property: under some condition on \(\mu\), if \(\mu(\underline{t})\) satisfies the selection property, then \(\underline{t}\) satisfies it too. \(\bullet\) Theorem of structure: under the same condition as above on \(\mu\), if \(\mu(\underline{t})\) satisfies the selection property, then any set is MSO-definable in \(\underline{t}\) iff it is recognized by a finite automaton using only oracles of the form \(\mu^{-1}(D)\) where \(D\) is MSO-definable in \(\mu(\underline{t})\). (Then each oracle tests a property MSO-definable in \(\mu(\underline{t})\), on the image by \(\mu\) of input word prefixes.) Applying these results, we obtain tree structures having a decidable MSO theory and classes of languages having two equivalent characterizations: one as languages recognized by automata with oracles, and the one as sets MSO-definable in some labeled tree structures. To complete this extension of regular languages, we have to take into account a third characterization: regular languages are exactly sets of pushdown contexts generated by a pushdown system of transitions. This is done in the last part of the paper in which we consider the stack languages generated by `iterated pushdown automata', which are automata whose memory is roughly a stack of stack of stack \dots. We define a notion of `regular' sets of \(k\)-pushdown (i.e., stacks with \(k\) level of embedded pushdowns) which generalize the notion of regular set of words.''