Weight Assignment Logic

Abstract

We introduce a weight assignment logic for reasoning about quantitative languages of infinite words. This logic is an extension of the classical MSO logic and permits to describe quantitative properties of systems with multiple weight parameters, e.g., the ratio between rewards and costs. We show that this logic is expressively equivalent to unambiguous weighted Büchi automata. We also consider an extension of weight assignment logic which is expressively equivalent to nondeterministic weighted Büchi automata.

This is the full version of the paper published at DLT 2015

References in corpus (2)

• A Nivat Theorem for Weighted Timed Automata and Weighted Relative Distance Logic
• Multi-weighted Automata and MSO Logic