Eleni Mandrali | Searcharxiv

arXiv2023

Describing weighted safety with weighted LTL over product $ω$-valuation monoids

We define the notion of $k$-safe infinitary series over idempotent ordered totally generalized product $ω$-valuation monoids that satisfy specific properties. For each element $k$ of the underlying structure (different from the neutral elements of the additive, and the multiplicative operation) we determine two syntactic fragments of the weighted $LTL$ with the property that the semantics of the formulas in these fragments are $k$ -safe infinitary series. For specific idempotent ordered totally generalized product $ω$-valuation monoids we provide algorithms that given a weighted Büchi automaton and a weighted $LTL$ formula in these fragments, decide whether the behavior of the automaton coincides with the semantics of the formula.

cs.LO↗

arXiv2022

A translation of weighted LTL formulas to weighted Büchi automata over ω-valuation monoids

In this paper we introduce a weighted LTL over product $ω$-valuation monoids that satisfy specific properties. We also introduce weighted generalized Büchi automata with $\varepsilon$-transitions, as well as weighted Büchi automata with $\varepsilon$-transitions over product $ω$-valuation monoids and prove that these two models are expressively equivalent and also equivalent to weighted Büchi 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üchi automaton with $\varepsilon$-transitions. For generalized product $ω$-valuation monoids that satisfy specific properties we define a weighted LTL, weighted generalized Büchi automata with $\varepsilon$-transitions, and weighted Büchi automata with $\varepsilon$-transitions, and we prove the aforementioned results for generalized product $ω$-valuation monoids as well. The translation of weighted LTL formulas to weighted generalized Büchi automata with $\varepsilon$-transitions is now obtained for a restricted syntactical fragment of the logic.

cs.FL↗