Multi-weighted Automata and MSO Logic

TL;DR

This paper introduces a general model for multi-weighted automata and a corresponding MSO logic, establishing their expressive equivalence and decidability for finite and infinite words, thus advancing quantitative system modeling.

Contribution

It presents a novel multi-weighted automata model and an MSO logic, proving their expressive equivalence and effective translation, which leads to new decidability results.

Findings

Multi-weighted automata model multiple quantitative aspects.

Multi-weighted MSO logic is expressively equivalent to automata.

Decidability results are obtained for the logic over finite and infinite words.

Abstract

Weighted automata are non-deterministic automata where the transitions are equipped with weights. They can model quantitative aspects of systems like costs or energy consumption. The value of a run can be computed, for example, as the maximum, limit average, or discounted sum of transition weights. In multi-weighted automata, transitions carry several weights and can model, for example, the ratio between rewards and costs, or the efficiency of use of a primary resource under some upper bound constraint on a secondary resource. Here, we introduce a general model for multi-weighted automata as well as a multiweighted MSO logic. In our main results, we show that this multi-weighted MSO logic and multi-weighted automata are expressively equivalent both for finite and infinite words. The translation process is effective, leading to decidability results for our multi-weighted MSO logic.