{'fraction_non_alphanumeric': 0.06079415390033457, 'fraction_numerical': 0.010873393203028702, 'mean_word_length': 3.8037640093042926, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 8, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Multi-weighted Automata and MSO Logic

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


Introduction
Recently, multi-priced timed automata [5,6,17,20] 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 [5,6], or the optimal consumption of several resources where more than one resource must be restricted [20]. Arising from the model of timed automata, the multi-weighted setting has also attracted much notice for classical non-deterministic automata [1,3,16,18].
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 [7,15] established the expressive equivalence of finite automata and MSO logic. Weighted MSO logic with weights taken from an arbitrary semiring was introduced in [10,11] 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 [11]. Chatterjee, Doyen, and Henzinger [8,9] investigated weighted automata modeling the average and long-time behavior of systems. The behavior of such automata cannot be described by semiring-weighted automata. In [13,14], valuation monoids were presented to model the quantitative behaviors of these automata. Their logical characterization was given in [14]. 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 [2,12,19,22], or even valuation monoid automata [13,14].
First, we develop a general model for multi-weighted automata which incorporates several multi-weighted settings from the literature. 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). Different 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 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. Our Büchi-type result for multi-weighted automata on finite words is established by reducing it to the corresponding result of [14] for the product valuation monoid of finite multisets.
In the case of infinite words, it is usually not possible to collect all the information about weights of paths in finite multisets. Therefore, we cannot directly reduce the desired result to the proof given in [14] for infinite words. But we can use the result of [14] to translate each multi-weighted formula of our logic into an automaton over the product ω-valuation monoid of multisets, and we show that the weights of transitions in this automaton satisfy certain properties which allow us to translate it into a multiweighted automaton.
All our automata constructions are effective. Thus, decision problems for multiweighted logic can be reduced to decision problems of multi-weighted automata. Some of these problems for automata can be solved whereas for others the details still have to be explored.

Multi-weighted Automata on Finite Words
The model of multi-weighted (or multi-priced) automata is an extension of the model of weighted automata over semirings [2,12,19,22] and valuation monoids [13,14] by featuring several price parameters. In the literature, different situations of the behaviors of multi-weighted automata were considered (cf. [1,3,5,6,16,17,18,20]) to model the consumption of several resources. For instance, the model of multi-priced timed automata introduced in [5] 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.
Consider an automaton in which every transition carries a reward and a cost. For paths of transitions, we are interested in the ratio between accumulated rewards and accumulated costs. The automaton should assign to each word the maximal reward-cost ratio of accepting paths on w. The idea is to model the weights by elements of the set M = R × R ≥0 . We use a valuation function val : M + → M to associate to each sequence of such weights a single weight in M . Since our automata are nondeterministic and a word may have several accepting paths, we obtain a multiset of weights of these paths, hence a multiset of elements from M . We use an evaluator function Φ which associates to each multiset of M a single value. The mapping Φ can be considered as a general summation operator. Now we turn to formal definitions.
To cover also the later case of infinite words, we let N = N ∪ {∞}. Let M be a set. A multiset over M is a mapping r : M → N. For each m ∈ M , r(m) is the number of copies of m in r. We let supp(r) = {m ∈ M | r(m) = 0}, the support of r. We say that a multiset r is finite if supp(r) is finite and ∞ / ∈ r(M ). We denote the collection of all multisets by N M and the collection of all finite multisets by N M . A nondeterministic automaton over an alphabet Σ is a tuple A = (Q, I, T, F ) where Q is a set of states, I, F ⊆ Q are sets of initial resp. final states and T ⊆ Q × Σ × Q is a transition relation. Finite paths π = (t i ) 0≤i≤n of A are defined as usual as finite sequences of matching transitions, say t i = (q i , a i , q i+1 ). Then we call the word w = a 0 a 1 ...a n ∈ Σ + the label of the path π and π a path on w. A path is accepting if it starts in I and ends in F . We denote the set of all accepting paths of A on w ∈ Σ + by Acc A (w). Let A be a multi-weighted automaton over Σ and M, w ∈ Σ + and π = t 0 ...t n a path on w. The weight of π is defined by Weight A (w) = val(γ(t i )) 0≤i≤n . Let |A|(w) ∈ N M be the finite multiset containing the weights of all accepting paths in Acc A (w). Formally, |A|(w)(m) = |{π ∈ Acc A (w) | Weight A (π) = m}| for all m ∈ M . The behavior ||A|| : Σ + → K of A is defined for all w ∈ Σ + by ||A||(w) = Φ(|A|(w)).
Note that every weighted automaton over a valuation monoid (M, +, val, 0) (cf. [13,14]) can be considered as a multi-weighted automaton over the Kvaluation structure (M, val, Φ) with K = M and Φ : N M → M defined by Φ(r) = (m | m ∈ supp(r) and 1 ≤ i ≤ r(m)) (as usual, ∅ = 0). Moreover, multi-weighted automata extend the model of weighted automata over valuation monoids in two directions. First, whereas the weights of transitions in multi-weighted automata are taken from M , the behavior is a mapping with the codomain K where K and M do not necessarily coincide. Second, we resolve the nondeterminism in multiweighted automata using an evaluator function Φ defined on finite multisets.
Next, we consider several examples how to describe the behavior of multi-weighted automata known from the literature using valuation structures. In each of the three examples below, let Σ be an alphabet, M = (M, val, Φ) a K-valuation structure, and A a multi-weighted automaton over Σ and M.
x y where we put x 0 = ∞ and max(∅) = −∞. For instance, for every transition weight (x, y) ∈ M , x might mean the reward and y the cost of the transition. Then ||A||(w) is the maximal ratio between accumulated rewards and costs of accepting paths on w. The ratio setting was considered first for multi-priced timed automata [5,6] and also for nondeterministic automata [3,18].
Let val be as in the previous example and Φ(r) = min{x | (x, y) ∈ supp(r) and y ≤ p}, for r ∈ N M , with min(∅) = ∞. Let t be a transition and γ(t) = (x, y). We call x the primary and y the secondary cost. Then ||A||(w) is the cheapest primary cost of reaching with w some final state under the given upper bound constraint p ∈ R on the secondary cost. The optimal conditional reachability problem for multi-priced timed automata was studied in [20].
Suppose that A controls the movement of some object in R n and each transition t carries the coordinates of the displacement vector of this object. Then, ||A||(w) is the value of the average displacement of the object after executing w.

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, the semantics of formulas must reflect the maximal 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 [11,14]. We solve this problem in the following way. We associate to each word a multiset of elements of M . Here, for disjunction and existential quantification, we use the multiset union. For conjunction, we extend a product operation given on the set M to the Cauchy product of multisets. Similarly, for universal quantification, we extend the valuation function on M + to N M + . Then, we use an evaluator function Φ which associates to each multiset of elements a single value (e.g. the maximal reward-cost ratio of pairs contained in a multiset).
As in the case of weighted MSO logics over product valuation monoids [14], we extend a valuation structure (cf. Definition 1) with a unit element and a binary operation in order to define the semantics of atomic formulas and of the conjunction.
For the rest of this section, we fix an alphabet Σ and a K-pv-structure M = (M, val, ⋄, 1, Φ). Let V be a countable set of first and second order variables. Lower-case letters like x, y denote first order variables whereas capital letters like X, Y etc. denote second order variables. The syntax of multi-weighted MSO logic over Σ and M is defined as in [4] by the grammar: The formulas β are called boolean formulas and the formulas ϕ multi-weighted MSO-formulas. Note that negation and universal second order quantification are allowed in boolean formulas only. Note also that the boolean formulas have the same expressive power as (unweighted) MSO logic.
The class of almost boolean formulas over Σ and M is the smallest class containing all constants m ∈ M and all boolean formulas and which is closed under ∧ and ∨. A multi-weighted MSO formula ϕ is syntactically restricted if whenever it contains a subformula ∀xψ, then ψ is almost boolean, and if for every subformula ϕ 1 ∧ ϕ 2 of ϕ either both ϕ 1 and ϕ 2 are almost boolean, or ϕ 1 or ϕ 2 is boolean.
The set Free(ϕ) of free variables in ϕ is defined as usual.
where every first order variable is mapped to an element of dom(w) and every second order variable to a subset of dom(w).
The update for second order variables can be defined similarly. Each pair (w, σ) of a word and (V, w)-assignment can be encoded as a word over the extended alphabet Σ V = Σ × {0, 1} V . Note that a word (w, σ) ∈ Σ + V represents an assignment if and only if, for every first order variable in V, the corresponding row in the extended word contains exactly one 1; then (w, σ) is called valid. The set of all valid words in Σ + V is denoted by N V . We also denote by Σ ϕ the alphabet Σ Free(ϕ) . Consider again the collection N M of all finite multisets over M . Here, we consider the set of natural numbers as the semiring (N, +, ·, 0, 1) where + and · are usual addition and multiplication. The union (r 1 ⊕ r 2 ) ∈ N M of finite multisets r 1 , r 2 ∈ N M is defined by (r 1 ⊕ r 2 )(m) = r 1 (m) + r 2 (m) for all m ∈ M . We define the Cauchy product (r 1 · r 2 ) ∈ N M of two finite multisets r 1 , r 2 ∈ N M by Note that in the equation above there are finitely many non-zero summands, because the multisets r 1 and r 2 are finite. Let n ≥ 1 and r 1 , ..., r n ∈ N M . We also define the valuation val(r 1 , ..., r n ) ∈ N M by val(r 1 , ..., r n )(m) = Note that the right side of the equation above also contains only finitely many nonzero summands. The empty multiset ε is the finite multiset whose support is empty. A simple multiset over M is a finite multiset r ∈ N M such that supp(r) = {m r } and  As opposed to the case of pv-monoids [14], the pv-structure M does not contain a commutative and associative sum operation to define the semantics of the disjunction and the existential quantification. For this, we employ the sum of multisets. Let ϕ be a multi-weighted formula over Σ and M, and V ⊇ Free(ϕ). We define the auxiliary multiset semantics function ϕ V : Σ + V → N M relying on the ideas of [11] (cf. also [14]) as follows: for all (w, σ) / ∈ N V , ϕ V (w, σ) = ε and, for all (w, σ) ∈ N V , ϕ V (w, σ) is defined inductively as shown in Table 1. Here, x, y, X ∈ V, a ∈ Σ, m ∈ M , β is a boolean formula and ϕ, ϕ 1 , ϕ 2 are multi-weighted formulas. In Table 1, for the semantics of ∀Xϕ the subsets I ⊆ dom(w) are enumerated in some fixed order, e.g. lexicographically. For a formula ϕ, we put ϕ = ϕ Free(ϕ) . Then, we define the semantics ϕ : Σ + ϕ → K as the composition ϕ = Φ • ϕ .

Example 7.
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 Rvaluation structure (R 2 , val, Φ) from Example 5. We define ⋄ as the componentwise sum of vectors and put 1 = (0, 0). Then, M = (R 2 , val, ⋄, 1, Φ) is an R-pv-structure. Consider the following multi-weighted MSO sentence over the alphabet Σ = {↔, } and the R-pv-structure M: where, for a boolean formula ϕ and a multi-weighted formula ψ, β → ψ is an abbreviation for (β ∧ ψ) ∨ ¬β. For every sequence of commands w ∈ Σ + , the multiset ϕ (w) contains all possible displacement vectors of the object. For example, let w =↔↔. The object has 4 possibilities to move: 1) two steps to the right; 2) one step to the right and Note that the multi-weighted MSO logic over K-pv-structures contains the case of weighted MSO logic over semirings (cf. [10,11]). Hence, in general, multi-weighted MSO logic is expressively more powerful than multi-weighted automata.
Our main result for finite words is the following theorem. The proof is similar to the proof of the corresponding Theorem 17 for infinite words. For lack of space, we skip it.
We consider examples of decision problems for multi-weighted MSO logic.
Example 9. Let Σ be an alphabet and M = (Q × Q ≥0 , val, ⋄, (0, 0), Φ) the R-pvstructure where ⋄ is the componentwise sum, and val and Φ are defined as in Example 3. Let ϕ be a multi-weighted MSO sentence over Σ and M, and ν ∈ Q a threshold. The ≥ ν-emptiness problem is whether there exists a word w ∈ Σ + such that ϕ (w) ≥ ν.
If ϕ is syntactically restricted, then, using our Theorem 8, we can effectively translate ϕ into a multi-weighted automaton over Σ and M. Then ≥ν-emptiness for these multiweighted automata can be decided in the following way. First, we use a shortest path algorithm to decide whether there exists a path with cost 0, i.e. ||A||(w) = ∞ ≥ ν for some w. If this is not the case (i.e. the costs of all accepting paths in A are strictly positive), we use the same technique as for the ≥ν-emptiness problem for ratio automata with strictly positive costs (cf. [18], Theorem 3). We replace the weight (r, c) of every transition by the single value r − νc and obtain a weighted automaton A ′ over the maxplus semiring Q ∪ {−∞}. Then, ||A||(w) ≥ ν iff the semiring-behavior of A ′ on w is not less than zero. Then, the decidability of our problem follows from the decidability of the ≥0-emptiness problem for max-plus automata.
Example 10. Let Σ be an alphabet and M = (Q 2 , val, ⋄, (0, 0), Φ) where ⋄ is the componentwise sum, and val and Φ are as in Example 4. Again, using our Theorem 8, we can reduce the ≤ν-emptiness problem (defined similarly as in Example 9) for syntactically restricted multi-weighted MSO logic over Σ and M to the emptiness problem for multi-weighted automata. This problem is decidable, since the optimal conditional reachability for multi-priced timed automata is decidable [20].

Multi-weighted Automata and MSO Logic on Infinite Words
In A Muller automaton over an alphabet Σ is a tuple A = (Q, I, T, F ) where Q is a set of states, I ⊆ Q is a set of initial states, T ⊆ Q × Σ × Q is a transition relation and F ⊆ 2 Q is a Muller acceptance condition. Infinite paths π = (t i ) i∈ω of A are defined as infinite sequences of matching transitions, say t i = (q i , a i , q i+1 ). Then we call the word w = (a i ) i∈ω the label of the path π and π a path on w. We say that a path π = (q i , a i , q i+1 ) i∈ω is accepting if q 0 ∈ I and {q ∈ Q | q = q i for infinitely many i ∈ ω} ∈ F . Let Acc A (w) denote the set of all accepting paths of A on w.
Remark 13. The multiplication ⋄, the unital element 1 and the condition val ω (m1 ω ) = m are irrelevant for the definition of the behaviors of multi-weighted automata. However, they will be used to describe the semantics of multi-weighted MSO formulas.
We consider several examples of multi-weighted automata A over Σ and M, and their behaviors.

Example 14.
Consider the reward-cost ratio setting of Example 3 for infinite words. For a sequence (r i , c i ) i∈ω ∈ (R × R ≥0 ) ω of reward-cost pairs, the supremum ratio (cf. [5]) is defined by lim sup n→∞ n i=0 ri n i=0 ci ∈ R where r 0 = ∞. Unfortunately, since ∞ i=0 r i and ∞ i=0 c i may not exist or may be infinite, we cannot proceed as for finite words by considering pairs of accumulated rewards and costs and their ratios. Instead, we can define M as follows. Let M = R × R ≥0 , K = R and 1 = (0, 0).
The syntax of the multi-weighted MSO logic over Σ and M is defined exactly as for finite words (cf. Section 3). To define the semantics of this logic, we proceed similarly as for finite words, i.e. by means of the auxiliary multiset semantics. For this, we consider N as the totally complete semiring (N, +, ·, 0, 1) (cf. [11]) where 0 · ∞ = ∞ · 0 = 0. The sum ⊕ and the Cauchy product · for infinite multisets from N M are defined as for finite words. The ω-valuation val ω (r i ) i∈ω for r i ∈ N M is defined for all m ∈ M by Let ϕ be a multi-weighted MSO formula over Σ and M, and V ⊇ Free(ϕ). We define the auxiliary multiset semantics ϕ V : Σ ω V → N M inductively on the structure of ϕ as in Table 1 where we have to replace val by val ω . For w ∈ Σ ω , we let dom(w) = ω. To define the semantics ∀Xϕ , we have to extend val ω for multisets to index sets of size continuum such that val ω ((r i ) i∈I ) = ε whenever r i = ε for some i ∈ I, and val ω (( [1]) i∈I ) = [1]. The semantics of ϕ is defined by ϕ = Φ • ϕ .
Example 16. Assume that a bus can operate two routes A and B which start and end at the same place. The route R lasts t R time units and profits p R money units on the average per trip, for R ∈ {A, B}. 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 sense 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 K-ω-pv structure M from Example 14 and a one-element alphabet Σ = {τ } which is irrelevant here. Now we construct a weighted MSO sentence ϕ over Σ and M to define the optimal income of the bus per time unit (supremum ratio between rewards and time): where ∞ ∃ xψ is an abbreviation for a boolean formula ∀y(¬∀x(¬(y ≤ x ∧ ψ))). Here, the second order variable X corresponds to the set of positions in an infinite schedule For this, we can show that (N M , ⊕, val ω , ·, ε, [1]) is an ω-pv monoid as defined in [14]. Let D ⊆ N M . We denote by wMA(Σ, D) the collection of weighted automata over Σ and the ω-pv monoid N M where the weights of transitions are taken from D. Let wMSO res (Σ, D) denote the set of syntactically restricted sentences over Σ and the ω-pv monoid N M with constants from D. Let [[ϕ]] denote the semantics of ϕ ∈ wMSO res (Σ, M) as defined in [14]. The proof scheme of our result is depicted in Fig. 1. Here, ↔ means the expressive equivalence and → the expressive inclusion.
(i) If we replace the weight m ∈ M of every transition of a multi-weighted automaton A by the simple multiset [m] ∈ Mon(M ), we obtain a weighted automaton A ′ over the pv monoid N M such that the pv-monoid behavior of A ′ is equal to |A|. Conversely, we can replace the weights [m] in A ′ by m to obtain a multi-weighted automaton with the same behavior. (ii) Similarly to (i), we replace the constants m occurring in MSO formulas by simple multisets [m] and vice versa. (iii) The proof is based on the proof of Theorem 6.2 (a) of Droste and Meinecke [14]. We proceed inductively on the structure of ϕ ∈ wMSO res (Σ, Mon(M )).
Using the property val ω (m1 ω ) = m for m ∈ M , we show that every almost boolean formula is equivalent to a weighted Muller automaton with weights from ] is recognizable by a weighted automaton with weights from N M . (iv) The proof follows from Theorem 6.2 of [14] where a weighted automaton with weights in D ⊆ N M was translated into an MSO sentence with weights in D. • T ′ = T 1 ∪ T 2 , where T 1 consists of all transitions (p, a, (q, m, i)) from I × Σ × (Q ′ \ I) with (p, a, q) ∈ T ; T 2 consists of all transitions ((q 1 , m 1 , i 1 ), a, (q 2 , m 2 , i 2 )) from (Q ′ \ I) × Σ × (Q ′ \ I) with (q 1 , a, q 2 ) ∈ T . • For all t = (q ′ , a, (q, m, i)) ∈ T ′ , let γ ′ (t) = [m].