Weighted tree automata over valuation monoids and their characterization by weighted logics

Abstract

Quantitative aspects of systems can be modeled by weighted automata. Here, we deal with such automata running on finite trees. Usually, transitions are weighted with elements of a semiring and the behavior of the automaton is obtained by multiplying the weights along a run. We turn to a more general cost model: the weight of a run is now determined by a global valuation function. An example of such a valuation function is the average of the weights. We establish a characterization of the behaviors of these weighted finite tree automata by fragments of weighted monadic second-order logic. For bi-locally finite bimonoids, we show that weighted tree automata capture the expressive power of several semantics of full weighted MSO logic. Decision procedures follow as consequences. © 2011 Springer-Verlag Berlin Heidelberg.