A translation of weighted LTL formulas to weighted B\"uchi automata over {\omega}-valuation monoids

TL;DR

This paper develops a framework for translating weighted LTL formulas over product ω-valuation monoids into weighted B"uchi automata with ε-transitions, establishing expressiveness equivalences and effective translation methods for certain logical fragments.

Contribution

It introduces weighted LTL and automata models over product ω-valuation monoids, proving their expressive equivalence and providing translation techniques for specific logical fragments.

Findings

Weighted LTL over product ω-valuation monoids is effectively translatable to weighted B"uchi automata.

Weighted automata models with ε-transitions are expressively equivalent to existing models.

Translation is effective for a syntactic fragment of the weighted LTL logic.

Abstract

In this paper we introduce a weighted LTL over product $\omega$-valuation monoids that satisfy specific properties. We also introduce weighted generalized B\"uchi automata with $\varepsilon$-transitions, as well as weighted B\"uchi automata with $\varepsilon$-transitions over product $\omega$-valuation monoids and prove that these two models are expressively equivalent and also equivalent to weighted B\"uchi automata already introduced in the literature. We prove that every formula of a syntactic fragment of our logic can be effectively translated to a weighted generalized B\"uchi automaton with $\varepsilon$-transitions. For generalized product $\omega$-valuation monoids that satisfy specific properties we define a weighted LTL, weighted generalized B\"uchi automata with $\varepsilon$-transitions, and weighted B\"uchi automata with $\varepsilon$-transitions, and we prove the aforementioned results for generalized product $\omega$-valuation monoids as well. The translation of weighted LTL formulas to weighted generalized B\"uchi automata with $\varepsilon$-transitions is now obtained for a restricted syntactical fragment of the logic.