Weight Assignment Logic

TL;DR

This paper introduces a weight assignment logic for infinite words that extends MSO logic to describe quantitative properties, establishing equivalences with unambiguous and nondeterministic weighted B"uchi automata.

Contribution

It presents a novel logical framework for quantitative reasoning about infinite words, linking it to weighted automata with different nondeterminism levels.

Findings

Logic is expressively equivalent to unambiguous weighted B"uchi automata.

Extension of the logic matches nondeterministic weighted B"uchi automata.

Provides a formal foundation for quantitative language analysis.

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\"uchi automata. We also consider an extension of weight assignment logic which is expressively equivalent to nondeterministic weighted B\"uchi automata.