Regular sets over extended tree structures

DOI10.1016/J.TCS.2011.10.020MaRDI QIDQ764339zbMATH OpenOpenAlexFDO

Authors Séverine Fratani

Publication date 13 March 2012

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2011.10.020

zbMATH Keywords

automata with oracle iterated pushdown structures labeled tree structures MSO-definable sets

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Formal languages and automata (68Q45)

Review text

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.

Recommendations

Cites work

Cited in

(8)

This page was built for publication: Regular sets over extended tree structures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q764339)