Describing weighted safety with weighted LTL over product \(\omega\)-valuation monoids

Abstract

We define the notion of \(k\)-safe infinitary series over idempotent ordered totally generalized product \(\omega \)-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 \(\omega \)-valuation monoids we provide algorithms that given a weighted B\"{u}chi automaton and a weighted \(LTL\) formula in these fragments, decide whether the behavior of the automaton coincides with the semantics of the formula.