Regular languages of nested words: fixed points, automata, and synchronization (Q649107)

A nested finite or infinite word represents a model of execution of a program with recursive procedure calls. The nesting relation then connects matching calls and returns, while other elements correspond to internal operations. Let \(\Sigma\) be a finite alphabet and let \(|w|\) denote the length of \(w\in\Sigma\)*. A finite nested word over \(\Sigma\) is a pair \(wh=(w,h)\), where \(a\in\Sigma\)* and \(h\) is a binary matching relation on \(\{1,2,\dots,|w|\}\) that satisfies: (1) \(h(i,j)\to i<j\); (2) \(h(i,j)\) and \(h(i,j_1)\) implies \(j=j_1\), \(h(i,j)\) and \(h(i_1,j)\) implies \(i=i_1\); (3) if \(h(i,j),h(i_1,j_1),i<i_1\) then either \(j<i_1\) or \(j_1<j\). A nested \(\omega\)-word is defined by analogy. A nested word deterministic or nondeterministic automaton (NWA) runs from left to right as a finite state automaton, but each time it encounters a return position, the next state depends not only on the current state but also on the state of the matching call. A nondeterministic nested word automaton (NWA) is a tuple \({A}=(\Sigma, {Q}, {Q}_0, {Q}_{f}, {P}, {P}_0, {P}_{f}, \delta_{c}, \delta_{i}, \delta_{r})\), where \({P}\) is a finite set of hierarchical states, \({Q}\cap {P}\) is empty, \({P}_0\subseteq {P}\) is the set of initial hierarchical states, \({P}_{f}\subseteq{P}\) is the set of final hierarchical states, \(\delta_{c} :{Q}\otimes\Sigma^{<}\rightarrow 2^{Q \otimes P }\) is the call transition function, \(\delta_{i} : {Q}\otimes\Sigma\rightarrow 2^{Q}\) is the internal transition function, \(\delta_{r}:{Q}\otimes{P}\otimes \Sigma^{>} \rightarrow 2^{Q}\) is the return transition function. A nested word automaton is deterministic (NWA) if \({Q}_{0}\) and \({P}_{0}\) are singleton sets and cardinalities of \(|\delta_{c}(q,a)|\), \(|\delta_{i}(q,a)|\), \(|\delta_{r}(q,a)|\) are equal to 1. A nested word language is regular if it is recognized by a NWA. A regular language of nested words is a set of nested words accepted by a NWA. Over nested words, the vocabulary of monadic second-order logic (MSO) contains the following: predicates \(Pa(w)\) (word \(w\) is ended by symbol \(a\)), predicate of linear order \(i < j\) over the natural numbers \(\mathbb{N}\), predicate \(h(i,j)\) over \(\mathbb{N}\) which matches call \(i\) and its return \(j\). First-order variables in MSO are interpreted as positions in a nested word, while monadic second-order variables range over sets of positions in a nested word. Regular languages of nested words are a special case of visibly push-down languages (VPL) which are a restriction of the class of context-free languages. VPL has the input alphabet \(I\) which is partitioned into three parts \(I_c\), \(I_r\), \(I_i\) of symbols viewed as procedure calls, returns, internal operations. Stair VPL controls unmatched calls. The \(\mu\)-calculus \(L_{\mu}\) over nested words is defined as a grammar with Boolean operations with modalities. Each formula of \(L_{\mu}\) without free languages defines a language which is a class of nested words. Every MSO formula with one free first-order variable defines a unary query, and every MSO sentence defines a language. To deal with unary queries, the authors consider \(L_{\mu}\) with the past, i.e. \(L_{\mu}^{\text{full}}\). These are the main results of the article under review: \textbf{Theorem 1}. For finite nested words and nested \(\omega\)-words, MSO and \(L_{\mu}^{\text{full}}\) define the same classes of unary queries. The languages of nested words (resp. nested \(\omega\)-words) definable in MSO and \(L_{\mu}\) are the same. \textbf{Theorem 2}. Over nested \(\omega\)-words, MSO, \(\omega\)-NWA with Büchi acceptance condition, deterministic \(\omega\)-NWA with Muller acceptance condition define precisely the regular languages. Translations between these formalisms are effective. \textbf{Theorem 3}. For every \(\omega\)-alternating NWA, there exists (and can be effectively constructed) an equivalent \(\omega\)-NWA with a Büchi acceptance condition. \textbf{Theorem 4}. For every Büchi alternating VPA, there exists (and can be effectively constructed) an equivalent Büchi nondeterministic VPA. \textbf{Theorem 5}. The nonemptiness problem is undecidable for simplified 2-letter-to-letter NWAs (and thus for \(k\)-letter-to-letter NWAs for \(k>1\)).