A Buechi-Like Theorem for Weighted Tree Automata over Multioperator Monoids

摘要

A multioperator monoid A is a commutative monoid with additional operations on its carrier set. A weighted tree automaton over A is a finite state tree automaton of which each transition is equipped with an operation of A. We define M-expressions over A in the spirit of formulas of weighted monadic second-order logics and, as our main result, we prove that if A is absorptive, then the class of tree series recognizable by weighted tree automata over A coincides with the class of tree series definable by M-expressions over A. This result implies the known fact that for the series over semirings recognizability by weighted tree automata is equivalent with definability in syntactically restricted weighted monadic second-order logic. We prove this implication by providing two purely syntactical transformations, from M-expressions into formulas of syntactically restricted weighted monadic second-order logic, and vice versa.