Weighted nested word automata and logics over strong bimonoids (Q2929640)

A \textit{nested word} is formed of a finite word (on some alphabet \(\Delta\)) with a binary relation defining a nesting. More formally, a nested word is a finite word \(a_1\cdots a_n\) with a binary relation \(\nu\) on \(\{1,\dots,n\}\) such that \(i<j\) if \(\nu(i,j)\), \(\nu\) is a bijection between its projections on its first and second components and finally if \(\nu(i,j)\), \(\nu(i',j')\) and \(i<i'\) then either \(j<i'\) or \(j'<j\) (no overlapping).NEWLINENEWLINENested words are hence a representation for finite trees or functions calls. When \(\nu(i,j)\) holds, \(i\) is said to be a \textit{call} position and \(j\) a \textit{return} position. All other positions are said to be \textit{internal}.NEWLINENEWLINEThis notion was introduced in [\textit{R. Alur} and \textit{P. Madhusudan}, ``Adding nesting structure to words'', Lect. Notes Comput. Sci. 4036, 1--13 (2006; Zbl 1227.68045)], which furthermore defined a suitable notion of finite automata. Intuitively, this is the usual notion of finite automaton with the additional provision that on return positions the transition relation considers both the state at the return position and the state at the matching call position, in order to determine the next state.NEWLINENEWLINEThis paper generalizes nested word automata to bimonoids and gives a characterization of regular sets in terms of a monadic second-order logic.NEWLINENEWLINEA \textit{bimonoid} is a structure \((K,+,\cdot,0,1)\), where \(K\) is a set, \(+\) and \(\cdot\) are binary relations on \(K\) and \(0,1\in K\) such that \((K,+,0)\) and \((K,\cdot,1)\) are monoids. A bimonoid is said to be \textit{strong} if \(+\) is commutative and \(0\) acts as a multiplicative zero, i.e. \(k\cdot 0=0=0\cdot k\) for all \(k\in K\). A bimonoid \((K,+,\cdot,0,1)\) is said to be \textit{bi-locally finite} if both of the monoids \((K,+,0)\) and \((K,\cdot,1)\) are locally finite, i.e. their finitely generated submonoids are finite.NEWLINENEWLINENested automata are generalized to bimonoids by replacing the transition relation with a function into a bimonoid. By mapping a run to the bimonoid's product of the values of its transitions, an automaton defines a formal power series mapping nested words to the sum (in the bimonoid) of the values of its runs. Such power series are said to be \textit{regular}.NEWLINENEWLINEFor \(\mathcal{K}=(K,+,\cdot,0,1)\) a bimonoid, this paper considers the monadic second-order \(\mathcal{K}\)-valued logic (\textit{weighted MSO} for short) built from \(k\) (for \(k\in \mathcal{K}\)), \(x=y\), \(Lab_a(x)\) (for \(a\in \Delta\)), \(x\leq y\), \(\nu(x,y)\), \(x\in X\), Boolean connectors, first-order quantification on lower-case variables and monadic second-order quantification on upper-case variables. The semantics, on a strong bimonoid with a complement function exchanging \(0\) and \(1\), is given by mapping \(\land\) to the bimonoid product, \(\lor\) to its sum and \(\neg\) to the complement function. Quantifiers are treated in a similar way, where first-order universal quantification is mapped to a product in the natural order of the positions and second-order quantification is mapped to a product in lexicographic order of the power set of positions. This last provision is necessary as a monoidal product is not necessarily commutative. A series is said to be definable in weighted MSO if it can be obtained in this way. Finally, the authors consider the second-order existential fragment of this logic formed of all formulas that can be expressed by leading second-order existential quantifiers followed by a first-order formula.NEWLINENEWLINEThe principal results of this paper are the following. For a bi-locally finite strong bimonoid with complement function, a series is regular if and only if it is definable in the second-order existential fragment of weighted MSO. Furthermore, for strong bimonoids, a characterization of regular series is also given, but in terms of a fragment of weighted MSO.