Multi-weighted Automata and MSO Logic

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, 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 multi-weighted MSO logic. In our main results, we show that this multi-weighted MSO logic and multi-weighted auto-mata are expressively equivalent both for finite and infinite words. The translation process is effective, leading to decidability results for our multi-weighted MSO logic.

1 Introduction

Recently, multi-priced timed automata [7, 8, 26, 31] have received much attention for real-time systems. These automata extend priced timed automata by featuring several price parameters. This permits to compute objectives like the optimal ratio between rewards and costs [7, 8], or the optimal consumption of several resources where more than one resource must be restricted [31]. Arising from the model of timed automata, the multi-weighted setting has also attracted much notice for classical non-deterministic automata [2, 4, 23, 27].

The goal of the present paper is to develop a multi-weighted monadic second order (MSO) logic and to show that it is expressively equivalent to multi-weighted automata.

Büchi’s and Elgot’s fundamental theorems [9, 22] established the expressive equivalence of finite automata and MSO logic. Weighted MSO logic with weights taken from an arbitrary semiring was introduced in [13, 14] and it was shown that a fragment of this weighted logic and semiring-weighted automata on finite and infinite words have the same expressive power [13]. Chatterjee, Doyen, and Henzinger [11, 12] investigated weighted automata modeling the average and long-time behavior of systems. The behavior of such automata cannot be described directly by semiring-weighted automata. In [17], valuation monoids were presented to model the quantitative behaviors of these automata. Their logical characterization was given in [17]. In this paper, we establish, both for finite and infinite words, the Büchi-type result for multi-weighted automata; these do not fit into the framework of other weighted automata like semiring automata [3, 15, 21, 29, 30, 36], or even valuation monoid automata [17].

The contributions of this paper are the following.

• We develop a general model for multi-weighted automata which incorporates several multi-weighted settings from the literature [2, 4, 7, 8, 23, 26, 27, 31] as well as weighted automata over semirings and valuation monoids. In the latter automata, the behavior is defined by taking the sum of the weights of runs. However, an interesting different automaton model arises by defining the behavior by taking the average over the weights of all paths. This model is outside the scope of weighted automata over semirings and valuation monoids and seems to be new in the literature. We show that our general model covers this case as well. As opposed to the model presented in the preliminary version [18], here we do not put any additional conditions on our algebraic structure and we process the transition weights in a general way, e.g., by evaluating finite multisets of strings of weights.

• The ratio measure was considered in [4, 7, 8, 27]. Here we study several algorithmic problems for ratio automata on finite words. We show that the threshold problem for them is decidable in polynomial time (this result extends the result of [27]). We also show that the behavior of ratio automata on a given word is computable in polynomial time (like in the case of, e.g., the tropical semiring or the semiring of natural numbers).

• Next, we define a multi-weighted MSO logic by extending the classical MSO logic with constants which could be tuples of weights. The semantics of formulas should be single weights (not tuples of weights). Differently from weighted MSO logics over semirings or valuation monoids, this makes it impossible to define the semantics inductively on the structure of an MSO formula. Instead, for finite words, we introduce an intermediate semantics which maps each word to a finite multiset containing strings of tuples of weights. The semantics of a formula is then defined by applying to the multiset semantics an operator which evaluates a multiset to a single value. We show that our new approach to multi-weighted MSO logic extends the semiring-weighted MSO logic of [13].

• We characterize multi-weighted automata by a fragment of our multi-weighted MSO logic. Here, in general, the fragment proposed by [13] for semirings is more expressive than multi-weighted automata. We put additional restrictions on the syntax and show the equivalence of this restricted logic and multi-weighted automata. The proof of this result can be reduced to the case of semirings. However, we cannot apply directly the result of [13], since we must pay attention to the weight constants which appear in weighted automata. Therefore, we revisit the proof of [13] with respect to the suitable constructions.

• We also show that if we add suitable properties to our algebraic weight structure, the fragment of [13] proposed for semirings also leads to quantitative languages recognizable by multi-weighted automata. Semirings as well as various weight measures considered in literature satisfy this property.

• We extend the results obtained to the setting of infinite words. Here, we introduce a model of multi-weighted Büchi automata as well as multi-weighted MSO logic, and we establish a Büchi-like equivalence result for them.

All our automata constructions are effective. Thus, decision problems for multi-weighted logic can be reduced to decision problems of multi-weighted automata. Some of these problems for multi-weighted automata can be solved whereas for others the details still have to be explored.

2 Multi-weighted Automata on Finite Words and Decidability Problems

The model of multi-weighted (or multi-priced) automata is an extension of the model of weighted automata over semirings [3, 15, 21, 29, 30, 36] and valuation monoids [17] by featuring several price parameters. In the literature, different situations of the behaviors of multi-weighted automata have been considered (cf. [2, 4, 7, 8, 23, 26, 27, 31]) to model the consumption of several resources. For instance, the model of multi-priced timed automata introduced in [7] permits to describe the optimal ratio between accumulated rewards and accumulated costs of transitions. In this section, we introduce a general model to describe the behaviors of multi-weighted automata on finite words.

The motivation for a new framework is the following. The existing concepts of semirings and valuation monoids do not cover the multi-weighted case since the weight constants in a multi-weighted automaton are tuples of weights (e.g., the reward-cost pair) whereas the behavior takes on a single value (e.g., the reward-cost ratio). Then, the weight of a run in a multi-weighted automaton cannot be defined by means of a monoidal operation (like in a semiring) or by means of a valuation function (like in a valuation monoid).

In our framework, we process the transition weights in a general way, i.e., we take into account all the history of weights and the nondeterminism before we evaluate the behavior on a given word. This means that we collect the strings of weights occurred along runs in a multiset. After that, we use an aggregation function Φ which associates to such a multiset a single value. Now we turn to formal definitions.

An alphabet is a non-empty finite set. Let Σ be a non-empty set (not necessarily finite). A finite word over Σ is a finite sequence w = a ₁...a _n where n ≥ 0 and a _i ∈ Σ for all i ∈ {1,...,n}. If n = 0, then we say that the word w is empty and denote it by ε. Otherwise, we say that w is non-empty. Let |w| = n, the length of w. We denote by Σ^∗ the set of all finite words over Σ. Let Σ⁺ = Σ^∗ ∖ {ε}, the set of all non-empty words over Σ. Any set $\mathcal L \subseteq {\Sigma }^{+}$ is called a language over Σ. Note that we eliminate the empty word ε when considering languages of finite words.

We let $\mathbb N = \{0,1,2, ...\}$, the set of nonnegative integers. Let X be a set. A multiset over X is a mapping $\mu : X \to \mathbb N$. For any multiset μ over X, the support of μ is the set s u p p(μ) = {x ∈ X | μ(x) ≠ 0}. We say that μ is finite if s u p p(μ) is a finite set. The set of all finite multisets over X is denoted by $\mathbb N \langle X \rangle$. For u ∈ X, let $[u] \in \mathbb N \langle X \rangle$ denote the finite multiset such that supp([u]) = {u} and [u](u) = 1. Let Y be a set, f : X → Y a mapping and X ^′ ⊆ X a finite subset of X. We denote by $f[X^{\prime }] \in \mathbb N \langle Y \rangle$ the multiset such that f[X ^′](y) = |{x ∈ X ^′ | f(x) = y}| for all y ∈ Y.

Now we introduce an algebraic structure for multi-weighted automata.

Definition 1

An evaluator is a structure $\mathbb E = (M, K, {\Phi })$ where M, K are non-empty sets and ${\Phi }: \mathbb N \langle M^{*} \rangle \to K$ is an aggregation function.

Note that in Definition 1 we do not put any conditions on the aggregation function Φ.

Definition 2

Let Σ be an alphabet and $\mathbb E = (M, K, {\Phi })$ an evaluator. A multi-weighted automaton over Σ and $\mathbb E$ is a tuple $\mathcal A = (Q, I, T, F, \mathrm{wt})$ where Q is a finite set of states, I ⊆ Q is a set of initial states, T ⊆ Q × Σ × Q is a set of transitions, F ⊆ Q is a set of final states, and w t : T → M is a transition weight function.

Note that the framework of evaluators also permits to handle the situations where the elements of M are not necessarily tuples of weights and the elements of K are not necessarily single values. Nevertheless, we will call all models of weighted automata which fit into our framework multi-weighted, since the multi-weighted setting is the original motivation of our framework.

Let $\mathcal A$ be a multi-weighted automaton over Σ and $\mathbb E$. Let $\text {\sc Const}(\mathcal A) = \mathrm{wt}(T) \subseteq M$ the set of all weight constants of $\mathcal A$. An accepting run (or simply run) of $\mathcal A$ is a sequence $\rho = q_{0} \xrightarrow {a_{1}} q_{1} \xrightarrow {a_{2}} ... \xrightarrow {a_{n}} q_{n}$ such that n>1, q ₀ ∈ I, t _i := (q _i−1, a _i , q _i ) ∈ T for all 1 ≤ i ≤ n, and q _n ∈ F. The finite word l a b e l(ρ) := a ₁...a _n ∈ Σ⁺ is called the label of ρ. Let $\mathrm{Run}_{\mathcal A}$ denote the set of all accepting runs of $\mathcal A$. For any w ∈ Σ⁺, let ${\mathrm{Run}_{\mathcal A}(w) = \{\rho \in \mathrm{Run}_{\mathcal A} \; | \; \mathrm{label}(\rho ) = w\}}$.

We define the mapping $\mathrm{wt}^{\#}_{\mathcal A}: Run_{\mathcal A} \to M^{*}$ as follows. For each run ${\rho = t_{1} ... t_{n} \in Run_{\mathcal A}}$ with n ≥ 1 and t ₁,...,t _n ∈ T, we put ${\mathrm{wt}^{\#}_{\mathcal A}(\rho ) = \mathrm{wt}(t_{1}) ... \mathrm{wt}(t_{n}) \in M^{*}}$. Recall that, for any finite subset $X \subseteq Run_{\mathcal A}$, we have $\mathrm{wt}^{\#}_{\mathcal A}[X] \in \mathbb N \langle M^{*} \rangle$. Then, the behavior of $\mathcal A$ is the mapping $[\![\mathcal A]\!]: {\Sigma }^{+} \to K$ defined for all w ∈ Σ⁺ by $[\![\mathcal A]\!](w) = {\Phi }(\mathrm{wt}^{\#}_{\mathcal A}[\mathrm{Run}_{\mathcal A}(w)])$. A mapping $\mathbb L: {\Sigma }^{+} \to K$ is called a quantitative language. We say that $\mathbb L$ is recognizable over $\mathbb E$ if there exists a multi-weighted automaton $\mathcal A$ over Σ and $\mathbb E$ such that $[\![\mathcal A]\!] = \mathbb L$.

Since we ignore the empty word, it suffices to define Φ only on finite multisets containing only non-empty strings of the same length. However, the use of $\mathbb N \langle M^{*} \rangle$ will simplify our further considerations.

Now we consider several examples how to describe the behavior of weighted and multi-weighted automata known from the literature using evaluators.

Example 1

The model of double-weighted reward-cost ratio automata (cf. [4, 7, 8, 27, 28]) can be described by means of the evaluator ${\mathbb E^{\text {\sc Ratio}} = (M, \mathbb Q \cup \{\infty \}, {\Phi }^{\text {\sc Ratio}})}$. Here, $M = \mathbb Q \times \mathbb Q_{\ge 0}$ and Φ^Ratio is defined for every $\mu \in \mathbb N \langle M^{*} \rangle$ as ${{\Phi }^{\text {\sc Ratio}}(\mu ) = \min \left \{\textstyle {\frac {r_{1} + ... + r_{k}}{c_{1} + ... + c_{k}}} \; \big | \; (r_{1}, c_{1}) ... (r_{k}, c_{k}) \in \mathrm{supp}(\mu ) \right \}}$ where we put $\sum (\emptyset ) = 0$ and $\frac {r}{0} = \infty$ for all $r \in \mathbb Q$. Then in a multi-weighted automaton $\mathcal A$ over Σ and $\mathbb E^{\text {\sc Ratio}}$, transitions have a reward and a cost, and $[\![\mathcal A]\!](w)$ is the minimal ratio between the total reward and the total cost of a run for w.

Example 2

Now we consider model of double-priced automata with the optimal conditional reachability objective [31] (cf. also the multi-constraint routing problem [33]). Here, the first price parameter is called the primary cost and the second price parameter is called the secondary cost. The goal is to minimize the accumulated primary cost under some upper bound on the accumulated secondary cost. Since this objective is similar to the objective of the well known knapsack problem, we will call these automata knapsack automata. We define the evaluator for knapsack automata as follows. Let $\eta \in \mathbb Q_{\ge 0}$ be a secondary cost bound. Then, consider ${\mathbb E^{\text {\sc Knap}(\eta )} = (M, \mathbb Q \cup \{\infty \}, {\Phi }^{\text {\sc Knap}(\eta )})}$ where $M = \mathbb Q \times \mathbb Q$ and Φ^Knap(η) is defined for all $\mu \in \mathbb N \langle M^{*} \rangle$ by ${{\Phi }^{\text {\sc Knap}(\eta )}(\mu ) = \min \left \{\textstyle {{\sum }_{i = 1}^{k}} x_{i} \; | \; (x_{1}, y_{1}) ... (x_{k}, y_{k}) \in \mathrm{supp}(\mu ) \wedge \textstyle {{\sum }_{i = 1}^{k}} y_{i} \le \eta \right \}},$ with min∅ = ∞.

Example 3

Here, we consider the model of multi-weighted automata with discounting. In this model, there are two weight parameters: the cost and the discounting factor (which is not fixed and depends on a transition). This situation was considered in [1] (cf. also the models of weighted automata [11, 12, 16] and weighted timed automata [24, 25] with the fixed discounting factor). A discounting automaton can be considered as a multi-weighted automaton over the evaluator ${\mathbb E^{\text {\sc Disc}} = (M, \mathbb Q \cup \{\infty \}, {\Phi }^{\text {\sc Disc}})}$ with ${M = \mathbb Q \times (\mathbb Q \cap (0,1])}$ where Φ^Disc is defined by ${{\Phi }^{\text {\sc Disc}}(\mu ) = \min \left \{ {\textstyle {\sum }_{i = 1}^{k} c_{i} \cdot {\prod }_{j = 1}^{i-1} d_{j}} \; \big | \; (c_{1}, d_{1}) ... (c_{k}, d_{k}) \in \mathrm{supp}(\mu ) \right \}}$ for all ${\mu \in \mathbb N \langle M^{*} \rangle }$. Here, $\sum (\emptyset ) = \infty$ and $\prod (\emptyset ) = 1$.

Example 4

The following quantitative automaton model seems to be new. In weighted automata over semirings [15] and valuation monoids [17], the behavior is defined by summing up the weights of accepting runs. However, it could be interesting to define the behavior by taking the average of the weights of all runs. This average measure could be useful in cases when we take into account not only the weights of runs but also how often these weights may occur. This average setting can be describe by means of the evaluator ${\mathbb E^{\text {\sc Avg}} = (\mathbb Q, \mathbb Q \cup \{\infty \}, {\Phi }^{\text {\sc Avg}})}$ where the aggregation function Φ^Avg is defined for all $\mu \in \mathbb N \langle \mathbb Q^{*} \rangle$ by ${{\Phi }^{\text {\sc Avg}}(\mu ) = \frac {1}{|\mu |} \cdot \sum (\mu (u) \cdot (x_{1} + ... + x_{k}) \; | \; u := x_{1} ... x_{k} \in \mathrm{supp}(\mu ))}$ where we put $\frac {r}{0} = \infty$ for all $r \in \mathbb Q$. Here, $|\mu | = \sum (\mu (u) \; | \; u \in \mathrm{supp}(\mu ))$ is the size of μ.

Example 5

This example is, to the best of our knowledge, new in this context. However, a similar concept might have been considered in different settings. Let $M = \mathbb R^{n}$ for some n ≥ 1 and $K = \mathbb R_{\ge 0} \cup \{\infty \}$. Consider the evaluator $\mathbb E^{\text {\sc Disp}(n)} = (M, K, {\Phi }^{\text {\sc Disp}(n)})$ where ${\Phi }^{\text {\sc Disp}(n)}: \mathbb N \langle M^{*} \rangle \to K$ is defined as follows. For v ₁, v ₂ ∈ M, let (v ₁ + v ₂) ∈ M be the componentwise sum of vectors. For a vector v = (v ₁,...,v _n ) ∈ M, let $||v|| = \sqrt {{v_{1}^{2}} + ... + {v_{n}^{2}}}$, the length of v. Then, for every $\mu \in \mathbb N \langle M^{*} \rangle$, we put

$${\Phi}^{\text{\sc Disp}(n)}(\mu) = \frac{1}{|\mu|} \cdot \sum \left( \mu(u) \cdot ||v_{1} + ... + v_{k}|| \; | \; u := v_{1} ... v_{k} \in \mathrm{supp}(\mu) \right) $$

where $\frac {r}{0} = \infty$ for all $r \in \mathbb R$. Suppose that $\mathcal A$ controls the movement of some object in $\mathbb R^{n}$ and each transition carries the coordinates of the displacement vector of this object. Then, the behavior of $\mathcal {A}$ is the value of the average displacement of the object after executing w.

Example 6

Semiring-weighted automata (cf. [15] for surveys) also fit into the framework of evaluators. Given a semiring $\mathbb S = (S, +, \cdot, 0, 1)$, a weighted automaton over $\mathbb S$ can be considered as a multi-weighted automaton over the evaluator $\mathbb E^{\mathbb S} = (S, S, {\Phi }^{\mathbb S})$ where the aggregation function ${\Phi }^{\mathbb S}$ is defined as follows. For any multiset $\mu \in \mathbb N \langle S^{*} \rangle$, we put ${\Phi }^{\mathbb S}(\mu ) = \sum \left (\mu (u) \cdot {\prod }_{j = 1}^{k} s_{j} \; | \; u := s_{1} ... s_{k} \in \mathrm{supp}(\mu ) \right ),$ where, $\sum (\emptyset ) = 0$, $\prod (\emptyset ) = 1$ and n⋅s = s+...+s (n summands) for $n \in \mathbb N$, s ∈ S.

Example 7

A valuation monoid is a tuple $\mathbb M = (M, +, val, 0)$ where $(M, +, 0)$ is a commutative monoid and val : M ⁺→M is a valuation function with ${\mathrm{val}(m_{1}, ..., m_{n}) = 0}$ whenever $m_{i} = 0$ for some i ∈ {1,..., n}. Weighted automata over valuation monoids were considered in [17]. We can understand each weighted automaton over $\mathbb M$ as a multi-weighted automaton over $\mathbb E^{\mathbb M} = (M, M, {\Phi }^{\mathbb M})$ where the aggregation function ${\Phi }^{\mathbb M}$ is defined for each finite multiset $\mu \in \mathbb N \langle M^{*} \rangle$ by ${{\Phi }^{\mathbb M}(\mu ) = \sum (\mu (u) \cdot val(m_{1}, ..., m_{k}) \; | \; u := m_{1} ... m_{k} \in mathrm{supp}(\mu )).}$ Here, v a l(ε) is defined arbitrarily.

Remark 1

Note that our model of evaluating multi-weighted automata using aggregation functions is very general. Indeed, given an alphabet Σ and a non-empty set K, for every quantitative language $\mathbb L: {\Sigma }^{+} \to K$ (even not computable) there exists an evaluator $\mathbb E^{\mathbb L}$ such that $\mathbb L$ is recognizable over $\mathbb E^{\mathbb L}$. For this, fix k ₀ ∈ K and let $\mathbb E^{\mathbb L} = ({\Sigma }, K, {\Phi }^{\mathbb L})$ where ${{\Phi }^{\mathbb L}: \mathbb N \langle {\Sigma }^{*} \rangle \to K}$ is defined for all $\mu \in \mathbb N \langle M^{*} \rangle$ by ${\Phi }^{\mathbb L}(\mu ) = \mathbb L(w)$ if μ = [w] for some w ∈ Σ⁺ and ${\Phi }^{\mathbb L}(\mu ) = k_{0}$ otherwise. Consider the multi-weighted automaton $\mathcal A = (\{1\}, \{1\}, \{1\} \times {\Sigma } \times \{1\}, \{1\}, \mathrm{wt})$ over Σ and $\mathbb E^{\mathbb L}$ such that w t((1,a,1)) = a for all a ∈ Σ. It is straightforward to see that $\mathrm{wt}_{\mathcal A}^{\#}(Run_{\mathcal A}(w)) = [w]$ for all w ∈ Σ⁺ and hence $[\![\mathcal A]\!] = \mathbb L$. Then $\mathbb L$ is recognizable over $\mathbb E^{\mathbb L}$.

The generality of our framework is motivated by the fact that it reflects the overall idea of computations in multi-weighted automata and does not appeal to concrete properties of concrete multi-weighted settings. Moreover, as we will see later in this paper, the use of our framework in the context of multi-weighted MSO logic permits to show its close relationship to the setting of semirings. In real word examples the aggregation function should be concretely given and certainly should be computable.

As mentioned before, the goal of this paper is to give a logical characterization of multi-weighted automata, i.e., we will develop a logical formalism for the multi-weighted properties and an effective translation into multi-weighted automata. As a motivation for our new logic, we consider in the rest of this section several algorithmic problems for multi-weighted automata which can be carried over to the logic.

Let $\mathcal A = (Q^{\prime }, I, T, F, \mathrm{wt})$ be a reward-cost ratio automaton over an alphabet Σ. For every transition t ∈ T, assume that w t _t = (r _t , c _t ). For a run $\rho = t_{1} ... t_{n} \in Run_{\mathcal A}$ with t ₁,...,t _n ∈ T, we let $\text {\sc Cost}(\rho ) = {\sum }_{i = 1}^{n} c_{t_{i}}$ and $\text {\sc Reward}(\rho ) = {\sum }_{i = 1}^{n} r_{t_{i}}$. We start with the following technical lemma.

Lemma 1

Let $\mathcal A = (Q, I, T, F, \mathrm{wt})$ be a reward-cost ratio automaton over an alphabet Σ. Then there exists a reward-cost ratio automaton $\mathcal A^{\prime } = (Q^{\prime }, I^{\prime }, T^{\prime }, F^{\prime }, \mathrm{wt}^{\prime })$ over Σ such that $[\![\mathcal A^{\prime }]\!] = [\![\mathcal A]\!]$ , |Q ^′ |=2⋅|Q| and Cost(ρ)>0 for every run $\rho \in Run_{\mathcal A^{\prime }}$.

Proof

The idea of the construction of $\mathcal A^{\prime }$ is to label each state of $\mathcal A$ with the Boolean flag whose initial value is 0 and its value is switched to 1 whenever a transition with the strictly positive cost is taken. Then, $\mathcal A^{\prime }$ accepts only such runs of $\mathcal A$ whose flags have been switched to 1. We define $\mathcal A^{\prime }$ formally as follows:

• Q ^′ = Q × {0, 1}, I ^′ = I × {0}, F ^′ = F × {1}.

• T ^′ consists of all transitions t ^′ := ((p, i),a,(q, j)) such that t := (p, a, q) ∈ T, i, j ∈ {0, 1} and one of the following conditions holds:

  • i = j = 0 and c _t = 0;

  • i = 0, j = 1 and c _t > 0;

  • i = j = 1.

  For such a transition t ^′, we let wt^′(t ^′) = wt(t).

Then, it can be easily checked that $[\![\mathcal A^{\prime }]\!] = [\![\mathcal A]\!]$ and Cost(ρ) > 0 for every run $\rho \in Run_{\mathcal A^{\prime }}$. □

Using Lemma 1 and a straightforward extension of the proof of Theorem 3 of [27], we obtain:

Lemma 2

Let $\mathbb E^{\text {\sc Ratio}}$ be the evaluator of Example 1, ⋈∈{<, ≤} and $\theta \in \mathbb Q$ a threshold. Then, it is decidable in polynomial time, given an alphabet Σ and a reward-cost ratio automaton $\mathcal A$ over Σ, whether there exists a word w ∈ Σ ⁺ such that $[\![\mathcal A]\!](w) \bowtie \theta$.

Now we turn to the problem of evaluation of the behavior of reward-cost ratio automata on an input word. Note that, for instance, for the tropical semiring, the behavior of a weighted automaton can be evaluated efficiently (in polynomial time) by matrix multiplications. The distributivity property of the tropical semiring is crucial for this method. In the case of ratio automata, we do not have distributivity and the method of matrix multiplications is not applicable. Note that, for a given word, there can be exponentially many runs. Hence, the naive algorithm which computes the weights of all runs is an exponential time algorithm. Interestingly, we can still evaluate the behavior of ratio automata in polynomial time.

Lemma 3

Given an alphabet Σ, a reward-cost ratio automaton $\mathcal A$ over Σ and a word w∈Σ ⁺ , the value $[\![\mathcal A]\!](w)$ can be computed in polynomial time.

Proof

Our algorithm will be based on the idea of the minimization of rational functions presented in [32]. By Lemma 1, we may assume that, for the reward-cost ratio automaton $\mathcal A = (Q, I, T, F, \mathrm{wt})$, we have: Cost(ρ) > 0 for all $\rho \in Run_{\mathcal A}(w)$. In order to avoid confusion, we denote the behavior of $\mathcal A$ by $[\![\mathcal A]\!]^{\text {\sc Ratio}}$.

First, using the product of Boolean matrices, we can check in time O(|Q|²⋅|w|) whether $Run_{\mathcal A}(w) = \emptyset$. In this case, ${[\![\mathcal A]\!]^{\text {\sc Ratio}}(w) = \infty }$. Now assume that $Run_{\mathcal A}(w) \neq \emptyset$. Then, for ${\theta = [\![\mathcal A]\!]^{\text {\sc Ratio}}(w) = \min \limits _{\rho \in Run_{\mathcal A}(w)} \frac {\text {\sc Reward}(\rho )}{\text {\sc Cost}(\rho )}}$, we have $\min \limits _{\rho \in Run_{\mathcal A}(w)} \frac {\text {\sc Reward}(\rho ) - \theta \cdot \text {\sc Cost}(\rho )}{\text {\sc Cost}(\rho )} = 0.$ Let $\varphi : \mathbb Q \to \mathbb Q$ be defined for all $x \in \mathbb Q$ by

$$\varphi(x) = \min\limits_{\rho \in Run_{\mathcal A}(w)} (\text{\sc Reward}(\rho) - x \cdot \text{\sc Cost}(\rho)) $$

Note that the equation φ(x) = 0 has the unique solution 𝜃. Then, our task of computing $[\![\mathcal A]\!]^{\text {\sc Ratio}}(w)$ is equivalent to the task of finding this solution.

First, we mention an interesting property of the mapping φ. Let $x \in \mathbb Q$ be such that φ(x) > 0. Then, for any run $\rho \in Run_{\mathcal A}(w)$, we have: $\frac {\text {\sc Reward}(\rho )}{\text {\sc Cost}(\rho )} > x$ and hence 𝜃 > x. Now assume that φ(x) < 0. Then, there exists a run $\pi \in Run_{\mathcal A}(w)$ such that Reward(π)−x ⋅ Cost(π) < 0 which implies $\theta \le \frac {\text {\sc Reward}(\pi )}{\text {\sc Cost}(\pi )} < x$. Hence, the following holds true:

$$ \forall x \in \mathbb Q: ((\varphi(x) > 0 \to \theta > x) \wedge (\varphi(x) < 0 \to \theta < x)). $$

(1)

Let $x \in \mathbb Q$ be a parameter. We consider the semiring-weighted automaton ${\mathcal A^{\prime }(x) = (Q, I, T, F, \mathrm{wt}^{\prime }(x))}$ over Σ and the tropical semiring $\text {\sc Trop} = (\mathbb Q \cup \{\infty \}, \min , +, \infty , 0)$ of rational numbers where $\mathrm{wt}^{\prime }(x): T \to \mathbb Q$ is defined as follows. For any t ∈ T with w t(t) = (r, c), we put w t ^′(x)(t) = r − x ⋅ c. We denote the behavior of $\mathcal A^{\prime }(x)$ by $[\![\mathcal A^{\prime }(x)]\!]^{\text {\sc Trop}}$. Clearly, $[\![\mathcal A^{\prime }(x)]\!]^{\text {\sc Trop}}(w) = \varphi (x)$. Then, our task is to find $x \in \mathbb Q$ with ${[\![\mathcal A^{\prime }(x)]\!]^{\text {\sc Trop}}(w) = 0}$.

Fix a enumeration (q _i )_{1 ≤ i ≤ |Q|} of Q and consider a matrix representation (γ, μ(x), ν) of $\mathcal A^{\prime }(x)$ defined as follows.

• Let γ = (γ ₁,...,γ _|Q|) ∈ {0, ∞}^1×|Q| be the row vector defined for all i ∈ {1,...,|Q|} by $\gamma _{i} = \left \{\begin {array}{ll} 0, & \text {if}\, q_{i} \in I, \\ \infty , & \text {otherwise}. \end {array}\right .$

• Let $\mu (x): {\Sigma } \to (\mathbb Q \cup \{\infty \})^{|Q| \times |Q|}$ map every letter a ∈ Σ into the square matrix μ(x)(a) = (m _{i j} )_{1 ≤ i, j ≤ |Q|} with

  $$m_{ij} = \left\{\begin{array}{lll} \mathrm{wt}^{\prime}(x)(q_{i}, a, q_{j}), & \text{if}\, (q_{i}, a, q_{j}) \in T, \\ \infty, & \text{otherwise} \end{array}\right.$$

  for all i, j ∈ {1,...,|Q|}.

• Let ν = (ν ₁,...,ν _|Q|)^T∈{0,∞}^|Q|×1 be the column vector defined for all i ∈ {1,...,|Q|} by $\nu _{i} = \left \{\begin {array}{lll} 0, & \text {if} q_{i} \in F, \\ \infty , & \text {otherwise}. \end {array}\right .$

Let w = a ₁...a _|w|. It is known from the theory of weighted automata (cf., e.g., [15]) that

$$ [\![\mathcal A^{\prime}(x)]\!]^{\text{\sc Trop}}(w) = \gamma \cdot [\mu(x)(a_{1})] \cdot ... \cdot [\mu(x)(a_{|w|})] \cdot \nu $$

(2)

where the product ⋅ of matrices is defined with respect to the semiring Trop. Then, for a fixed $\overline {x} \in \mathbb Q$, $[\![\mathcal A^{\prime }(\overline {x})]\!]^{\text {\sc Trop}}(w)$ can be computed using O(|Q|²⋅|w|) additions and O(|Q|²⋅|w|) comparisons of rational numbers.

Our goal is to compute $\varphi (\theta ) = [\![\mathcal A^{\prime }(\theta )]\!]^{\text {\sc Trop}}$ (where 𝜃 is unknown and will be considered as parameter) and to solve the equation φ(𝜃) = 0. The basic idea of our parametric computation relies on the fact that $\varphi : \mathbb Q \to \mathbb Q$ is a piecewise linear function, i.e., in some neighborhood $\mathcal I$ of 𝜃 (i.e., $\{\theta \} \subseteq \mathcal I \subseteq \mathbb Q$) it is of the form φ(x) = a−b⋅x for some $a, b \in \mathbb Q$. Then, since 𝜃 is the unique solution of φ(x) = 0, we have b ≠ 0 and $\theta = \frac {a}{b}$, and we are done.

Using Eq. 2, we will compute $[\![\mathcal A^{\prime }(x)]\!]^{\text {\sc Trop}}(w)$ with parameter x whose value is taken from some neighborhood $\mathcal I$ of 𝜃. Note that the entries of γ, μ(x)(a ₁), ..., μ(x)(a _|w|) and ν either can be considered as linear functions of the form a−b⋅x with $a, b \in \mathbb Q$ or they are the infinity symbol ∞. We denote a linear function of the form a−b⋅x where $a, b \in \mathbb Q$ and x is a variable by ℓ _{a, b} (x).

It remains to show how to implement the operations + and min of the tropical semiring for the linear functions ℓ _{a, b} (x) and ∞. First, we show how to implement + . Let $a_{1}, b_{1}, a_{2}, b_{2} \in \mathbb Q$.

• We let $\ell _{a_{1}, b_{1}}(x) + \infty = \infty + \ell _{a_{1}, b_{1}}(x) = \infty$, since, for every fixed $\overline {x} \in \mathbb Q$, $\ell _{a_{1}, b_{1}}(\overline {x}) \in \mathbb Q$ and, in the semiring Trop, we have r + ∞ = ∞ + r = ∞ for all $r \in \mathbb Q$.

• We let $\ell _{a_{1}, b_{1}}(x) + \ell _{a_{2}, b_{2}}(x) = \ell _{a_{1} + a_{2}, b_{1} + b_{2}}(x)$. Indeed, for every fixed $\overline {x} \in \mathbb Q$, we have $\ell _{a_{1}, b_{1}}(\overline {x}) + \ell _{a_{2}, b_{2}}(\overline {x}) = (a_{1} - b_{1} \cdot \overline {x}) + (a_{2} - b_{2} \cdot \overline {x}) = (a_{1} + a_{2}) - (b_{1} + b_{2}) \cdot \overline {x} = \ell _{a_{1} + a_{2}, b_{1} + b_{2}}(\overline {x})$.

The most interesting and complicated part of the proof is the implementation of the minimum operation for linear functions. The main difficulty is that the pointwise minimum of two linear parametric expressions can be a piecewise linear function. However, for our purpose it is enough to compute the minimum in some neighborhood of 𝜃. Note that, by Eq. 1, given a point $\overline {x} \in \mathbb Q$, the computation of $\varphi (\overline {x})$ gives us the following information about the location of 𝜃.

• If $\varphi (\overline {x}) = 0$, then $[\![\mathcal A]\!]^{\text {\sc Ratio}}(w) = \theta = \overline {x}$ and 𝜃 is found. So we stop the computation.

• If $\varphi (\overline {x}) > 0$, then 𝜃 is located in the interval $(\overline {x}, \infty )$.

• If $\varphi (\overline {x}) < 0$, then 𝜃 is located in the interval $(-\infty , \overline {x})$.

Based on this, after computing $\varphi (\overline {x})$ we can refine the neighborhood of 𝜃. We will use this refinement technique for the computation of the minimum of two linear parametric expressions in some neighborhood of 𝜃.

Note that, for all $a, b \in \mathbb Q$ and each value of the parameter x, we have: min(∞, ℓ _{a, b} (x))= min(ℓ _{a, b} (x),∞) = ℓ _{a, b} (x) and min(ℓ _{a, b} (x),ℓ _{a, b} (x)) = ℓ _{a, b} (x). Suppose now that $f= \ell _{a_{1},b_{1}}(x)$ and $g = \ell _{a_{2}, b_{2}}(x)$ be two distinct linear functions and that we know that 𝜃 is contained in some neighborhood $\mathcal I = (u, v)$ with −∞ ≤ u < 𝜃 < v ≤ ∞. Then, we refine the neighborhood $\mathcal I^{\prime }$ of 𝜃 and compute the minimum $\min _{\mathcal I^{\prime }}(f, g)$ in the new neighborhood $\mathcal I^{\prime }$ as follows. We distinguish the following cases (a) - (d). The ideas of these cases are depicted in Fig. 1 (in the cases (a) - (c), $\min _{\mathcal I^{\prime }}(f, g)$ is denoted by the thick line)

• (a) Assume that f and g do not have a crossing point in $\mathcal I$. Then, one of the lines f(x) and g(x) is strictly higher than the other in the neighborhood $\mathcal I$ and there is no need to refine $\mathcal I$. Then we let $\mathcal I^{\prime } = \mathcal I$, fix a point $\overline {y} \in \mathcal I^{\prime }$ and let $\min _{\mathcal I^{\prime }}(f, g) = \left \{\begin {array}{lll} f, & \text {if} a_{1} - b_{1} \cdot \overline {y} < a_{2} - b_{2} \cdot \overline {y}, \\ g, & \text {otherwise}. \end {array}\right .$

• (b) Assume that f and g have the crossing point $\overline {x} \in \mathcal I$ and $\varphi (\overline {x}) > 0$. Then, 𝜃 is located in the interval $\mathcal I \cap (\overline {x}, \infty )$ and we put $\mathcal I^{\prime } = \mathcal I \cap (\overline {x}, \infty )$. Note that one of the lines f and g is strictly higher than the other in $\mathcal I^{\prime }$. So, we put $\min _{\mathcal I^{\prime }}(f, g) = \left \{\begin {array}{lll} f, & \text {if} b_{2} < b_{1}, \\ g, & \text {otherwise}. \end {array}\right .$

• (c) Assume that f and g have the crossing point $\overline {x} \in \mathcal I$ and $\varphi (\overline {x}) < 0$. This case is symmetric to (b). We put $\mathcal I^{\prime } = \mathcal I \cap (-\infty , \overline {x})$ and $\min _{\mathcal I^{\prime }}(f, g) = \left \{\begin {array}{lll} f, & \text {if} b_{1} < b_{2}, \\ g, & \text {otherwise}. \end {array}\right .$

• (d) Assume that f and g have the crossing point $\overline {x} \in \mathcal I$ and $\varphi (\overline {x}) = 0$. Then, $\theta = \overline {x}$. So we can return $\overline {x}$ as the value of $[\![\mathcal A]\!]^{\text {\sc Ratio}}(w)$ and stop the computation.

Fig. 1

Computation of $\mathcal I^{\prime }$ and $\min _{\mathcal I^{\prime }}(f(x), g(x))$

Then, we start with the neighborhood $\mathcal I = \mathbb Q$ and compute $[\![\mathcal A^{\prime }(x)]\!]^{\text {\sc Trop}}(w)$ using Eq. 2 where whenever we need to take the minimum of two distinct linear functions f, g, we refine the neighborhood $\mathcal I^{\prime }$ of 𝜃 and take $\min _{\mathcal I^{\prime }}(f, g)$. If the case (d) holds when computing $\min _{\mathcal I^{\prime }}(f, g)$, we return $[\![\mathcal A]\!]^{\text {\sc Ratio}}(w) = \overline {x}$. If the case (d) never happens, we obtain as the result a linear function of the form a−b⋅x. Then, we return $[\![\mathcal A]\!]^{\text {\sc Ratio}}(w) = \frac {a}{b}$ (note that, as discussed before, b ≠ 0).

Note that $[\![\mathcal A^{\prime }(x)]\!]^{\text {\sc Trop}}$ can be computed using O(|Q|²⋅|w|) additions of linear functions and O(|Q|²⋅|w|) applications of $\min _{\mathcal I^{\prime }}(f, g)$ which requires O(|Q|²⋅|w|) additions and O(|Q|²⋅|w|) comparisons of rational numbers. Then, $[\![\mathcal A]\!]^{\text {\sc Ratio}}(w)$ can be computed using O(|Q|⁴⋅|w|²) additions and O(|Q|⁴⋅|w|²) comparisons of rational numbers. If we assume that the operations with rational numbers are performed in time O(1) (e.g., the set of transition weights is constant), then $[\![\mathcal A]\!]^{\text {\sc Ratio}}(w)$ can be computed in time O(|Q|⁴⋅|w|²).

Now consider a more general case. Assume that we represent each rational number as a pair r = (p, q) where $p \in \mathbb Z$ and $q \in \mathbb N \setminus \{0\}$. We use the binary encoding of integers and define the size of r by |r|= max(⌈log|p|⌉,⌈logq⌉). Let R = maxr ∈ w t(T)∪{0}|r|. Note that all rational numbers which will occur in the computation are of size O(|Q|⁴⋅|w|²⋅|r|) (since the sum and the product of two rational numbers $r_{1}, r_{2} \in \mathbb Q$ is of size O(|r ₁|+|r ₂|). Since the sum and the product of two rational numbers $r_{1}, r_{2} \in \mathbb Q$ can be computed in time O(|r ₁|⋅|r ₂|), then $[\![\mathcal A]\!]^{\text {\sc Ratio}}(w)$ can be computed in time O(|Q|¹²⋅|w|⁶⋅|r|²). Then, our algorithm has polynomial time complexity. □

3 Multi-weighted MSO Logic on Finite Words

In this section, we wish to develop a multi-weighted MSO logic where the weight constants are elements of a set M. Again, if weight constants are pairs of a reward and a cost, we want the semantics of formulas to be able to reflect the minimal reward-cost ratio setting, so the weights of formulas should be single weights. Then, there arises a problem to define the semantics function inductively on the structure of a formula as in [13]. Therefore we proceed as follows. Given a formula, we associate to each word a multiset in $\mathbb N \langle M^{*} \rangle$. Here, for disjunction and existential quantification we use the multiset union. For conjunction and universal quantification, we extend the concatenation of strings in M ^∗ to the Cauchy product of multisets in $\mathbb N \langle M^{*} \rangle$. Then, we use an aggregation function ${\Phi }: \mathbb N \langle M^{*} \rangle$ which associates to each multiset of elements a single value (e.g. the maximal reward-cost ratio of pairs contained in a multiset).

For the rest of this section, we fix an alphabet Σ and an evaluator $\mathbb E = (M, K, {\Phi })$ where ${\Phi }: \mathbb N \langle M^{*} \rangle \to K$ is an aggregation function. We fix countable and pairwise disjoint sets V ₁ and V ₂ of first-order resp. second-order variables. The first-order variables are denoted by lower-case letters, e.g., x, y, z,... whereas the second-order variables are denoted by upper-case letters, for instance, X, Y, Z,... . Let V = V ₁∪V ₂.

The syntax of formulas of $\textbf {mwMSO}({\Sigma }, \mathbb E)$, the multi-weighted MSO logic over Σ and $\mathbb E$, is given as in [5] by the grammar

$$ \begin{array}{l@{\hspace{0.2cm}}l@{\hspace{0.2cm}}l} \beta & ::= & P_{a}(x) \; | \; x \le y \; | \; X(x) \; | \; \beta \vee \beta \; | \; \lnot \beta \; | \; \exists x. \beta \; | \; \exists X. \beta \vspace{0.1cm} \\ \varphi & ::= & \beta \; | \; m \; | \; \varphi \oplus \varphi \; | \; \varphi \otimes \varphi \; | \; {\textstyle \bigoplus} x. \varphi \; | \; {{\textstyle \bigoplus}} X. \varphi \; | \; {{\textstyle \bigotimes}} x. \varphi \end{array} $$

(3)

where a ∈ Σ, m ∈ M, x, y ∈ V ₁ and X ∈ V ₂. The formulas β are called Boolean formulas and the formulas φ are called multi-weighted formulas. Let MSO(Σ) denote the set of all Boolean formulas.

Let $\varphi \in \textbf {mwMSO}({\Sigma }, \mathbb E)$ be a formula. We will denote by Free(φ) the set of all free variables of φ, i.e., the set of those variables in φ not bound by a quantifier. Then, we say that φ is a sentence if F r e e(φ) = ∅. Let Const(φ) ⊆ M denote the set of all weight constants appearing in φ. Notice that if φ ∈ MSO(Σ), then Const(φ) = ∅.

A word w = a ₁...a _n ∈ Σ⁺ is usually represented by the relational structure (dom(w), ≤, (P _a ) _{a ∈ Σ}) where dom(w) = {1,...,n} is the domain of w and, for all letters a ∈ Σ, P _a = {i ∈ dom(w) | a _i = a}. A w-assignment σ is a function mapping first-order variables in V ₁ to elements of dom(w) and second-order variables in V ₂ to subsets of dom(w). If x ∈ V ₁ and i ∈ dom(w), then the update σ[x/i] is the w-assignment with σ[x/i](x) = i and σ[x/i](y) = σ(y) for all y ∈ V ∖ {x}. Similarly, for X ∈ V ₂ and I ⊆ dom(w), we define the update σ[X/I] to be the w-assignment with σ[X/I](X) = I and σ[X/I](y) = σ(y) for all y ∈ V ∖ {X}. We denote by ${\Sigma }_{V}^{+}$ the set of all pairs (w, σ) where w ∈ Σ⁺ and σ is a w-assignment. We notice that ${\Sigma }_{V}^{+}$ is not (Σ _V )⁺. Let $(w, \sigma ) \in {\Sigma }_{V}^{+}$ and β ∈ MSO(Σ) be a Boolean formula. The definition that (w, σ) satisfies β, denoted (w, σ) ⊧ β, is given inductively on the structure of β as usual.

Let $\mu _{1}, \mu _{2} \in \mathbb N \langle M^{*} \rangle$ be multisets. The union $(\mu _{1} \uplus \mu _{2}) \in \mathbb N \langle M^{*} \rangle$ is defined by (μ ₁⊎μ ₂)(u) = μ ₁(u) + μ ₂(u) for all u ∈ M ^∗. Clearly, the union ⊎ is a commutative operation. The Cauchy product ${(\mu _{1} \cdot \mu _{2}) \in \mathbb N \langle M^{*} \rangle }$ is defined for all u ∈ M ^∗ as

$$(\mu_{1} \cdot \mu_{2})(u) = \sum (\mu_{1}(u_{1}) \cdot \mu_{2}(u_{2}) \; | \; u_{1} \in \mathrm{supp}(\mu_{1}), u_{2} \in \mathrm{supp}(\mu_{2}), u = u_{1} u_{2}). $$

We use the Cauchy product for the semantics of multi-weighted formulas in order to reflect the concatenation of the sequences of weights. The empty multiset $\mu \in \mathbb N \langle M^{*} \rangle$ is defined as μ(u) = 0 for all u ∈ M ^∗. We will abuse the notation and denote the empty multiset by ∅. The following proposition is a folklore result.

Proposition 1

$(\mathbb N \langle M^{*} \rangle , \uplus , \cdot , \emptyset , [\varepsilon ])$ is a semiring.

We will denote the semiring from Proposition 1 also by $\mathbb N \langle M^{*} \rangle$.

Now let $\varphi \in \textbf {mwMSO}({\Sigma }, \mathbb E)$ be a multi-weighted formula. We define the semantics of φ in two steps as follows:

• First, the auxiliary semantics ${\langle \! \langle \varphi \rangle \! \rangle : {\Sigma }^{+}_{V} \to \mathbb N \langle M^{*} \rangle }$ is defined for all ${(w, \sigma ) \in {\Sigma }^{+}_{V}}$ inductively on the structure of φ as shown in Table 1. Here, m ∈ M, β ∈ MSO(Σ), x ∈ V ₁ and X ∈ V ₂. Note that 〈φ〉 does not depend on K and Φ.

• Second, the proper semantics (or simply semantics) $[\![\varphi ]\!]: {\Sigma }^{+}_{V} \to K$ is defined for all $(w, \sigma ) \in {\Sigma }^{+}_{V}$ by [ [φ] ](w, σ) = Φ(〈φ〉(w, σ)).

Table 1 The auxiliary semantics of multi-weighted formulas

Sometimes, in order to emphasize that the semantics of a multi-weighted formula $\varphi \in \textbf {mwMSO}({\Sigma }, \mathbb E)$ is defined with respect to $\mathbb E$, we will write $[\![\varphi ]\!]^{\mathbb E}$ for [ [φ] ]. Now let $\varphi \in \textbf {mwMSO}({\Sigma }, \mathbb E)$ be a sentence. Then, for any $(w, \sigma ) \in {\Sigma }^{+}_{V}$, the value [ [φ] ](w, σ) depends only on w. Then, ignoring the values of variables, we can consider 〈 〈φ〉 〉 as the mapping $\langle \! \langle \varphi \rangle \! \rangle : {\Sigma }^{+} \to \mathbb N \langle M^{*} \rangle$ and [ [φ] ] as the mapping [ [φ] ]:Σ⁺→K. Let ${\Delta } \subseteq \textbf {mwMSO}({\Sigma }, \mathbb E)$ and $\mathbb L: {\Sigma }^{+} \to K$ a quantitative language. We say that $\mathbb L$ is Δ-definable if there exists a sentence φ ∈ Δ such that $[\![\varphi ]\!] = \mathbb L$.

Let β ∈ MSO(Σ) and $\varphi _{1}, \varphi _{2} \in \textbf {mwMSO}({\Sigma }, \mathbb E)$. Like in [6], we can define the $\textbf {mwMSO}({\Sigma }, \mathbb E)$-formula β ? (φ ₁:φ ₂) as an abbreviation for the formula (β⊗φ ₁)⊕((¬β)⊗φ ₂).

Example 8

Let A be an object on the plane whose displacement is managed by two types of commands: ⇔ and ⇕. After receiving the command ⇔ the object moves one step to the left or to the right; after receiving ⇕ one step up or down. Consider the evaluator $\mathbb E^{\text {\sc Disp}(n)}$ from Example 5 for n = 2. Let v _← = (−1, 0), v _→ = (1, 0), v _↓ = (0, −1) and v _↑ = (0, 1). Consider the following multi-weighted MSO sentence over the alphabet Σ = {⇔, ⇕} and the evaluator $\mathbb E^{\text {\sc Disp}(n)}$:

$$\varphi = {\textstyle \bigotimes} x. (P_{\leftrightarrow}(x) \, ? \, (v_{\leftarrow} \oplus v_{\rightarrow}) : (v_{\downarrow} \oplus v_{\uparrow})) $$

Then, for every sequence of commands w ∈ Σ⁺, [ [φ] ](w) is the average displacement of the object after execution of all commands from w. For instance, let w = ⇔⇔. Then, 〈φ〉(w) = [v _← v _←] ⊎ [v _← v _→] ⊎ [v _→ v _←] ⊎ [v _→ v _→] and [ [φ] ](w) = 1. For w = ⇔⇕, we have $[\![\varphi ]\!](w) = \sqrt {2}$.

Next, we discuss how our new multi-weighted MSO logic is related to the semiring-weighted logic of Droste and Gastin [13]. Let $\mathbb S = (S, +, \cdot , 0, 1)$ be a semiring. The syntax of weighted MSO logic $\textbf {wMSO}({\Sigma }, \mathbb S)$ is given by the grammar of Eq. 3 where we replace m ∈ S by s ∈ S. As opposed to the multi-weighted case, the semantics $[\![\varphi ]\!]^{\mathbb S}: {\Sigma }^{+}_{V} \to S$ of a weighted MSO formula $\varphi \in \textbf {wMSO}({\Sigma }, \mathbb S)$ was defined in one step using the weights 0, 1 for the Boolean values, the sum + for ⊕, and the product ⋅ for ⊗. More precisely, the semantics can be defined as shown in Table 1 where we replace 〈〈...〉〉 by $[\![ ... ]\!]^{\mathbb S}$, m ∈ M by s ∈ S, [m] by s, ∅ by 0, [ε] by 1, and ⊎ by +. Given a formula $\varphi \in \textbf {wMSO}({\Sigma }, \mathbb S)$, the set Const(φ) ⊆ S is defined as for mwMSO-formulas.

As we saw in Example 6, a semiring $\mathbb S$ can be considered as the evaluator ${\mathbb E^{\mathbb S} = (S, S, {\Phi }^{\mathbb S})}$. The following lemma shows that our multi-weighted MSO logic extends the semiring-weighted logic of [13].

Lemma 4

Let Σ be an alphabet, $\mathbb S$ a semiring and $\varphi \in \textbf {wMSO}({\Sigma }, \mathbb S)$ . Then, ${\varphi \in \textbf {mwMSO}({\Sigma }, \mathbb E^{\mathbb S})}$ and $[\![\varphi ]\!]^{\mathbb E_{\mathbb S}} = [\![\varphi ]\!]^{\mathbb S}$.

Assume that $\mathbb S = (S, +, \cdot , 0, 1)$. The proof of Lemma 4 follows from the following technical lemma.

Lemma 5

The mapping ${{\Phi }^{\mathbb S}: (\mathbb N \langle S^{*} \rangle , \uplus , \cdot , \emptyset , [\varepsilon ]) \to (S, +, \cdot , 0, 1)}$ is a semiring morphism with ${\Phi }^{\mathbb S}([s]) = s$ for all s∈S.

Proof

Clearly, ${\Phi }^{\mathbb S}(\emptyset ) = 0$, ${\Phi }^{\mathbb S}([\varepsilon ]) = 1$ and ${\Phi }^{\mathbb S}([s]) = s$ for all s ∈ S. Let ${\mu _{1}, \mu _{2} \in \mathbb N \langle S^{*} \rangle }$. It can be easily shown that ${\Phi }^{\mathbb S}(\mu _{1} \uplus \mu _{2}) = {\Phi }^{\mathbb S}(\mu _{1}) + {\Phi }^{\mathbb S}(\mu _{2})$. We show explicitly that ${\Phi }^{\mathbb S}(\mu _{1} \cdot \mu _{2}) = {\Phi }^{\mathbb S}(\mu _{1}) \cdot {\Phi }^{\mathbb S}(\mu _{2})$. Let $g: (S^{*}, \cdot , \varepsilon ) \to (S, \cdot , 1)$ be the monoid morphism with g(s) = s for all s ∈ S and $\mu _{1}, \mu _{2} \in \mathbb N \langle S^{*} \rangle$. Then:

$$\begin{array}{@{}rcl@{}} {\Phi}^{\mathbb S}(\mu_{1}) \cdot {\Phi}^{\mathbb S}(\mu_{2}) &=& \left( \sum\limits_{u \in S^{*}} \mu_{1}(u) \cdot g(u) \right) \cdot \left( \sum\limits_{v \in S^{*}} \mu_{2}(v) \cdot g(v) \right) \\ &=& \sum\limits_{u,v \in S^{*}} (\mu_{1}(u) \cdot \mu_{2}(v)) \cdot (g(u) g(v)) = \sum\limits_{w \in S^{*}} (\mu_{1} \cdot \mu_{2})(w) \cdot g(w) \\ &=&{\Phi}^{\mathbb S}(\mu_{1} \cdot \mu_{2}). \end{array} $$

□

The following example illustrates a situation where the use of multi-weighted MSO logic is more convenient than the use of semiring-weighted MSO logic.

Example 9

Let Σ be an alphabet and a ∈ Σ. Consider the quantitative language $\mathbb L: {\Sigma }^{+} \to \mathbb Q \cup \{\infty \}$ defined for every w ∈ Σ⁺ as ${\mathbb L(w) = 2 \cdot |w|_{a}}$ if |w| ≤ 1000 and $\mathbb L(w) = \infty$ otherwise. We can define $\mathbb L$ by means of the wMSO(Σ,Trop)-sentence $\beta \otimes {\textstyle \bigotimes } x. (P_{a}(x) \, ? \, (2 : 0))$ where Trop is the tropical semiring or rational numbers and β ∈ MSO(Σ) describes the property |w| ≤ 1000. Unfortunately, such a formula β will be very long and the use of semiring-weighted MSO logic is not convenient. Here, it is easier to use our multi-weighted MSO logic. Let η = 1000. Consider the evaluator ${\mathbb E^{\text {\sc Knap}(\eta )} = (\mathbb Q \times \mathbb Q, \mathbb Q \cup \{\infty \}, {\Phi }^{\text {\sc Knap}(\eta )})}$ as defined in Example 2. Then, $\mathbb L = [\![\varphi ]\!]$ where φ is the sentence $\varphi \in \textbf {mwMSO}({\Sigma }, \mathbb E^{\text {\sc Knap}(\eta )})$ defined as ${\varphi = {\textstyle \bigotimes } x. (P_{a}(x) \, ? \, (2, 1) : (0, 1)).}$

Next, we present a Büchi-like result of Droste and Gastin [13] for semiring-weighted MSO logic in order to compare it with our results in the sequel. Since weighted MSO logic is more powerful than weighted automata (cf. [13]), we consider a restricted version of weighted MSO logic. Let $\mathbb S = (S, +, \cdot , 0, 1)$ be a semiring. The set $\textbf {aBOOL}({\Sigma }, \mathbb S)$ of almost Boolean formulas is generated by the grammar

$$\gamma \; ::= \; \beta \; | \; s \; | \; \gamma \oplus \gamma \; | \; \gamma \otimes \gamma $$

where β ∈ MSO(Σ) and s ∈ S. For a subset X ⊆ S, let cl(X) denote the minimal subset of S which contains X∪{0, 1} and is closed under + and ⋅. For subsets X, Y ⊆ S, we say that X and Y commute elementwise, if x⋅y = y⋅x for all x ∈ X and y ∈ Y. The set ${\textbf {wMSO}}^{res}({\Sigma }, \mathbb S) \subseteq {\textbf {wMSO}}({\Sigma }, \mathbb S)$ of syntactically restricted formulas is defined by the rules

$$\varphi \; ::= \; \gamma \; | \; \varphi \oplus \varphi \; | \; \varphi \otimes \varphi^{\; (!)} \; | \; {\textstyle \bigoplus} x. \varphi \; | \; {{\textstyle \bigoplus}} X. \varphi \; | \; {{\textstyle \bigotimes}} x. \gamma $$

where $\gamma \in \textbf {aBOOL}({\Sigma }, \mathbb S)$, x ∈ V ₁ and X ∈ V ₂; moreover, there is an additional restriction at the place (!): a formula φ ₁⊗φ ₂ belongs to ${\textbf {wMSO}}^{res}({\Sigma }, \mathbb S)$ iff the sets Const(φ ₁) and Const(φ ₂) commute elementwise.

Theorem 1 (Droste, Gastin [13])

Let Σ be an alphabet, ${\mathbb S = (S, +, \cdot , 0 , 1 )}$ a semiring, and $\mathbb L \in \mathbb S \langle \! \langle {\Sigma }^{+} \rangle \! \rangle$ a quantitative language. Then, $\mathbb L \in \text {\sc Rec}({\Sigma }, \mathbb S)$ iff $\mathbb L$ is $\textbf {wMSO}^{res}({\Sigma }, \mathbb S)$ -definable.

4 Multi-weighted MSO Logic Versus Multi-weighted Automata

In this section we will compare the expressive power of multi-weighted MSO logic and multi-weighted automata. Even for the case of a semiring, weighted MSO logic is more expressive than semiring-weighted automata (cf. [13]). As we will see in the next example, if we consider the restricted fragment $\textbf {wMSO}^{res}({\Sigma }, \mathbb S)$ for multi-weighted logic, it is, in general, more expressive than multi-weighted automata.

Example 10

Here, we will consider examples of multi-weighted sentences which lead to unrecognizable quantitative languages. Let Σ be an arbitrary alphabet. Consider the evaluator $\mathbb E = (M, \mathbb N \langle M^{*} \rangle , {\Phi })$ where M is an arbitrary non-empty set and ${\Phi }: \mathbb N \langle M^{*} \rangle \to \mathbb N \langle M^{*} \rangle$ is the identity mapping. Let $\mathbb L: {\Sigma }^{+} \to \mathbb N \langle M^{*} \rangle$ be any quantitative language recognizable over $\mathbb E$. Then, for all w ∈ Σ⁺, ${\text {\sc Const}}(\mathbb L(w)) \subseteq M^{|w|}$. Based on this property, we show the unrecognizability of the semantics of the following sentences:

• Let φ = m where m ∈ M. Then, for all w ∈ Σ⁺, [ [φ] ](w) = [m]. Then, for all w ∈ Σ⁺ with |w|>1, we have: s u p p([ [φ] ](w))∩M ^|w| = ∅. Hence, the quantitative language [ [φ] ] is not recognizable. In contrast, in semiring-weighted logic of [13] the semantics of a constant is always recognizable by a semiring-weighted automaton.

• Let φ = True. Then, [ [φ] ](w) = [ε] for all w ∈ Σ⁺. Clearly, [ [φ] ] is not recognizable over $\mathbb E$. In contrast, in semiring-weighted logic of [13] the semantics of a Boolean sentence is always recognizable by a semiring-weighted automaton.

• Let $\varphi = {\textstyle \bigotimes } x. m$ where x ∈ V ₁. Then, [ [φ] ](w) = [m ^|w|] for all w ∈ Σ⁺. Clearly, [ [φ] ] is recognizable over $\mathbb E$. Note that, for all w ∈ Σ⁺, [ [φ⊗φ] ](w) = [m ^2|w|]. Then, [ [φ⊗φ] ] is not recognizable over $\mathbb E$. Here, the situation is similar to the case of semirings, since, as it was shown in [14], the use of ⊗ for noncommutative semirings may not preserve recognizability.

• Let $\varphi = {\textstyle \bigotimes } x. {\textstyle \bigotimes } y. m$ where x, y ∈ V ₁ and m ∈ M. Then, $[\![\varphi ]\!](w) = [m^{|w|^{2}}]$ for all w ∈ Σ⁺. Again, [ [φ] ] is not recognizable over $\mathbb E$. Note that in the case of semirings the nested use of the weighted first-order universal quantifier often leads to unrecognizability [13].

Hence Theorem 1 cannot be easily extended to the multi-weighted setting. Our next task is to find a restricted fragment of $\textbf {mwMSO}({\Sigma }, \mathbb E)$ which is expressively equivalent to multi-weighted automata. First, we analyze Example 10. Here, besides the standard restrictions on ⊗ and ${\textstyle \bigotimes } x$, we must pay attention to the length of the strings in the multisets of the auxiliary semantics: it must be equal to the length of an input word.

For multi-weighted MSO logic, instead of the almost Boolean fragment $\textbf {aBOOL}({\Sigma }, \mathbb E)$, we consider the fragment ${\textbf {aBOOL}}^{res}({\Sigma }, \mathbb E)$ of restricted almost boolean formulas which is defined by the grammar:

$$\gamma \; ::= \; m \; | \; \gamma \oplus \gamma \; | \; \beta \otimes \gamma. $$

Note that, for each $(w, \sigma ) \in {\Sigma }^{+}_{V}$, s u p p(〈 〈γ〉 〉(w, σ)) ⊆ M.

Then, we define the strongly restricted multi-weighted MSO logic $\textbf {mwMSO}^{\text {s.res}}({\Sigma }, \mathbb E) \subseteq \textbf {mwMSO}({\Sigma }, \mathbb E)$ over Σ and $\mathbb E$ to be the set of all formulas generated by the grammar

$$\varphi \; ::= \; {\textstyle \bigotimes} x. \gamma \; | \; \varphi \oplus \varphi \; | \; \beta \otimes \varphi \; | \; {\textstyle \bigoplus} x. \varphi \; | \; {{\textstyle \bigoplus}} X. \varphi $$

where x ∈ V ₁, X ∈ V ₂, β ∈ MSO(Σ) and $\gamma \in \textbf {aBOOL}^{res}({\Sigma }, \mathbb E)$. Note that the multi-weighted sentences from Examples 8 and 9 are strongly restricted. We call this fragment strongly restricted to avoid confusion with the definition of restricted semiring-weighted MSO logic. For a semiring $\mathbb S$, let ${\textbf {aBOOL}}^{res}({\Sigma }, \mathbb S) = {\textbf {aBOOL}}^{res}({\Sigma }, \mathbb E^{\mathbb S})$ and ${\textbf {wMSO}}^{{\text {s.res}}}({\Sigma }, \mathbb S) = {\textbf {wMSO}}^{{\text {s.res}}}({\Sigma }, \mathbb E^{\mathbb S})$

Now we state our main result about multi-weighted logic on finite words. We want to point out that here we do not put any restrictions on an evaluator $\mathbb E$ and that this result does not extend Theorem 1 to the multi-weighted case (because of the generality of our model, cf. Example 10). In Section 6, we consider evaluators with additional properties and show that multi-weighted automata over them can be characterized by the same logical fragment as in Theorem 1.

Theorem 2

Let Σ be an alphabet, $\mathbb E = (M, K, {\Phi })$ an evaluator and ${\mathbb L: {\Sigma }^{+} \to K}$ a quantitative language. Then, the following are equivalent.

• (a) $\mathbb L$ is recognizable over $\mathbb E$.

• (b) $\mathbb L$ is $\textbf {mwMSO}^{\text {s.res}}({\Sigma }, \mathbb E)$ -definable.

The proof of this theorem will be given in the rest of this section. We start with the following remark.

Remark 2

Note that the semantics [ [φ] ] of a multi-weighted formula ${\varphi \in \textbf {mwMSO}({\Sigma }, \mathbb E)}$ is defined as the composition Φ∘〈 〈φ〉 〉 where 〈 〈φ〉 〉 is the auxiliary semantics of φ. Now let $\mathcal A$ be a multi-weighted automaton over Σ and $\mathbb E$. The behavior $[\![\mathcal A]\!]$ of $\mathcal A$ can be decomposed as $[\![\mathcal A]\!] = {\Phi } \circ \langle \! \langle \mathcal A \rangle \! \rangle$ where ${\langle \! \langle \mathcal A \rangle \! \rangle : {\Sigma }^{+} \to \mathbb N \langle M^{*} \rangle }$ is defined for all w ∈ Σ⁺ by $\langle \! \langle \mathcal A \rangle \! \rangle (w) = \mathrm{wt}^{\#}_{\mathcal A}[Run_{\mathcal A}(w)].$ We call $\langle \! \langle \mathcal A \rangle \! \rangle$ the auxiliary behavior of $\mathcal A$.

Since we define the behavior of multi-weighted automata and the semantics of multi-weighted MSO logic by means of the equal aggregation function Φ, by Remark 1 it suffices to show the equivalence of multi-weighted automata and logic with respect to the auxiliary behavior and the auxiliary semantics, respectively.

Recall that the codomain of the auxiliary behavior of multi-weighted automata and the codomain of the auxiliary semantics of multi-weighted MSO logic are $\mathbb N \langle M^{*} \rangle$ whereas the weight constants are taken from M.

Our further considerations will reduce the proof of Theorem 2 to the case of the semiring $\mathbb N \langle M^{*} \rangle$. Here we will use the idea that a weight constant m ∈ M can be identified with the multiset $[m] \in \mathbb N \langle M^{*} \rangle$. Let $Mon(M) = \{[m] \; | \; m \in M \} \subseteq \mathbb N \langle M^{*} \rangle$, the set of monomials.

Lemma 6

Let $\mathbb L: {\Sigma }^{+} to \mathbb N \langle M^{*} \rangle$ be a mapping. Then:

• (a) $\mathbb L = \langle \! \langle \mathcal A \rangle \! \rangle$ for some multi-weighted automaton $\mathcal A$ over Σ and $\mathbb E$ iff $\mathbb L = [\![\mathcal A^{\prime }]\!]^{\mathbb N \langle M^{*} \rangle }$ for some semiring-weighted automaton $\mathcal A^{\prime }$ over Σ and $\mathbb N \langle M^{*} \rangle$ such that ${\text {\sc Const}}(\mathcal A^{\prime }) \subseteq \mathrm{Mon}(M)$.

• (b) $\mathbb L = \langle \! \langle \varphi \rangle \! \rangle$ for some multi-weighted sentence $\varphi \in \textbf {mwMSO}^{{\text {s.res}}}({\Sigma }, \mathbb E)$ iff $\mathbb L = [\![\varphi ^{\prime }]\!]^{\mathbb N \langle M^{*} \rangle }$ for some weighted sentence $\varphi ^{\prime } \in {\text {\sc wMSO}}^{{\text {s.res}}}({\Sigma }, \mathbb N \langle M^{*} \rangle )$ over the semiring $\mathbb N \langle M^{*} \rangle$ with Const(φ ^′) ⊆ Mon(M).

Proof

The proof follows from the fact that if we identify elements m ∈ M with the monomials [m] ∈ Mon(M), then the auxiliary behavior of a multi-weighted automaton can be computed in the same way as the behavior of a semiring-weighted automaton with respect to the semiring $\mathbb N \langle M^{\ast } \rangle$ and, similarly, the auxiliary semantics of a multi-weighted formula can be computed as the semantics of a semiring-weighted formula over the semiring $\mathbb N \langle M^{\ast } \rangle$.

To finish the proof of our Theorem 2, we show that the right hand side statements of the equivalences (a) and (b) of Lemma 6 are equivalent as well. To prove this, we cannot directly use the proof of [13] for Theorem 1 for the case $\mathbb S = \mathbb N \langle M^{*} \rangle$, since the translation from logic into automata presented in [13] employs some computations in the semiring $\mathbb S$ but the set Mon(M) is not closed under the union ⊎ and the Cauchy product ⋅.

We say that a sentence $\varphi \in \textbf {wMSO}^{\text {s.res}}({\Sigma }, \mathbb S)$ admits a constant-preserving translation if there exists a semiring-weighted automaton $\mathcal A$ over Σ and $\mathbb S$ such that $[\![\mathcal A]\!]^{\mathbb S} = [\![\varphi ]\!]^{\mathbb S}$ and ${\text {\sc Const}}(\mathcal A) \subseteq {\text {\sc Const}}(\varphi )$. Similarly, we say that a semiring-weighted automaton $\mathcal A$ over Σ and $\mathbb S$ admits a constant-preserving translation if there exists a sentence $\varphi \in {\text {\sc wMSO}}^{{\text {s.res}}}({\Sigma }, \mathbb S)$ such that $[\![\varphi ]\!]^{\mathbb S} = [\![\mathcal A]\!]^{\mathbb S}$ and ${\text {\sc Const}}(\varphi ) \subseteq {\text {\sc Const}}(\mathcal A)$. Next we show that both wMSO ^s.res-sentences and semiring-weighted automata admit constant-preserving translations. This result could be also of independent interest, e.g., for the case when the operations in a semiring $\mathbb S$ are not computable. In this situation a constant-preserving translation would be preferable.

Theorem 3

Let Σ be an alphabet and $\mathbb S$ a semiring.

(a) Every sentence $\varphi \in \textbf {wMSO}^{\text {s.res}}({\Sigma }, \mathbb S)$ admits a constant-preserving translation.

(b) Every semiring-weighted automaton $\mathcal A$ over Σ and $\mathbb S$ admits a constant-preserving translation.

We will present a proof of this theorem in the next section. Then Theorem 2 follows immediately from Theorem 3 for $\mathbb S = \mathbb N \langle M^{*} \rangle$ and Lemma 6.

5 Constant-preserving Translations

In this section, we present a proof of Theorem 3. Let $\mathbb S = (S, +, \cdot , 0, 1)$ be a semiring.

We start with part (a). For a set X ⊆ S, let c l ₊(X) ⊆ S be the minimal set containing $X \cup \{\mathbb 0\}$ which is closed under + .

Lemma 7

Let $\varphi \in \textbf {wMSO}^{\text {s.res}}({\Sigma }, \mathbb S)$ be a sentence. Then there exists a weighted automaton $\mathcal A$ over Σ and $\mathbb S$ such that $[\![\mathcal A]\!] = [\![\varphi ]\!]$ and $\text {\sc Const}(\mathcal A) \subseteq cl_{+}(\text {\sc Const}(\varphi ))$.

Proof

We proceed by induction on φ. As in the proof presented in [13], we can restrict ourselves to a finite set $\mathcal V \supseteq \mathrm{Free}(\varphi )$ of variables and encode values of variables as a word over the extended alphabet ${\Sigma \times \{0,1\}^{\mathcal V}}$. Next, we will omit the details of the proof which are analogous to the proof of [13].

• Let $\varphi = {\textstyle \bigotimes } x. \gamma$ where x ∈ V ₁ and $\gamma \in \textbf {aBOOL}^{res}({\Sigma }, \mathbb S)$. It can be easily shown by induction on the structure of a restricted almost Boolean formula $\gamma \in {text{\sc aBool}}^{res}({\Sigma }, \mathbb S)$ that ${[\![\gamma ]\!]({\Sigma }^{+}_{V}) \subseteq cl_{+}({\sc CONST}(\gamma ))}$ is a finite set. Then, we construct a weighted automaton $\mathcal A$ for φ as in [13], Lemma 4.4. Note that ${\sc CONST}(\mathcal A) \subseteq [\![\gamma ]\!]({\Sigma }^{+}_{V}) \subseteq cl_{+}({\sc CONST}(\gamma ))$.

• Let φ = φ ₁ ⊕ φ ₂. In this case, we apply the standard disjoint union construction which preserves the set of weight constants of automata for φ ₁ and φ ₂.

• Let φ = β⊗φ ^′ where β ∈ MSO(Σ). We proceed here like in the proof of [17], i.e., we take a product of a deterministic complete unweighted automaton for β and a weighted automaton for φ ^′. This construction preserves the set of weight constants of the weighted automaton for φ ^′.

• Let $\varphi = {\textstyle \bigoplus } \mathcal X. \varphi ^{\prime }$ with $\mathcal X \in V_{1} \cup V_{2}$. Here, we apply the construction for the projection of [20], Lemma 1, which preserves the constants.

Now we transform the weighted automaton $\mathcal A$ from the previous lemma into a weighted automaton $\mathcal A^{\prime }$ with $[\![\mathcal A^{\prime }]\!] = [\![\mathcal A]\!]$ and $\text {\sc Const}(\mathcal A^{\prime }) \subseteq \text {\sc Const}(\varphi )$.

Lemma 8

Let X⊆S be a finite set and $\mathcal A$ a weighted automaton over Σ and $\mathbb S$ such that $\text {\sc Const}(\mathcal A) \subseteq \mathrm{cl}_{+}(X)$ . Then, there exists a weighted automaton $\mathcal A^{\prime }$ over Σ and $\mathbb S$ such that $[\![\mathcal A^{\prime }]\!] = [\![\mathcal A]\!]$ and $\text {\sc Const}(\mathcal A^{\prime }) \subseteq X$.

Proof

Let $\mathcal A = (Q, I, T, F, \mathrm{wt})$. We may assume that T ≠ ∅. For each t ∈ T, let $\mathrm{wt}(t) = s_{t,1} + ... + s_{t, n_{t}}$ where n _t ≥ 0 and $s_{t,1}, ..., s_{t,n_{t}} \in X$. Let n = max{n _t | t ∈ T}. The key idea of our construction is to split each transition t of $\mathcal A$ into n _t transitions with the weights $s_{t,1}, ..., s_{t,n_{t}}$. We construct the weighted automaton $\mathcal A^{\prime } = (Q^{\prime }, I^{\prime }, T^{\prime }, F^{\prime }, wt^{\prime })$ over Σ and $\mathbb S$ as follows:

• Q ^′ = (Q × {1,...,n}), I ^′ = I × {1}, F ^′ = F × {1,...,n};

• T ^′ consists of all transitions t ^′ := ((p, i),a, (q, j)) where t := (p, a, q) ∈ T, i ∈ {1,...,n} and j ∈ {1,...,n _t }. We define the weight of t ^′ as wt^′(t ^′) = s _{t, j} .

Clearly, $\text {\sc Const}(\mathcal A^{\prime }) \subseteq X$. Using the distributivity property of the semiring $\mathbb S$, it can be easily shown that $[\![\mathcal A^{\prime }]\!] = [\![\mathcal A]\!]$. □

Clearly, Lemmas 7 and 8 imply Theorem 3(a). Next, we show part (b) of Theorem 3.

Lemma 9

Let $\mathcal A$ be a weighted automaton over Σ and $\mathbb S$ . Then, there exists a sentence $\varphi \in \textbf {wMSO}^{\text {s.res}}({\Sigma }, \mathbb S)$ such that $[\![\varphi ]\!] = [\![\mathcal A]\!]$ and $\text {\sc Const}(\varphi ) = \text {\sc Const}(\mathcal A)$.

Proof

The proof of this lemma is a slight modification of the proof of Theorem 5.5 of [13]. Let $\mathcal A = (Q, I, T, F, \mathrm{wt})$. As in [13], Theorem 5.5, we assign with every transition t ∈ T a second-order variable X _t which will keep track of positions where this transition is taken. Let $\mathcal V = \{X_{t}\}_{t \in T}$. A run of $\mathcal A$ can be described using a formula β ∈ MSO(Σ) with $\mathrm{Free}(\beta ) = \mathcal V$ which demands that the values of $\mathcal V$-variables form a partition of the domain of an input word, the transitions of a run are matching, the labels of transitions of a run are compatible with an input word, a run starts in I and ends in F. Then, the $\textbf {wMSO}^{\text {s.res}}({\Sigma }, \mathbb S)$-sentence φ is defined as

$$ \varphi = {\textstyle \bigoplus} \mathcal V. \left( \beta \otimes {\textstyle \bigotimes} x. {\textstyle \bigoplus}_{t \in T} (X_{t}(x) \otimes wt(t)) \right). $$

(4)

where ${\textstyle \bigoplus } \mathcal V$ abbreviates ${\textstyle \bigoplus } X_{1}...{\textstyle \bigoplus } X_{n}$ for an enumeration $\mathcal V = \{X_{1}, ..., X_{n}\}$. Clearly, $\text {\sc Const}(\varphi ) = wt(T) = \text {\sc Const}(\mathcal A)$. Moreover, $[\![\varphi ]\!] = [\![\mathcal A]\!]$. □

Then, Theorem 3 follows immediately from Lemmas 7, 8 and 9.

6 Evaluators with Additional Properties

As we already mentioned in Section 4, the concept of multi-weighted MSO logic extends the semiring-weighted MSO logic. However, our Büchi result for the multi-weighted setting (cf. Theorem 2) does not agree with Theorem 1 for semirings, since the logical fragment of Theorem 2 is more restricted than the logical fragment of Theorem 1. This restriction can be explained, e.g., by Example 10.

In order to complete the picture of the robustness of multi-weighted logic, we put additional conditions on the evaluator under which the logical fragment of Theorem 1 (considered in the multi-weighted setting) is equivalent to multi-weighted automata. First, we provide an informal discription. As in the case of semiring-weighted automata, using a monoidal operation on M, we will define the weights of runs (which are also in M). After that, we collect the weights of runs in a multiset and evaluate this multiset using an aggregation function.

Let X, Y be sets, f : X → Y a mapping, and $\mu \in \mathbb N \langle X \rangle$ a finite multiset. Let $\mathbb E = (M, K, {\Phi })$ be an evaluator and $\mathbb M = (M, \diamond , 1)$ a monoid. Let ${f_{\mathbb M}: (M^{*}, \cdot , \varepsilon ) \to (M, \diamond , 1)}$ be the monoid morphism with $f_{\mathbb M}(m) = m$ for all m ∈ M. Let $F_{\mathbb M}: \mathbb N \langle M^{*} \rangle \to \mathbb N \langle M \rangle$ be defined for all $\mu \in \mathbb N \langle M^{*} \rangle$ and m ∈ M by ${F_{\mathbb M}(\mu )(m) = \sum (\mu (x) \; | \; x \in \mathrm{supp}(\mu ), f_{\mathbb M}(x) = m)}$. Informally, the mapping $F_{\mathbb M}$ replaces each sequence m ₁...m _k ∈ M ^∗ in a multiset by a single element (m ₁◇...◇m _k ) ∈ M, keeping multiplicities. We will abuse the notation and understand a multiset $\mu \in \mathbb N \langle M \rangle$ as a multiset in $\mathbb N \langle M^{*} \rangle$ with s u p p(μ) ⊆ M.

Definition 3

Let $\mathbb E = (M, K, {\Phi })$ be an evaluator and $\mathbb M = (M, \diamond , 1)$ a monoid. We say that $\mathbb E$ is an $\mathbb M$ -evaluator if ${\Phi } \circ F_{\mathbb M} = {\Phi }$.

Definition 3 means that the values of Φ of $\mathbb N \langle M \rangle$ completely determine its values on $\mathbb N \langle M^{*} \rangle$, and the diagram depicted in Fig. 2 commutes.

Fig. 2

The diagram for $\mathbb M$-evaluators

Example 11

(a) Let $\mathbb S = (S, +, \cdot , 0, 1)$ be a semiring and $\mathbb M = (S, \cdot , 1)$. Then, ${\mathbb E^{\mathbb S} = (S, S, {\Phi }^{\mathbb S})}$ is an $\mathbb M$-evaluator.

(b) Consider the evaluator $\mathbb E^{\text {\sc Ratio}} = (M, K, {\Phi }^{\text {\sc Ratio}})$ from Example 1 where ${M = \mathbb Q \times \mathbb Q_{\ge 0}}$ and $K = \mathbb Q \cup \{\infty \}$. Let $\mathbb M = (M, +, (0, 0))$ where + is the componentwise addition. Then, $\mathbb E^{\text {\sc Ratio}}$ is an $\mathbb M$-evaluator.

(c) Let $\eta \in \mathbb Q_{\ge 0}$ be a secondary cost bound. Consider the evaluator ${\mathbb E^{{\text {\sc Knap}}(\eta )} = (M, K, {\Phi }^{{\text {\sc Knap}}(\eta )})}$ from Example 2 where $M = \mathbb Q \times \mathbb Q$ and ${K = \mathbb Q \cup \{\infty \}}$. Consider the monoid ${\mathbb M = (M, +, (0, 0))}$ where + is the componentwise addition. Then, $\mathbb E^{{\text {\sc Knap}}(\eta )}$ is an $\mathbb M$-evaluator.

(d) Let $\mathbb E^{\text {\sc Disc}} = (M, K, {\Phi }^{\text {\sc Disc}})$ be the evaluator where ${M = \mathbb Q \times (\mathbb Q \cap (0,1])}$, ${K = \mathbb Q \cup \{\infty \}}$ and Φ^Disc is defined as in Example 3. Consider the monoid ${\mathbb M = (M, \diamond , (0, 1))}$ where ◇ is defined for all (x ₁, d ₁), (x ₂, d ₂) ∈ M by (x ₁, d ₁) ◇ (x ₂, d ₂) = (x ₁ + d ₁⋅x ₂, d ₁⋅d ₂). Then, $\mathbb E^{{\text {\sc Disc}}}$ is an $\mathbb M$-evaluator.

(e) Now we consider the evaluator from Example 10. This example was a witness why the restricted fragment of [13] (considered in the multi-weighted setting) is more expressive than multi-weighted automata over arbitrary evaluators. Let $\mathbb E = (M, \mathbb N \langle M^{*} \rangle , {\Phi })$ where M is a non-empty set and Φ is the identity mapping. Let ${\mathbb M = (M, \diamond , 1)}$ be any monoid. We show that $\mathbb E$ is not an $\mathbb M$-evaluator. Indeed, let m ∈ M and $\mu = [mm] \in \mathbb N \langle M^{*} \rangle$. Note that m ◇ m ∈ M and hence m m ≠ m ◇ m. Then, $F_{\mathbb M}(\mu ) = [m \diamond m] \neq \mu$ and hence ${\Phi }(F_{\mathbb M}(\mu )) = F_{\mathbb M}(\mu ) \neq \mu = {\Phi }(\mu ).$ Thus, there exists no monoid $\mathbb M$ such that $\mathbb E$ is an $\mathbb M$-evaluator.

We say that subsets M ^′,M ^″ of M ◇-commute elementwise if m ^′◇m ^″ = m ^″◇m ^′ for all m ^′ ∈ M ^′ and m ^″ ∈ M ^″.

Let the set $\textbf {aBOOL}({\Sigma }, \mathbb E)$ be defined as in the case of semirings. The fragment ${\textbf {mwMSO}_{\mathbb M}^{res}({\Sigma }, \mathbb E) \subseteq \textbf {mwMSO}({\Sigma }, \mathbb E)}$ is also defined as for semirings by the rules:

$$\varphi \; ::= \; \gamma \; | \; \varphi \oplus \varphi \; | \; \varphi \otimes \varphi^{\; (!)} \; | \; {\textstyle \bigoplus} x. \varphi \; | \; {{\textstyle \bigoplus}} X. \varphi \; | \; {{\textstyle \bigotimes}} x. \gamma $$

where $\gamma \in \textbf {aBOOL}({\Sigma }, \mathbb E)$, x ∈ V ₁ and X ∈ V ₂; moreover, there is an additional restriction at the place (!): a formula φ ₁⊗φ ₂ belongs to ${\textbf {mwMSO}}^{res}_{\mathbb M}({\Sigma }, \mathbb E)$ iff the sets Const(φ ₁) and Const(φ ₂) ◇-commute elementwise. Note that if $\mathbb M$ is a commutative monoid, then the use of φ ₁⊗φ ₂ is allowed without any restrictions. Clearly, ${\textbf {mwMSO}}^{\text {s.res}}({\Sigma }, \mathbb E) \subseteq {\textbf {mwMSO}}^{res}_{\mathbb M}({\Sigma }, \mathbb E)$.

Remark 3

Consider a semiring $\mathbb S = (S, +, \cdot , 0 , 1)$, the corresponding evaluator $\mathbb E_{\mathbb S}$ and the monoid $\mathbb M = (S, \cdot , \mathbb 1)$. Then, $\textbf {mwMSO}^{res}_{\mathbb M}({\Sigma }, \mathbb E^{\mathbb S}) = \textbf {wMSO}^{res}({\Sigma }, \mathbb S)$.

The main result of this section is the following theorem.

Theorem 4

Let Σ be an alphabet, $\mathbb E = (M, K, {\Phi })$ an evaluator, ${\mathbb M = (M, \diamond , 1)}$ a monoid such that $\mathbb E$ is an $\mathbb M$ -evaluator, and $\mathbb L: {\Sigma }^{+} \to K$ a quantitative language. Then, the following are equivalent.

(a) $\mathbb L$ is recognizable over $\mathbb E$.

(b) $\mathbb L$ is $\textbf {mwMSO}_{\mathbb M}^{res}({\Sigma }, \mathbb E)$ -definable.

If we apply this theorem to the evaluator $\mathbb E = \mathbb E^{\mathbb S}$ (where $\mathbb S = (S, +, \cdot , 0, 1)$ is a semiring) and to the monoid $\mathbb M = (S, \cdot , 1)$, then we obtain Theorem 1. Hence, Theorem 4 generalizes Theorem 1.

The rest of this section will be devoted to the proof of Theorem 4. Like in the proof of Theorem 2, we reduce the proof to the case of semirings. In contrast to the proof of Theorem 2, here we do not need to revisit the constructions for semiring-weighted formulas; we can apply the result of [13] as a ”black box”. Whereas in the proof of Theorem 2 we used the semiring $(\mathbb N \langle M^{*} \rangle , \uplus , \cdot , \emptyset , [\varepsilon ])$, here we will consider a different semiring. The domain of this semiring will be the set $\mathbb N \langle M \rangle$. We will consider the following operations. For all $\mu _{1}, \mu _{2} \in \mathbb N \langle M \rangle$, the union r ₁⊎r ₂ is defined as before. We extend ◇ to finite multisets as follows. Let $\mu _{1}, \mu _{2} \in \mathbb N \langle M \rangle$. Then, we define $(\mu _{1} \diamond \mu _{2}) \in \mathbb N \langle M \rangle$ for all m ∈ M by

$$(\mu_{1} \diamond \mu_{2})(m)\! =\! \sum \!\left( \mu_{1}(m_{1})\! \cdot \mu_{2}(m_{2}) \; \!|\! \; m_{1}\! \in \mathrm{supp}(\mu_{1}), m_{2} \!\in \mathrm{supp}(\mu_{2}), \\ \!m\! = \!m_{1} \!\diamond\! m_{2} \right) $$

It is well known that $(\mathbb N \langle M \rangle , \uplus , \diamond , \emptyset , [1])$ is a semiring (cf., e.g., [35], Subsect. 2.1). We will denote this semiring simply by $\mathbb N \langle M \rangle$.

Lemma 10

$F_{\mathbb M}: (\mathbb N \langle M^{*} \rangle , \cdot , \diamond , \emptyset , [\varepsilon ]) \to (\mathbb N \langle M \rangle , \uplus , \diamond , \emptyset , [1])$ is a semiring morphism with $F_{\mathbb M}([m]) = [m]$ for all m∈M.

Lemma 11

Let $\varphi \in \textbf {mwMSO}_{\mathbb M}^{res}({\Sigma }, \mathbb E)$ be a formula. Then, there exists a formula ${\varphi ^{\prime } \in \textbf {wMSO}^{res}({\Sigma }, \mathbb N \langle M \rangle )}$ such that ${[\![\varphi ^{\prime }]\!]^{\mathbb N \langle M \rangle } = F_{\mathbb M} \circ \langle \! \langle \varphi \rangle \! \rangle }$ and Free(φ ^′) = Free(φ.)

Proof

Let $\varphi ^{\prime } \in \textbf {wMSO}({\Sigma }, \mathbb N \langle M \rangle )$ be the formula obtained from φ by replacing each constant m ∈ M occurring in φ by the multiset $[m] \in \mathbb N \langle M \rangle$. Clearly, φ ^′ satisfies the restrictions on the use of ⊗ in $\textbf {wMSO}^{res}({\Sigma }, \mathbb N \langle M \rangle )$-formulas and hence $\varphi ^{\prime } \in \textbf {wMSO}^{res}({\Sigma }, \mathbb N \langle M \rangle )$. The equality $[\![\varphi ^{\prime }]\!]^{\mathbb N \langle M \rangle } = F_{\mathbb M} \circ \langle \! \langle \varphi \rangle \! \rangle$ can be easily shown inductively using Lemma 10. □

Lemma 12

Let $\mathcal A$ be a semiring-weighted automaton over Σ and $\mathbb N \langle M \rangle$ . Then, there exists a multi-weighted automaton $\mathcal A^{\prime }$ over Σ and $\mathbb E$ such that ${F_{\mathbb M} \circ \langle \! \langle \mathcal A^{\prime } \rangle \! \rangle = [\![\mathcal A]\!]^{\mathbb N \langle M \rangle }}$.

Proof

The proof is based on a similar construction as in the proof of Lemma 8. Here, for every transition t of $\mathcal A$, we represent its weight as $wt(t) = [m_{t,1}] + ... + [m_{t,n_{t}}]$ where n _t ≥ 0 and $m_{t_{1}}, ..., m_{t, n_{t}} \in M$. Then, as in Lemma 8, we split t into n _t transitions with the weights m _t,1, ..., $m_{t,n_{t}}$. □

Proof (of Theorem 4)

(a) ⇒ (b). Let $\mathcal A$ be a multi-weighted automaton over Σ and $\mathbb E$. Then, by Theorem 2, there exists a sentence $\varphi \in \textbf {mwMSO}^{\text {s.res}}({\Sigma }, \mathbb E)$ (and hence $\varphi \in \textbf {mwMSO}^{res}({\Sigma }, \mathbb E)$) with $[\![\varphi ]\!] = [\![\mathcal A]\!]$.

(b) ⇒ (a). Let $\varphi \in \textbf {mwMSO}_{\mathbb M}^{res}({\Sigma }, \mathbb E)$ be a sentence. By Lemma 11, there exists a sentence $\varphi ^{\prime } \in \textbf {wMSO}^{\mathrm{res}}({\Sigma }, \mathbb N \langle M \rangle )$ such that $[\![\varphi ^{\prime }]\!]^{\mathbb N \langle M \rangle } = F_{\mathbb M} \circ \langle \! \langle \varphi \rangle \! \rangle$. By Theorem 1, there exists a semiring-weighted automaton $\mathcal A^{\prime }$ over Σ and $\mathbb N \langle M \rangle$ such that ${[\![\mathcal A^{\prime }]\!]^{\mathbb N \langle M \rangle } = [\![\varphi ^{\prime }]\!]^{\mathbb N \langle M \rangle }}$. By Lemma 12, there exists a multi-weighted automaton $\mathcal A$ over Σ and $\mathbb E$ such that $F_{\mathbb M} \circ \langle \! \langle \mathcal A \rangle \! \rangle = [\![\mathcal A^{\prime }]\!]^{\mathbb N \langle M \rangle }$. Then, we have:

$$\begin{array}{@{}rcl@{}} [\![\varphi]\!]^{\mathbb E} &=&{\Phi} \circ \langle \! \langle \varphi \rangle \! \rangle \overset{*}{=} {\Phi} \circ F_{\mathbb M} \circ \langle \! \langle \varphi \rangle \! \rangle = {\Phi} \circ [\![\varphi^{\prime}]\!]^{\mathbb N \langle M \rangle} = {\Phi} \circ [\![\mathcal A^{\prime}]\!]^{\mathbb N \langle M \rangle} \\ &&= {\Phi} \circ F_{\mathbb M} \circ \langle \! \langle \mathcal A \rangle \! \rangle \overset{*}{=} {\Phi} \circ \langle \! \langle \mathcal A \rangle \! \rangle = [\![\mathcal A]\!]^{\mathbb E} \end{array} $$

where at ∗ we used that $\mathbb E$ is an $\mathbb M$-evaluator. □

7 Multi-weighted Automata and MSO Logic on Infinite Words

In this section, we will define and investigate multi-weighted automata and MSO logic on infinite words.

7.1 Multi-weighted Büchi Automata

In this subsection, we present a general framework for multi-weighted automata on infinite words. As opposed to the case of finite words, instead of finite multisets over M ^∗, we must consider multisets of infinite strings with possibly infinite supports and infinite multiplicities of elements.

Let Γ be a set (possibly infinite). An ω-word over Γ is an infinite sequence $(\gamma _{i})_{i \in \mathbb N}$ where γ _i ∈ Γ for all $i \in \mathbb N$. Let Γ^ω denote the set of all ω-words over Γ. Any set $\mathcal L \subseteq {\Gamma }^{\omega }$ is called an ω-language over Γ.

For a set X, let $|X| \in \mathbb N$ be the size of X if X is finite and |X| = ∞ otherwise. Let $\overline {\mathbb N} = \mathbb N \cup \{\infty \}$. Note that $(\overline {\mathbb N}, +, \cdot , 0, 1)$ is a semiring if we put 0 ⋅ ∞ = ∞ ⋅ 0 = 0. We will denote this semiring simply by $\overline {\mathbb N}$. Note that the operations + and ⋅ can be naturally extended to arbitrary families of elements in $\overline {\mathbb N}$.

For a set X, an ω-multiset over X is a mapping $\mu : X \to \overline {\mathbb N}$. Let $\overline {\mathbb N} \langle \! \langle X \rangle \! \rangle$ denote the set of all ω-multisets over X. For any $\mu \in \overline {\mathbb N} \langle \! \langle X \rangle \! \rangle$, the support of μ is the set s u p p(μ) = {x ∈ X | μ(x) ≠ 0}. Note that, comparing to the notation $\mathbb N \langle X \rangle$ for the class of finite multisets with the notation $\overline {\mathbb N} \langle \! \langle X \rangle \! \rangle$ for the class of ω-multisets, the double angle brackets emphasize that the support of an ω-multiset is not necessarily finite anymore. Let Y be a set, f : X → Y a mapping and X ^′ ⊆ X a subset of X (not necessarily finite). We denote by $f[X^{\prime }] \in \overline {\mathbb N} \langle \! \langle Y \rangle \! \rangle$ the ω-multiset such that f[X ^′](y) = |{x ∈ X ^′ | f(x) = y}| for all y ∈ Y.

Definition 4

An ω-evaluator is a structure $\mathbb E = (M, K, {\Phi }^{\omega })$ where M and K are non-empty sets and ${\Phi }^{\omega }: \overline {\mathbb N} \langle \! \langle M^{\omega } \rangle \! \rangle \to K$ is an ω-aggregation function.

Definition 5

Let Σ be an alphabet and $\mathbb E = (M, K, {\Phi }^{\omega })$ an ω-evaluator. A multi-weighted Büchi automaton over Σ and $\mathbb E$ is a tuple $\mathcal A = (Q, I, T, F, wt)$ where Q is a finite set of states, I, F are sets of initial resp. accepting sets, T ⊆ Q × Σ × Q is a transition relation, and w t : T → M is a transition weight function.

In other words, a multi-weighted Büchi automaton $\mathcal A$ is defined just like a multi-weighted automaton. Infinite runs ${\rho = (t_{i})_{i \in \mathbb N}}$ of $\mathcal A$ are defined as infinite sequences of matching transitions, say t _i = (q _i , a _i , q _i+1) for each $i \in \mathbb N$, such that q ₀ ∈ I and ${\{q \in F \; | \; q = q_{i} \text { for infinitely many} i \in \mathbb N\} \neq \emptyset }.$ Let $label\, (\rho ) := (a_{i})_{i \in \mathbb N} \in {\Sigma }^{\omega }$, the label of ρ. As in the case of finite words, we denote by $Run_{\mathcal A}$ the set of all runs of $\mathcal A$ and, for each w ∈ Σ^ω, we denote by $Run_{\mathcal A}(w)$ the set of all runs ρ of $\mathcal A$ with label (ρ) = w. Similarly to multi-weighted automata on finite words, we define ${wt^{\#}_{\mathcal A}: Run_{\mathcal A} to M^{\omega }}$ for every run $\rho = (t_{i})_{i \in \mathbb N} \in Run_{\mathcal A}$ as $wt^{\#}_{\mathcal A}(\rho ) = (wt(t_{i}))_{i \in \mathbb N}$. Recall that, for any subset $X \subseteq Run_{\mathcal A}$, $wt^{\#}_{\mathcal A}[X] \in \overline {\mathbb N} \langle \! \langle M^{\omega } \rangle \! \rangle$. Then, the behavior of $\mathcal A$ is the mapping $[\![\mathcal A]\!]: {\Sigma }^{\omega } to K$ defined for all w ∈ Σ^ω by $[\![\mathcal A]\!](w) = {\Phi }^{\omega }(wt^{\#}_{\mathcal A}[Run_{\mathcal A}(w)]).$ A mapping $\mathbb L: {\Sigma }^{\omega } \to K$ is called a quantitative ω-language. We say that $\mathbb L$ is recognizable over $\mathbb E$ if there exists a multi-weighted Büchi automaton $\mathcal A$ over Σ and $\mathbb E$ such that $[\![\mathcal A]\!] = \mathbb L$.

Example 12

(a) Here, we consider the reward-cost ratio setting of Example 1 for infinite words (cf. [7, 8]). Let $M = \mathbb Q \times \mathbb Q_{\ge 0}$ and $K = \mathbb R \cup \{-\infty , \infty \}$. For a sequence ${u = (m_{i})_{i \in {\mathbb N}} \in M^{\omega }}$ with m _i = (r _i , c _i ), the supremum ratio (cf. [7]) is ${\text {\sc Ratio}^{\omega } (u) = \limsup \limits _{n to \infty } \frac {r_{1} + ... + r_{n}}{c_{1} + ... + c_{n}}}$ with $\frac {r}{0} = \infty$. Consider the ω-evaluator $\mathbb E^{\omega \text {-}{\text {\sc Ratio}}} = (M, K, {\Phi }^{\omega \text {-}{\text {\sc Ratio}}})$ where Φ^ω-Ratio is defined for every ω-multiset $\mu \in {\overline {\mathbb N}} \langle M^{\omega } \rangle$ as Φ^ω-Ratio(μ) = sup{Ratio^ω(u) | u ∈ s u p p(μ)}.

(b) Alternatively to finding the supremum of the set of supremum ratios of runs in (a), it could be also interesting to check, whether there are finitely many runs whose supremum ratio is above some threshold $\theta \in \mathbb R$. For this purpose, we can consider the ω-evaluator $\mathbb E^{\omega \text {-}{\text {\sc Ratio}} > \theta } = (M, K, {\Phi }^{\omega \text {-}{\text {\sc Ratio}} > \theta })$ where $M = \mathbb Q \times \mathbb Q_{\ge 0}$, $K = \overline {\mathbb N}$ and Φ^{ω-Ratio>𝜃} is defined for every ω-multiset $\mu \in \overline {\mathbb N} \langle M^{\omega } \rangle$ by

$${\Phi}^{\omega\text{-}\text{\sc Ratio} > \theta}(\mu) = \sum \left( \mu(u) \; | \; u \in \mathrm{supp}(\mu) \text{ and} \text{\sc Ratio}^{\omega}(u) >\theta \right) $$

where $\sum$ is the usual sum operation where n + ∞ = ∞ + n = ∞ and every infinite sum is evaluated to ∞ if it contains infinitely many non-zero summands. We note that in this example multiplicities of elements if an ω-multiset matter, since we use the natural sum operation.

(c) Here, we present an ω-evaluator for the model of multi-weighted automata which correspond to one-player energy games considered in [23]. Let n ≥ 1 be the number of energy storages and $E^{1}_{\max }, ..., E^{n}_{\max } \in \mathbb N$ their maximal capacities. We start with the empty storages and, along a run, the energy level of each storage can be increased (if we regain energy) or decreased (if we consume energy). Our goal is to keep the energy level of each storage j between 0 and $E^{j}_{\max }$. Consider the sequence $u = (u_{i})_{i \in {\mathbb N}}$ where, for all $i \in {\mathbb N}$, $u_{i} = ({u_{i}^{1}}, ..., {u_{i}^{n}}) \in \mathbb Z^{n}$ is a vector of the energy level changes for each storage. We transform this sequence to the sequence $\tilde {u} = (\tilde {u}_{i})_{i \in {\mathbb N}}$ of the absolute energy levels ${\tilde {u}_{i} = (\tilde {u}^{1}_{i}, ..., \tilde {u}^{n}_{i}) \in \mathbb Z^{n}}$ defined inductively on i ≥ 1 as follows. For j ∈ {1,...,n}, let ${\tilde {u}_{1}^{j} = \min \{{u_{i}^{j}}, E_{\max }^{j} \}}$. Then, for i > 1 and j ∈ {1,...,n}, we let $\tilde {u}_{i}^{j} = \min \{\tilde {u}_{i-1}^{j} + {u_{i}^{j}}, E_{\max }^{j} \}$. Note that, for all $i \in {\mathbb N}$ and j ∈ {1,...,n}, $\tilde {u}^{j}_{i} \in (-\infty , E^{j}_{\max })$. We say that u is correct if $\tilde {u}_{i}^{j} \ge 0$ for all $i \in {\mathbb N}$ and j ∈ {1,...,n}. Then, for this situation we consider the ω-evaluator $\mathbb E^{\omega \text {-}{\text {\sc Energy}}} = (M, K, {\Phi }^{\omega \text {-}{\text {\sc Energy}}})$ where $M = \mathbb Z^{n}$, K = {0, 1} and ${\Phi }^{\omega \text {-}{\text {\sc Energy}}}: {\overline {\mathbb N}} \langle M^{\omega } \rangle \to K$ is defined for every ω-multiset $\mu \in {\overline {\mathbb N}} \langle M^{\omega } \rangle$ as

$${\Phi}^{\omega\text{-}\text{\sc Energy}}(\mu) = \left\{\begin{array}{ll} 1, & \text{if} \exists u \in \mathrm{supp}(\mu): u \text{ is correct},\\ 0, & \text{otherwise}. \end{array}\right. $$

(d) In this example, we consider an ω-valuation monoid $\mathbb V = (D, +, val^{\omega }, 0)$ of Droste and Meinecke (cf. for details [17], Definition 5.1) where $\mathbb D = (D, +, 0)$ is a complete monoid (i.e., it has infinitary sum operations satisfying several natural axioms) and v a l ^ω:D ^ω t o D is an ω-valuation function with some additional properties. We say that $\mathbb D$ is ∞-idempotent if, for all d ∈ D and all infinite index sets I, J, we have $d_{\infty } := {\sum }_{i \in I} d = {\sum }_{j \in J} d$. The idempotent complete monoids ${(\mathbb R \cup \{-\infty , \infty \}, \sup , -\infty )}$ and $(\mathbb R \cup \{-\infty , \infty \}, \inf , \infty )$ are examples of ∞-idempotent monoids. The non-idempotent monoid $(\overline {\mathbb N}, +, 0)$ is another example of an ∞-idempotent monoid. If $\mathbb D$ is ∞-idempotent, then $\mathbb V$ can be considered as the ω-evaluator $\mathbb E^{\mathbb V} = (D, D, {\Phi }^{\mathbb V})$ where ${\Phi }^{\mathbb V}: \overline {\mathbb N} \langle D^{\omega } \rangle \to D$ is defined for every ω-multiset $\mu \in \overline {\mathbb N} \langle D^{\omega } \rangle$ by

$${\Phi}^{\mathbb V}(\mu) = \sum\limits_{u \in \mathrm{supp}(\mu)} \mu(u) \cdot val^{\omega}(u) $$

where for all $n \in \mathbb N$ and d ∈ D, n⋅d = d+...+d (n summands) and ∞⋅d = d _∞ .

The case of ω-valuation monoids which are not ∞-idempotent could be handled by extending our ω-evaluators to the ω-multisets where, instead of the multiplicity ∞ for infinite sets, we use infinite cardinal numbers. However, due to lack of motivation and technical complicating of the paper, we do not consider this extension.

7.2 Multi-weighted MSO Logic on Infinite Words

Now we will introduce a multi-weighted MSO logic on infinite words. We want to follow a similar approach as for finite words, i.e., we define the semantics using the framework of ω-evaluators. Recall that, for finite words, an aggregation function was defined as ${\Phi }: \mathbb N \langle M^{*} \rangle \to K$ whereas for infinite words an ω-aggregation function is a mapping ${\Phi }^{\omega }: \overline {\mathbb N} \langle \! \langle M^{\omega } \rangle \! \rangle \to K$. In order to avoid the difficulties with the definition of the concatenation of ω-strings, we will not introduce a general definition of logic and restrict ourselves to a restricted fragment which will be defined exactly as $\textbf {mwMSO}^{\text {s.res}}({\Sigma },\mathbb E)$ for finite words.

For ω-multisets $\mu _{1}, \mu _{2} \in \overline {\mathbb N} \langle \! \langle X \rangle \! \rangle$, the union is defined for all x ∈ X by (μ ₁⊎μ ₂)(x) = μ ₁(x) + μ ₂(x). Let I be an arbitrary index set (possibly infinite) and (μ _i ) _{i ∈ I} a family of ω-multisets $\mu _{i} \in \overline {\mathbb N} \langle \! \langle X \rangle \! \rangle$. Then, the union ${\mu := ({\textstyle \biguplus }_{i \in I} \mu _{i}) \in \overline {\mathbb N} \langle \! \langle X \rangle \! \rangle }$ is defined for all x ∈ X by $\mu (x) = {\sum }_{i \in I} \mu _{i}(x)$.

For $(k_{i})_{i \in \mathbb N} \in \overline {\mathbb N}^{\omega }$, the product $k := \left ({\prod }_{i \in \mathbb N} k_{i} \right ) \in \overline {\mathbb N}$ is defined as follows:

• if k _i = 0 for some $i \in \mathbb N$, then we let k = 0;

• if k _i > 0 for all $i \in \mathbb N$ and k _j = ∞ for some $j \in \mathbb N$, then we let k = ∞;

• if $k_{i} \in \mathbb N \setminus \{0\}$ for all $i \in \mathbb N$ and there are infinitely many $i \in \mathbb N$ with k _i > 1, then we let k = ∞;

• if $k_{i} \in \mathbb N \setminus \{0\}$ for all $i \in \mathbb N$ and there exists $j \in \mathbb N$ such that k _i = 1 for all i > j, then we let $k = {\prod }_{i = 1}^{j} k_{j}$.

Let $(r_{i})_{i \in \mathbb N}$ be a family of finite multisets $r_{i} \in \mathbb N \langle X \rangle$ (as defined in Section 3). Then, we define the ω-multiset $\mu := \left ({\prod }_{i \in \mathbb N} r_{i} \right ) \in \overline {\mathbb N} \langle \! \langle X^{\omega } \rangle \! \rangle$ for each $u = (x_{i})_{i \in \mathbb N} \in X^{\omega }$ as $\mu (u) = {\prod }_{i \in \mathbb N} r_{i}(x_{i}).$

Let Σ be an alphabet. As in Section 3, we consider countable and pairwise disjoint sets V ₁ and V ₂ of first-order resp. second order variables. The set MSO ^ω(Σ) of Boolean ω-formulas is defined exactly as MSO(Σ) for finite words. Given an ω-word w ∈ Σ^ω, a w-ω-assignment σ is defined as in the case of finite words with the only difference that $\mathrm{dom}(w) = \mathbb N$. A first-order update σ[x/i] with x ∈ V ₁ and $i \in \mathbb N$ and a second-order update σ[X/I] with X ∈ V ₂ and $I \subseteq \mathbb N$ are defined in the usual manner. Let ${\Sigma }_{V}^{\omega }$ denote the set of all pairs (w, σ) where w ∈ Σ^ω and σ is a w- ω-assignment. Again, we stress that ${\Sigma }_{V}^{\omega }$ is not (Σ _V )^ω. Given $(w, \sigma ) \in {\Sigma }_{V}^{\omega }$ and β ∈ MSO ^ω(Σ), the definition that (w, σ) satisfies β, written (w, σ) ⊧ β, is given inductively on the structure of β as usual.

Let $\mathbb E = (M, K, {\Phi }^{\omega })$ an ω-evaluator. The set $\textbf {aBOOL}^{\omega }({\Sigma }, \mathbb E)$ of almost Boolean ω-formulas is given by the grammar

$$\gamma \; ::= \; m \; | \; \gamma \oplus \gamma \; | \; \beta \otimes \gamma $$

where β ∈ MSO ^ω(Σ) and m ∈ M.

The set $\textbf {mwMSO}^{\omega }({\Sigma }, \mathbb E)$ of multi-weighted ω-formulas over Σ and $\mathbb E$ is given by the grammar

$$\varphi \; ::= \; {\textstyle \bigotimes} x. \gamma \; | \; \varphi \oplus \varphi \; | \; \beta \otimes \varphi \; | \; {\textstyle \bigoplus} x. \varphi \; | \; {{\textstyle \bigoplus}} X. \varphi $$

where β ∈ MSO ^ω(Σ), $\gamma \in \textbf {aBOOL}^{\omega }({\Sigma }, \mathbb E)$, x ∈ V ₁ and X ∈ V ₂. Note that ${\textbf {aBOOL}}^{\omega } \cap {\textbf {mwMSO}}^{\omega }({\Sigma }, \mathbb E) = \emptyset$ and that ${\textbf {mwMSO}}^{\omega }({\Sigma }, \mathbb E)$ is defined exactly as ${\textbf {mwMSO}}^{\text {s.res}}({\Sigma }, \mathbb E)$.

We define the auxiliary semantics 〈 〈...〉 〉 separately for almost Boolean and multi-weighted ω-formulas.

• Let $\gamma \in \textbf {aBOOL}^{\omega }({\Sigma }, \mathbb E)$. Then, the auxiliary semantics of γ is the mapping $\langle \gamma \rangle : {\Sigma }^{\omega }_{V} to \mathbb N \langle M \rangle$ defined for every $(w, \sigma ) \in {\Sigma }^{\omega }_{V}$ inductively on the structure of γ as shown in Table 2. Here, m ∈ M, β ∈ MSO ^ω(Σ), and ${\varphi , \varphi _{1}, \varphi _{2} \in {\textbf {aBOOL}}^{\omega }({\Sigma }, \mathbb E)}$.

• Let $\varphi \in \textbf {mwMSO}^{\omega }({\Sigma }, \mathbb E)$. Then, the auxiliary semantics of φ is the mapping $\langle \varphi \rangle : {\Sigma }^{\omega }_{V} to {\overline {\mathbb N}} \langle M^{\omega } \rangle$ defined for every $(w, \sigma ) \in {\Sigma }^{\omega }_{V}$ inductively on the structure of φ as shown in Table 3. Here, β ∈ MSO ^ω(Σ), $\gamma \in {\textbf {aBOOL}}^{\omega }({\Sigma }, \mathbb E)$, $\varphi , \varphi _{1}, \varphi _{2} \in {\textbf {mwMSO}}^{\omega }({\Sigma }, \mathbb E)$, x ∈ V ₁ and X ∈ V ₂.

  Table 2 The auxiliary semantics of almost Boolean ω-formulas

  Table 3 The auxiliary semantics of multi-weighted ω-formulas

Now, given a formula $\varphi \in \textbf {mwMSO}^{\omega }({\Sigma }, \mathbb E)$, we define the proper semantics (or simply semantics) $[\![\varphi ]\!]: {\Sigma }^{\omega }_{V} to K$ for all $(w, \sigma ) \in {\Sigma }^{\omega }_{V}$ as [ [φ] ](w, σ) = Φ^ω(〈 〈φ〉 〉(w, σ)).

Given a formula φ, the set Free(φ) of free variables of φ is defined as usual. We say that a formula $\varphi \in {\textbf {mwMSO}}^{\omega }({\Sigma }, \mathbb E)$ is a sentence if Free(φ) = ∅. Clearly, if φ is a sentence, then the semantics [ [φ] ](w, σ) does not depend on σ. Then, we can consider the semantics [ [φ] ] as the mapping [ [φ] ]:Σ^ω→K. Let $\mathbb L$ be a quantitative ω-language. We say that $\mathbb L$ is definable if there exists a sentence $\varphi \in {\textbf {mwMSO}}^{\omega }({\Sigma }, \mathbb E)$ such that $[\![\varphi ]\!] = \mathbb L$.

Example 13

Assume that a bus can operate two routes A and B which start and end at the same place. For R ∈ {A, B}, the route R lasts $t_{R} \in \mathbb Q_{> 0}$ timed units and profits $p_{R} \in \mathbb Q_{> 0}$ money units on the average per trip. We may be interested in making an infinite schedule for this bus which is represented as an infinite sequence from {A, B}^ω. This schedule must be fair in the sence that both routes A and B must occur infinitely often in this timetable (even if the route A or B is unprofitable). The optimality of the schedule is also preferred (we wish to profit per time unit as much as possible). We consider the ω-evaluator $\mathbb E^{\omega \text {-}{\text {\sc Ratio}}}$ from Example 12a and a singleton alphabet Σ = {τ} which is irrelevant here. Now we construct a sentence $\varphi \in {\textbf {mwMSO}}^{\omega }({\Sigma }, \mathbb E^{\omega \text {-}{\text {\sc Ratio}}})$ to define the optimal income of the bus per time unit (supremum ratio between rewards and time):

$$\varphi = {\textstyle \bigoplus} X. \left( \left( \overset{\infty}{\exists} x. X(x) \wedge \overset{\infty}{\exists} x. \lnot (X(x)) \right) \otimes {\textstyle \bigotimes} x. ((X(x) \otimes r_{A}) \oplus ((\lnot X(x)) \otimes r_{B})) \right) $$

where $\overset {\infty }{\exists } x. \psi$ is an abbreviation of the MSO ^ω(Σ)-formula ∀y.∃x.((y ≤ x) ∧ψ), r _A = (p _A , t _A ) and r _B = (p _B , t _B ). Here, the second order variable X corresponds to the set of positions in an infinite schedule which can be assigned to the route A. Then,

$$ [\![\varphi]\!](\tau^{\omega}) = \sup \left\{ \limsup_{n \to \infty} \frac{p_{A} \cdot |I \cap \overline{n}| + p_{B} \cdot |I^{c} \cap \overline{n}|} {t_{A} \cdot |I \cap \overline{n}| + t_{B} \cdot |I^{c} \cap \overline{n}|} \; | \; I \subseteq \mathbb N\, \text{with} I, I^{c} \text{infinite} \right\} $$

(5)

where $\overline {n} = \{1, ..., n\}$ and $I^{c} = \mathbb N \setminus I$.

Remark 4

In the case of finite words, we could also choose $\textbf {mwMSO}^{\text {s.res}}({\Sigma }, \mathbb E)$ as the basic definition of multi-weighted MSO logic. The motivation for the introduction of the unrestricted fragment $\textbf {mwMSO}({\Sigma }, \mathbb E)$ was to show that our multiset approach to the semantics is a natural extension of the semiring-based semantics of Droste and Gastin [13]. Moreover, in Example 10 we justified our restrictions in the general case of evaluators.

7.3 The Expressive Equivalence Result for Infinite Words

Here we prove our main result for infinite words which is a counterpart of Theorem 2 for finite words.

Theorem 5

Let Σ be an alphabet, $\mathbb E = (M, K, {\Phi }^{\omega })$ an ω-evaluator, and ${\mathbb L: {\Sigma }^{\omega } \to K}$ a quantitative ω-language. Then, $\mathbb L$ is recognizable over $\mathbb E$ iff $\mathbb L$ is definable over $\mathbb E$.

The proof of this theorem will be given below. Whereas for the proof of Theorem 2 we used the semiring $\mathbb N \langle M^{*} \rangle$ of finite multisets, here we deal with the monoid $(\overline {\mathbb N} \langle \! \langle M^{\omega } \rangle \! \rangle , \uplus , \emptyset )$ of ω-multisets.

First, we show that definability implies recognizability. As in the case of finite words, given a multi-weighted automaton $\mathcal A$, we define the auxiliary behavior ${\langle \mathcal A \rangle : {\Sigma }^{+} to {\overline {\mathbb N}} \langle M^{\omega } \rangle }$ as $\langle \mathcal A \rangle (w) = wt^{\#}_{\mathcal A}[Run_{\mathcal A}(w)]$. Then, $[\![\mathcal A]\!] = {\Phi }^{\omega } \circ \langle \mathcal A \rangle$.

Lemma 13

Let $\varphi \in \textbf {mwMSO}^{\omega }({\Sigma }, \mathbb E)$ be a sentence. Then, there exists a multi-weighted automaton $\mathcal A$ over Σ and $\mathbb E$ such that $\langle \mathcal A \rangle = \langle \varphi \rangle$.

Proof

Our construction follows the ideas from the proofs of Lemmas 7 and 8 for finite words. We only have to pay attention to the fact that Büchi automata are not determinizable. However, this is not an obstruction, since we can consider unambiguous Büchi automata (i.e., for every word there is at most one run) instead of deterministic Büchi automata. As it was shown in [10], every Büchi automaton can be transformed into an unambiguous one accepting the same language.

As in Lemma 7, we proceed by induction on the structure of φ. We briefly run through the significant details of the constructions:

• Let $\varphi = {\textstyle \bigotimes } x. \gamma$ where x ∈ V ₁ and $\gamma \in \textbf {aBOOL}^{\omega }({\Sigma }, \mathbb E)$. Following the idea of [13], Theorem 5.5, (where we replace deterministic automata by unambiguous automata) we can construct a multi-weighted Büchi automaton whose weights are finite multisets in $\mathbb N \langle M \rangle$. Then, applying the construction of Lemma 8, we split the transitions labelled by multisets into several transitions labelled by the elements of these multisets.

• Let φ = β⊗φ ^′ where β ∈ MSO ^ω(Σ). Here, we take an unambiguous Büchi automaton for β and apply the standard product construction for Büchi automata (where the weights of transitions are equal to the weights of the corresponding transitions of the multi-weighted Büchi automaton for φ ^′).

• Let φ = φ ₁ ⊕ φ ₂. Here, we use the standard disjoint union construction.

• Let $\varphi = {\textstyle \bigoplus } \mathcal V. \varphi ^{\prime }$ where $\mathcal X \in V_{1} \cup V_{2}$. Here, we apply the construction of [20] for the projection.

□

As an immediate corollary, we obtain:

Corollary 1

Let $\varphi \in \textbf {mwMSO}^{\omega }({\Sigma }, \mathbb E)$ be a sentence. Then, there exists a multi-weighted automaton $\mathcal A$ over Σ and $\mathbb E$ such that $[\![\mathcal A]\!] = [\![\varphi ]\!]$.

Now we turn to the converse direction of the proof of Lemma 5.

Lemma 14

Let $\mathcal A$ be a multi-weighted Büchi automaton over Σ and $\mathbb E$ . Then, there exists an ω-sentence $\varphi \in {\textbf {mwMSO}}^{\omega }({\Sigma }, \mathbb E)$ such that $[\![\varphi ]\!] = [\![\mathcal A]\!]$.

Proof

We proceed like in the proof of Lemma 9. Let $\mathcal A = (Q, I, T, F, \mathrm{wt})$ and $\mathcal V$ be defined as in the proof of Lemma 9. Analogously, we can define a run of $\mathcal A$ using an MSO ^ω(Σ)-formula β with $\mathrm{Free}(\beta ) = \mathcal V$ (in contrast to the case of finite words, we replace the condition that a run ends in a final state by the Büchi acceptance condition). We define φ as in Eq. 4. Then, $\langle \! \langle \varphi \rangle \! \rangle = \langle \! \langle \mathcal A \rangle \! \rangle$ and hence $[\![\varphi ]\!] = {\Phi }^{\omega } \circ \langle \! \langle \varphi \rangle \! \rangle = {\Phi }^{\omega } \circ \langle \! \langle \mathcal A \rangle \! \rangle = [\![\mathcal A]\!]$. □

Proof (of Theorem 5)

Immediate from Corollary 1 and Lemma 14. □

8 Conclusion

We introduced a general model of multi-weighted automata. On one hand, this model covers a new class of multi-weighted settings. On the other hand, it also extends the models of weighted automata over semirings and valuation monoids. We have extended the use of weighted MSO logic to this new class of multi-weighted settings. Since our translations from formulas to automata are effective, we can reduce the decidability problems for multi-weighted logics to the corresponding problems for multi-weighted automata. Decidability results of, e.g., [7, 23, 27, 31] lead to decidability results for multi-weighted nondeterministic automata. However, for infinite words, the literature did not consider the Büchi acceptance condition for multi-weighted automata. Therefore, our future work will investigate decision problems for multi-weighted Büchi automata. Also, weighted MSO logics for weighted timed automata were investigated in [34, 19]. In our further work, we wish to combine the ideas of [34, 19] and the current work to obtain a Büchi theorem for multi-weighted timed automata.