Weighted Automata and Logics on Graphs

Weighted automata model quantitative features of the behavior of systems and have been investigated for various structures like words, trees, traces, pictures, and nested words. In this paper, we introduce a general model of weighted automata acting on graphs, which form a quantitative version of Thomas' unweighted model of graph acceptors. We derive a Nivat theorem for weighted graph automata which shows that their behaviors are precisely those obtainable from very particular weighted graph automata and unweighted graph acceptors with a few simple operations. We also show that a suitable weighted MSO logic is expressively equivalent to weighted graph automata. As a consequence, we obtain corresponding Buchi-type equivalence results known from the recent literature for weighted automata and weighted logics on words, trees, pictures, and nested words. Establishing such a general result has been an open problem for weighted logic for some time.