A Büchi-like theorem for weighted tree automata over multioperator monoids (Q692910): Difference between revisions

There is a quite well-know correspondence between recognizability by finite automata and definability in monadic second-order logic (MSO) going back to results of \textit{J. R. Büchi} [Z. Math. Logik Grundlagen Math. 6, 66--92 (1960; Zbl 0103.24705)] and \textit{C. C. Elgot} [Trans. Am. Math. Soc. 98, 21--51 (1961; Zbl 0111.01102); Errata 103, 558--559 (1962)], which now covers, beyond the original case of strings, tree-like structures. In [Lect. Notes Comput. Sci. 3580, 513--525 (2005; Zbl 1084.03036); Theor. Comput. Sci. 380, No. 1--2, 69--86 (2007; Zbl 1118.68076); Handbook of Weighted Automata. Berlin: Springer (2009; Zbl 1200.68001), Chapter 5], \textit{M. Droste} and \textit{P. Gastin} extended this correspondence further by considering logical evaluation, no more in a Boolean algebra, but in the more general setting of semirings. The reviewed paper considers a similar extension but to multioperator monoids, which are commutative monoids with additional operations. The authors hence show that in this case also there is an equivalence between being recognizable by a finite tree automata and being definable in MSO. They furthermore show that their result subsumes the case of semiring by deriving Theorem 7.2 of [\textit{M. Droste} and \textit{H. Vogler}, Theory Comput. Syst. 48, No. 1, 23-47 (2011; Zbl 1226.03048)] from their own result.