A weighted MSO logic with storage behaviour and its Büchi-Elgot-Trakhtenbrot theorem

Abstract

We introduce a weighted MSO-logic in which one outermost existential quantification over behaviours of a storage type is allowed. As weight structures we take unital valuation monoids which include all semirings, bounded lattices, and computations of average or discounted costs. Each formula is interpreted over finite words yielding elements in the weight structure. We prove that this logic is expressively equivalent to weighted automata with storage. In particular, this implies a Büchi-Elgot-Trakhtenbrot Theorem for weighted iterated pushdown languages. For this choice of storage type, the satisfiability problem of the logic is decidable for each bounded lattice provided that its infimum is computable.