A link between multioperator and tree valuation automata and logics (Q2355687)

The authors compare two weight structures designed to overcome some limitations of weighted tree automata (wta) over semirings, namely multioperator monoids (m-monoids) and tree valuation monoids (tv-monoids), as well as the associated weighted tree automata and MSO tree logics. For any given tv-monoid \(\mathcal{D}\) they construct an m-monoid \(\mathcal{A}_{\mathcal{D}}\) such that the weighted tree languages recognized by a wta over \(\mathcal{D}\) are precisely certain projections of the weighted tree languages recognized by a wta over \(\mathcal{A}_{\mathcal{D}}\). Similarly, they construct for any so-called regular product tv-monoid \(\mathbb{D}\) an m-monoid \(\mathcal{A}_{\mathbb{D}}\) such that the weighted tree languages definable by restricted MSO formulas over \(\mathcal{D}\) are precisely certain projections of the weighted tree languages definable by so-called m-expressions over \(\mathcal{A}_{\mathbb{D}}\). The second result actually follows from the first one by the Büchi-like characterizations of the classes of weighted tree languages in question, but the construction given here leads to an essentially lower blow-up of the size of formulas. The authors also present forms of their results that do not involve projections. For the two weight structures, the corresponding wta and MSO logics considered here, cf. [\textit{Z. Fülöp} et al., Theory Comput. Syst. 50, No. 2, 241--278 (2012; Zbl 1280.03045); \textit{M. Droste} et al., Lect. Notes Comput. Sci. 7020, 30--55 (2011; Zbl 1331.68127)].