Filippo Bonchi

Marcello Bonsangue

Michele Boreale

Jan Rutten

Alexandra Silva

A Coalgebraic Perspective on Linear Weighted Automata

Weighted automata are a generalization of non-deterministic automata where each transition, in addition to an input letter, has also a quantity expressing the weight (e.g. cost or probability) of its execution. As for non-deterministic automata, their behaviours can be expressed in terms of either (weighted) bisimilarity or (weighted) language equivalence.

Coalgebras provide a categorical framework for the uniform study of state-based systems and their behaviours. In this work, we show that coalgebras can suitably model weighted automata in two different ways: coalgebras on Set (the category of sets and functions) characterize weighted bisimilarity, while coalgebras on V ect (the category of vector spaces and linear maps) characterize weighted language equivalence.

Relying on the second characterization, we show three different procedures for computing weighted language equivalence. The first one consists in a generalizion of the usual partition refinement algorithm for ordinary automata. The second one is the backward version of the first one. The third procedure relies on a syntactic representation of rational weighted languages.

Introduction

Weighted automata were introduced in Schützenberger's classical paper [START_REF] Paul | On the definition of a family of automata[END_REF]. They are of great importance in computer science [START_REF] Droste | Weighted automata and weighted logics[END_REF], arising in different areas of application, such as speech recognition [START_REF] Mohri | Finite-state transducers in language and speech processing[END_REF], image compression [START_REF] Albert | Handbook of Weighted Automata, chapter Digital Image Compression[END_REF], control theory [START_REF] Isidori | Nonlinear Control Systems[END_REF] and quantitative modelling [START_REF] Guldstrand | Bisimulation through probabilistic testing[END_REF][START_REF] Baier | Handbook of Weighted Automata, chapter Model Checking Linear-Time Properties of Probabilistic Systems[END_REF]. They can be seen as a generalization of non-deterministic automata, where each transition has a weight associated to it. This weight is an element of a semiring, representing, for example, the cost or probability of taking the transition.

The behaviour of weighted automata is usually given in terms of weighted languages (also called formal power series [START_REF] Salomaa | Automata-Theoretic Aspects of Formal Power Series[END_REF][START_REF] Berstel | Rational Series and Their Languages[END_REF]), that are functions assigning a weight to each finite string w ∈ A * over an input alphabet A. For computing the weight given to a certain word, the semiring structure plays a key role: the multiplication of the semiring is used to accumulate the weight of a path by multiplying the weights of each transition in the path, while the addition of the semiring computes the weight of a string w by summing up the weights of the paths labeled with w [START_REF] Kuich | Handbook of Formal Languages[END_REF]. Alternatively, the behaviour of weighted automata can be expressed in terms of weighted bisimilarity [START_REF] Buchholz | Bisimulation relations for weighted automata[END_REF], that is an extension of bisimilarity (for non-deterministic automata) subsuming several kinds of quantitative equivalences such as, for example, probabilistic bisimilarity [START_REF] Jou | Equivalences, congruences, and complete axiomatizations for probabilistic processes[END_REF]. As in the case of non-deterministic automata, (weighted) bisimilarity implies strictly (weighted) language equivalence.

Weighted automata still retain non-deterministic behavior, as two different transitions outgoing from the same state may be labelled by the same input action, possibly with different weights. Deterministic weighted automata are of interest because their construction is tightly connected with the existence of minimal automata recognizing the same weighted language. The classical powerset construction for obtaining a language-equivalent deterministic automaton from a non-deterministic one can be generalized to weighted automata, as long as the semiring respects certain restrictions [START_REF] Mohri | Handbook of Weighted Automata, chapter Weighted Automata Algorithms[END_REF][START_REF] Kirsten | On the determinization of weighted automata[END_REF]. The states of the determinized automaton are finite "subsets of weighted states" of the original non-deterministic automaton, or, more formally, functions from the set of states to the semiring that are almost everywhere zero. Differently from the classical case, though, the weighted automaton obtained by the powerset construction might be infinite. Usually, one restricts the attention to semirings for which determinization is guaranteed to terminate and produce a finite result, such as locally finite and tropical semirings, and extensions thereof [START_REF] Mohri | Handbook of Weighted Automata, chapter Weighted Automata Algorithms[END_REF][START_REF] Kirsten | On the determinization of weighted automata[END_REF].

In this paper, we study linear weighted automata, which are deterministic weighted automata where the set of states forms a vector space. A linear weighted automaton can be viewed as the result of determinizing an ordinary weighted automaton with weights in a generic field, using a weighted powerset construction. As such, linear weighted automata are typically infinite-state. The key point is that the linear structure of the state-space allows for finite representations of these automata and effective algorithms operating on them.

To be more specific, the goal of the present paper is to undertake a systematic study of the behavioural equivalences and minimization algorithms for (linear) weighted automata. To achieve this goal, we will benefit from a coalgebraic perspective on linear weighted automata. The theory of coalgebras offers a unifying mathematical framework for the study of many different types of state-based systems and infinite data structures. Given a functor G : C → C on a category C, a G-coalgebra is a pair consisting of an object X in C (representing the state space of the system) and a morphism f :X → GX (determining the dynamics of the system). Under mild conditions, functors G have a final coalgebra (unique up to isomorphism) into which every G-coalgebra can be mapped via a unique so-called G-homomorphism. The final coalgebra can be viewed as the universe of all possible G-behaviours: the unique homomorphism into the final coalgebra maps every state of a coalgebra to a canonical representative of its behaviour. This provides a general notion of behavioural equivalence (≈ G ): two states are equivalent if and only if they are mapped to the same element of the final coalgebra.

Our first contribution in this paper is to recast both weighted bisimilarity and weighted language equivalence in the theory of coalgebras. We see weighted automata for a field K and alphabet A, as coalgebras of the functor W = K × K -A on Set (the category of sets and functions). Concretely, a W-coalgebra consists of a set of states X and a function o, t : X → K × K X A where, for each state x ∈ X, o : X → K assigns an output weight in K and t : X → K X A assigns a function in K X A . For each symbol a ∈ A and state x ′ ∈ X, t(x)(a)(x ′ ) is a weight k ∈ K representing the weight of a transition from x to x ′ with label a, in symbols x a,k → x ′ . If t(x)(a)(x ′ ) = 0, then there is no a-labeled transition from x to x ′ . Note that there could exist several weighted transitions with the same label outgoing from the same state: x a,k1 → x 1 , x a,k2 → x 2 , . . . , x a,kn → x n . Adapting the above reasoning, we model linear weighted automata as coalgebras of the functor L = K × (-) A on V ect (the category of vector spaces and linear maps). A linear weighted automaton consists of a vector space V and a linear map o, t : V → K × V A where, as before, o : V → K defines the output and t : V → V A the transition structure. More precisely, for each v ∈ V and a ∈ A, t(v)(a) = v ′ means that there is a transition from v to v ′ with label a, in symbols v a → v ′ . Note that the transition structure is now "deterministic", since for each v and a there is only one v ′ ∈ V . When V = K X , each vector v ∈ V can be seen as a linear combination of states x 1 , . . . , x n ∈ X, i.e., v = k 1 x 1 + • • • + k n x n for some k 1 , . . . , k n ∈ K. Therefore, the transitions x a,k1 → x 1 , . . . , x a,kn → x n of a weighted automaton correspond to a single transition x a → (k 1 x 1 + • • • + k n x n ) of a linear weighted automaton. We show that ≈ W (i.e., the behavioural equivalence induced by W) coincides with weighted bisimulation while ≈ L coincides with weighted language equivalence. Determinization is the construction for moving from ordinary weighted automata and weighted bisimilarity to linear weighted automata and weighted language equivalence.

Once we have fixed the mathematical framework, we investigate three different types of algorithms for computing ≈ L . These algorithms work under the assumption that the underlying vector space has finite dimension. The first is a forward algorithm that generalizes the usual partition-refinement algorithm for ordinary automata: one starts by decreeing as equivalent states with the same output values, then refines the obtained relation by separating states for which outgoing transitions go to states that are not already equivalent. Linearity of the automata plays a crucial role to ensure termination of the algorithm. Indeed, the equivalences computed at each iteration can be represented as finite-dimensional sub-spaces in the given vector space. The resulting descending chain of sub-spaces must therefore converge in a finite number of steps, despite the fact that the state-space itself is infinite. We also show that each iteration of the algorithm coincides with the equivalence generated by each step of the (standard) construction of the final coalgebra via the final sequence. The minimal linear representations of weighted automata over a field was first considered by Schutzenberger [START_REF] Paul | On the definition of a family of automata[END_REF]. This algorithm was reformulated in a more algebraic and somewhat simplified fashion in Berstel and Reutenauer book [START_REF] Berstel | Rational Series and Their Languages[END_REF]. Their algorithm is different from our method, as it is related to the construction of a basis for a subgroup of a free group. Further, no evident connections can be traced between their treatment and the notions of bisimulation and coalgebras.

The second algorithm proceeds in a similar way, but uses a backward procedure. It has been introduced by the third authors together with linear weighted automata [START_REF] Boreale | Weighted bisimulation in linear algebraic form[END_REF]. In this case, the algorithm starts from the complement -in a precise geometrical sense -of the relation identifying vectors with equal weights. Then it incrementally computes the space of all states that are backward reachable from this relation. The largest bisimulation is obtained by taking the complement of this space. The advantage of this algorithm over the previous one is that the size of the intermediate relations is typically much smaller. The presentation of this algorithm in [START_REF] Boreale | Weighted bisimulation in linear algebraic form[END_REF] is somewhat more concrete, as there is no attempt at a coalgebraic treatment and the underlying field is fixed to R (for example, this leads to using orthogonal complements rather than dual spaces and annihilators, which we consider in Section 4). No connection is made with rational series.

Finally, the third algorithm is new and uses the fact that equivalent states are mapped by the unique homomorphism into the same element of the final coalgebra. We characterize the final morphism in terms of so-called rational weighted languages (which are also known as rational formal power series). This characterization is useful for the computation of the kernel of the final homomorphism, which consists of weighted language equivalence. Taking again advantage of the linear structure of our automata, calculating the kernel of the above homomorphism will correspond to solving a linear system of equations.

Structure of the paper. In Section 2 we introduce weighted automata and coalgebras. We also show that W-coalgebras characterize weighted automata and weighted bisimilarity. In Section 3.2, after recalling some preliminary notions of linear algebras, we show that each weighted automaton can be seen as a linear weighted automaton, i.e., an Lcoalgebra. This change of perspective allows us to coalgebraically capture weighted language equivalence. In Section 4, we show the forward and the backward algorithm while, in Section 5, we first introduce a syntactic characterization of rational weighted languages and then we shows how to employ it in order to compute ≈ L . In Section 6, after summarizing the main results of the paper, we discuss how to extend them to the case of automata with weights in a semiring.

Section 2.2 and Section 4.3 show some interesting minor results that could be safely skipped by the not interested reader. The presentation is self-contained and does not require any prior knowledge on the theory of coalgebras.

Weighted Automata as Coalgebras

We introduce weighted automata, weighted bisimilarity and their characterization as coalgebras over Set, the category of sets and functions.

First we fix some notation. We will denote sets by capital letter X, Y, Z . . . and functions by lower case f, g, h . . . . Given a set X, id X is the identity function and, given two functions f : X → Y and g : Y → Z, g • f is their composition. The product of two sets X, Y is X×Y with the projection functions π 1 :X×Y → X and π 2 :X×Y → Y . The product of two functions

f 1 : X 1 → Y 1 and f 2 : X 2 → Y 2 is f 1 × f 2 defined for all x 1 , x 2 ∈ X 1 × X 2 by (f 1 × f 2 ) x 1 , x 2 = f (x 1 ), f (x 2 ) . The disjoint union of X, Y is X + Y with injections κ 1 :X → X + Y and κ 2 :Y → X + Y . The union of f 1 : X 1 → Y 1 and f 2 : X 2 → Y 2 is f 1 + f 2 defined for all z ∈ X + Y by (f 1 + f 2 )(κ i (z)) = k i ((f i (z))) (for i ∈ {1, 2}). The set of functions ϕ : Y → X is denoted by X Y . For f : X 1 → X 2 , the function f Y : X Y 1 → X Y 2 is defined for all ϕ ∈ X Y 1 by f Y (ϕ) = λy ∈ Y.f (ϕ(y)).
The collection of finite subsets of X is denoted by P ω (X) and the emptyset by ∅. For a set of letters A, A * denotes the set of all words over A; ǫ the empty word; and w 1 w 2 the concatenation of words w 1 , w 2 ∈ A * .

We fix a field K. We use k 1 , k 2 , . . . to range over elements of K. The sum of K is denoted by +, the product by •, the additive identity by 0 and the multiplicative identity by 1. The support of a function ϕ from a set X to a field K is the set {x ∈ X | ϕ(x) = 0}.

Weighted automata [START_REF] Paul | On the definition of a family of automata[END_REF][START_REF] Droste | Weighted automata and weighted logics[END_REF] are a generalization of ordinary automata where transitions in addition to an input letter have also a weight in a field K and each state is not just accepting or rejecting but has an associated output weight in K. Formally, a weighted automaton (WA, for short) with input alphabet A is a triple (X, o, t ), where X is a set of states, o : X → K is an output function associating to each state its output weight and t : X → (K X ) A is the transition relation that associates a weight to each transition. We shall use the following notation:

x a,k → y means that t(x)(a)(y) = k. Weight 0 means no transition.
If the set of states is finite, a WA can be conveniently represented in form of matrices. First of all, we have to fix an ordering (x 1 , . . . , x n ) of the set of states X. Then the transition relation t can be represented by a family of matrices {T a } a∈A where each T a ∈ K n×n is an K-valued square matrix, with T a (i, j) specifying the value of the a-transition from x j to x i , i.e., t(x j )(a)(x i ). The output weight function o can be represented as an K-valued row vector in K 1×n that we will denote by the capital letter O.

For a concrete example, let K = R (the field of real numbers) and A = {a, b} and consider the weighted automata (X, o X , t X ) and (Y, o Y , t Y ) in Fig. 1. Their representation as matrix is the following.

O X = 1 1 1 T Xa =   1 0 0 1 3 0 1 0 3   T X b =   3 3 3 0 0 0 0 0 0   O Y = 1 T Ya = 3 T Y b = 3
Weighted bisimilarity generalizes the abstract semantics of several kind of probabilistic and stochastic systems. This has been introduced by Buchholz in [START_REF] Buchholz | Bisimulation relations for weighted automata[END_REF] for weighted automata with a finite state space. Here we extend that definition to (possibly infinite-states) automata with finite branching, i.e., those (X, o, t ) such that for all x ∈ X, a ∈ A, t(x)(a)(x ′ ) = 0 for finitely many x ′ . This is needed in the following to ensure that x ′ ∈X t(x)(a)(x ′ ) is always defined.

Hereafter we will always implicitly refer to weighted automata with finite branching. Moreover, given an x ∈ X and an equivalence relation R ⊆ X × X we will write [x] R to denote the equivalence class of x with respect to R. Definition 1. Let (X, o, t ) be a weighted automaton. An equivalence relation R ⊆ X×X is a weighted bisimulation if for all (x 1 , x 2 ) ∈ R, it holds that:

1. o(x 1 ) = o(x 2 ), 2. ∀a ∈ A, x ′ ∈ X, x ′′ ∈[x ′ ]R t(x 1 )(a)(x ′′ ) = x ′′ ∈[x ′ ]R t(x 2 )(a)(x ′′ ).
Weighted bisimilarity (in symbols ∼ w ) is defined as the largest weighted bisimulation.

For instance, the relation R h in Fig. 1 is a weighted bisimulation. Now, we will show that weighted automata and weighted bisimilarity can be suitably characterized through coalgebras [START_REF] Jan | Universal coalgebra: a theory of systems[END_REF].

We first recall some basic definitions about coalgebras. Given a functor G : C → C on a category C, a Gcoalgebra is an object X in C together with an arrow f : X → GX. For many categories and functors, such pair (X, f ) represents a transition system, the type of which is determined by the functor G. Viceversa, many types of transition systems (e.g., deterministic automata, labeled transition systems and probabilistic transition systems) can be captured by a functor.

A G-homomorphism from a G-coalgebra (X, f ) to a G-coalgebra (Y, g) is an arrow h : X → Y preserving the transition structure, i.e., such that the following diagram commutes.

X f h G G Y g GX Gh G G GY A G-coalgebra (Ω, ω) is said to be final if for any G-coalgebra (X, f ) there exists a unique G-homomorphism [[-]] G X : X → Ω.
Final coalgebra can be viewed as the universe of all possible G-behaviours: the unique homomorphism [[-]] G X : X → Ω maps every state of a coalgebra X to a canonical representative of its behaviour. This provides a general notion of behavioural equivalence: two states

x 1 , x 2 ∈ X are G-behaviourally equivalent (x 1 ≈ G x 2 ) iff [[x 1 ]] G X = [[x 2 ]] G X 1 .
The functors corresponding to many well known types of systems are shown in [START_REF] Jan | Universal coalgebra: a theory of systems[END_REF]. In this section we will show a functor W : Set → Set such that ≈ W coincides with weighted bisimilarity. In order to do that, we need to introduce the field valuation functor. Definition 2 (Field valuation Functor). Let K be a field. The field valuation functor K - ω : Set → Set is defined as follows. For each set X, K X ω is the set of functions from X to K with finite support. For each function h :

X → Y , K h ω : K X ω → K Y ω is the function mapping each ϕ ∈ K X ω into ϕ h ∈ K Y ω defined, for all y ∈ Y , by ϕ h (y) = x ′ ∈h -1 (y) ϕ(x ′ )
Note that the above definition employs only the additive monoid of K, i.e., the element 0 and the + operator. For this reason, such functor is often defined in literature (e.g., in [START_REF] Gumm | Monoid-labeled transition systems[END_REF]) for commutative monoids instead of fields. We need two further ingredients. Given a set B, the functor B × -: Set → Set maps every set X into B × X and every function f :

X → Y into id B × f : B × X → B × Y . Given a finite set A, the functor -A : Set → Set maps X into X A and f : X → Y into f A : X A → Y A .
Now, the functor corresponding to weighted automata with input alphabet A over the field K is W = K × (K - ω ) A : Set → Set. Note that every function f : X → W(X) consists of a pair of functions o, t with o : X → K and t : X → (K X ω ) A . Therefore any W-coalgebra (X, f ) is a weighted automata (X, o, t ) (and viceversa).

Proposition 1 ([34])

The functor W has a final coalgebra.

In order to show that the equivalence induced by the final W-coalgebra (≈ W ) coincides with weighted bisimilarity (∼ w ), it is instructive to spell out the notion of W-homomorphism.

A function h : X → Y is a W-homomorphism between weighted automata (X, o X , t X ) and (Y, o Y , t Y ) if the following diagram commutes. X oX ,tX h G G Y oY ,tY K × (K X ω ) A id×(K h ω ) A G G K × (K Y ω ) A This means that for all x ∈ X, y ∈ Y, a ∈ A, o X (x) = o Y (h(x)) and x ′ ∈h -1 (y) t X (x)(a)(x ′ ) = t Y (h(x))(a)(y).
For every

W-homomorphism h : (X, o X , t X ) → (Y, o Y , t Y ), the equivalence relation R h = {(x 1 , x 2 ) | h(x 1 ) = h(x 2 )
} is a weighted bisimulation. Indeed, by the properties of W-homomorphisms and by definition of R h , for all

(x 1 , x 2 ) ∈ R h o X (x 1 ) = o Y (h(x 1 )) = o Y (h(x 2 )) = o X (x 2 )
and for all a ∈ A, for all y ∈ Y

x ′′ ∈h -1 (y) t X (x 1 )(a)(x ′′ ) = t Y (h(x 1 ))(a)(y) = t Y (h(x 2 ))(a)(y) = x ′′ ∈h -1 (y) t X (x 2 )(a)(x ′′ ).
Trivially, the latter implies that for all x ′ ∈ X

x ′′ ∈[x ′ ]R h t X (x 1 )(a)(x ′′ ) = x ′′ ∈[x ′ ]R h t X (x 2 )(a)(x ′′ ).
For an example look at the function h depicted by the dotted arrows in Fig. 1: h is a W-homomorphism and R h is a weighted bisimulation.

Conversely, every bisimulation R on (X, o X , t X ) induces the coalgebra (X/R, o X/R , t X/R ) where X/R is the set of all equivalence classes of X w.r.t. R and o X/R : X/R → K and t X/R : X/R → (K

X/R ω ) A are defined for all x 1 , x 2 ∈ X, a ∈ A by o X/R ([x 1 ] R ) = o X (x 1 ) t X/R ([x 1 ] R )(a)([x 2 ] R ) = x ′ ∈[x2]R t X (x 1 )(a)(x ′ ).
Note that both o X/R and t X/R are well defined (i.e., independent from the choice of the representative) since R is a weighted bisimulation. Most importantly, the function ε

R : X → X/R mapping x into [x] R is a W-homomorphism. X oX ,tX [[-]] W X 8 8 εR G G X/R o X/R ,t X/R [[-]] W X/R G G Ω ω W(X) W([[-]] W X ) d d W(εR) G G W(X/R) W([[-]] W X/R ) G G W(Ω)
Theorem 1 Let (X, o, t ) be a weighted automaton and let x 1 , x 2 be two states in X. Then,

x 1 ∼ w x 2 iff x 1 ≈ W x 2 , i.e., [[x 1 ]] W X = [[x 2 ]] W X .
PROOF. The proof follows almost trivially from the above observations. If

x 1 ≈ W x 2 , i.e., [[x 1 ]] W X = [[x 2 ]] W X , then (x 1 , x 2 ) ∈ R [[-]] W X and R [[-]] W X is a weighted bisimulation because [[-]] W X is a W-homomorphism. Thus x 1 ∼ w x 2 If x 1 ∼ w x 2 , then there exists a weighted bisimulation R such that (x 1 , x 2 ) ∈ R. Let (X/R, o X/R , t X/R
) and ε R : X → X/R be the W-coalgebra and the W-homomorphism described above. Since there exists a unique W-homomorphism from (X, o X , t X ) to the final coalgebra, then

[[-]] W X = [[-]] W X/R • ε R . Since ε R (x 1 ) = ε R (x 2 ), then [[x 1 ]] W X = [[x 2 ]] W X , i.e., x 1 ≈ W x 2 .

Weighted language equivalence

The semantics of weighted automata can also be defined in terms of weighted languages. A weighted language over A and K is a function σ : A * → K assigning to each word in A * a weight in K. For each WA (X, o, t ), the function l X : X → K A * assigns to each state x ∈ X its recognized weighted language. For all words a 1 . . . a n ∈ A * , it is defined by Although they are all language equivalent, they are not bisimilar.

l X (x)(a 1 . . . a n ) = {k 1 • . . . • k n • k | x = x 1 a1,k1 → . . . an,kn → x n and o(x n ) = k}. x 1 x 2 x 3 x 4 x 5 0 0 2 0 0 a, 1 a, 1 a, 1 a, 1 x 1 x 2 x 3 x 5 0 0 2 0 a, 1 a, 1 a, 1 x 1 x 2 x 3 0 0 2 a, 1 a, 1 x 1 x 2 x 3 0 0 1 a, 1 a, 2
We will often use the following characterization: for all w ∈ A ⋆ ,

l X (x)(w) = o(x), if w = ǫ; x ′ ∈X (t(x)(a)(x ′ ) • l X (x ′ )(w ′ )), if w = aw ′ .
Two states x 1 , x 2 ∈ X are said to be weighted language equivalent (denoted by

x 1 ∼ l x 2 ) if l X (x 1 ) = l X (x 2 )
. In [START_REF] Buchholz | Bisimulation relations for weighted automata[END_REF], it is shown that if two states are weighted bisimilar then they are also weighted language equivalent. For completeness, we recall here the proof.

Proposition 2 ∼ w ⊆∼ l PROOF. We prove that if R is a weighted bisimulation, then for all (x 1 , x 2 ) ∈ R, l X (x 1 ) = l X (x 2 ). We use induction on words w ∈ A * . If w = ǫ, then l X (x 1 )(w) = o(x 1 ) and l X (x 2 )(w) = o(x 2 ) and o(x 1 ) = o(x 2 ) since R is a weighted bisimulation. If w = aw ′ , then l X (x 1 )(w) = x ′ ∈X (t(x 1 )(a)(x ′ ) • l X (x ′ )(w ′ )).
By induction hypothesis for all

x ′′ ∈ [x ′ ] R , l X (x ′′ )(w ′ ) = l X (x ′ )(w ′ ).
Thus in the above summation we can group all the states x ′′ ∈ [x ′ ] R as follows.

l X (x 1 )(w) = [x ′ ]R∈X/R   l X (x ′ )(w ′ ) •   x ′′ ∈[x ′ ]R t(x 1 )(a)(x ′′ )     Since (x 1 , x 2 ) ∈ R
and R is a weighted bisimulation, the above summation is equivalent to

[x ′ ]R∈X/R   l X (x ′ )(w ′ ) •   x ′′ ∈[x ′ ]R t(x 2 )(a)(x ′′ )    
that, by the previous arguments, is equal to l X (x 2 )(w).

The inverse inclusion does not hold: all the states x 1 in Fig. 2 are language equivalent but they are not equivalent according to weighted bisimilarity.

On the difference between W-bisimilarity and W-behavioural equivalence

We conclude this section with an example showing the difference between W-behavioral equivalence (and hence weighted bisimulation) and another canonical equivalence notion from the theory of coalgebra, namely Wbisimulation. This result is not needed for understanding the next sections, and therefore this sub-section can be safely skipped.

The theory of coalgebras provides an alternative definition of equivalence, namely G-bisimilarity (≃ G ), that coincides with G-behavioural equivalence whenever the functor G preserves weak pullbacks [START_REF] Jan | Universal coalgebra: a theory of systems[END_REF]. In the case of weighted automata, the functor W does not preserve weak pullbacks and ≃ W is strictly included into ≈ W . Since weighted automata are one of the few interesting cases where this phenomenon arises, we now show an example of two states that are in ≈ W , but not in ≃ W (the paper [START_REF] Gumm | Copower functors[END_REF] was of great inspiration in the construction of this example).

x 1 First, let us instantiate the general coalgebraic definition of bisimulation and bisimilarity to the functor

x 2 x 3 z 1 z 2 y 1 0 1 1 0 1 0 a, 1 a, -1
W. A W-bisimulation between two W-coalgebras (X, o X , t X ) and (Y, o Y , t Y ) is a relation R ⊆ X × Y such that there exists o R , t R : R → W(R) making the following diagram commute. The biggest W-bisimulation is called W-bisimilarity (≃ W ). X oX ,tX R π1 o o oR,tR π2 G G Y oY ,tY W(X) W(R) W(π1) o o W(π2) G G W(Y )
Note that the actual definition of ≈ W relates the states of a single automaton. We can extend it in order to relate states of possibly distinct automata: given

(X, o X , t X ) and (Y, o Y , t Y ), the states x ∈ X and y ∈ Y are equivalent w.r.t. ≈ W iff [[x]] W X = [[y]] W Y .
Consider now the coalgebras in Fig. 3:

x 1 ≈ W y 1 , but x 1 ≃ W y 1 .
For the former, it is enough to observe that the function h 1 and h 2 (represented by the dashed arrows) are W-homomorphisms, and by uniqueness of

[[-]] W : [[x 1 ]] W X = [[h 1 (x 1 )]] W Z = [[z 1 ]] W Z = [[h 2 (y 1 )]] W Z = [[y 1 ]] W Y .
For x 1 ≃ W y 1 , note that there exists no R ⊆ X × Y that is a W-bisimulation and such that (x 1 , y 1 ) ∈ R. Since x 2 and x 3 are both different from y 1 (their output values are different), then neither (x 2 , y 1 ) nor (x 3 , y 1 ) can belong to a bisimulation. Thus the only remaining relation on X × Y is the one equating just x 1 and y 1 , i.e., R = {(x 1 , y 1 )}. But this is not a W-bisimulation since there exists no o R , t R making the leftmost square of the above diagram commute. In order to understand this fact, note that π -1 1 (x 2 ) = ∅ and π -1 1 (x 3 ) = ∅. Thus for all possible choices of o R , t R , the function W(π 1 ) • o R , t R maps (x 1 , y 1 ) into a pair k, ϕ where ϕ(a)(x 2 ) = 0 and ϕ(a)(x 3 ) = 0. On the other side of the square, we have that o

X , t X • π 1 (x 1 , y 1 ) = o X (x 1 ), t X (x 1 ) and t X (x 1 )(a)(x 2 ) = 1 and t X (x 1 )(a)(x 3 ) = -1.

Linear Weighted Automata as Linear Coalgebras

In this section we will introduce linear weighted automata as coalgebras for an endofunctor L : V ect → V ect, where V ect is the category of vector spaces and linear maps over a field K. The goal of this change is to characterize weighted language equivalence as the behavioural equivalence induced by the final L-coalgebra.

Preliminaries

First we fix some notations and recall some basic facts on vector spaces and linear maps. We use v 1 , v 2 , . . . to range over vectors and V, W . . . to range over vector spaces on a field K. Given a vector space V , a vector v ∈ V and a k ∈ K, the scalar product is denoted by k • v (or kv for short). The space spanned by an I-indexed family of vectors

B = {v i } i∈I is the space span(B) of all v such that v = k 1 v i1 + k 2 v i2 + • • • + k n v in
where for all j, v ij ∈ B. In this case, we say that v is a linear combination of the vectors in B. A set of vectors is linearly independent if none of its elements can be expressed as the linear combination of the remaining ones. A basis for the space V is a linearly independent set of vectors that spans the whole V . All the basis of V have the same cardinality which is called the dimension of V (denoted by dim(V )).

If (v 1 , . . . v n ) is a basis for V , then each vector v ∈ V is equal to k 1 v 1 + • • • + k n v n for some k 1 , . . . , k n ∈ K. For this reason, each vector v can be represented as a n × 1-column vector v =    k 1 . . . k n   
We use f, g, . . . to range over linear maps. Identity and composition of maps are denoted as usual. If B V = (v 1 , . . . v n ) and B W = (w 1 . . . w m ) are, respectively, the basis for the vector spaces V and W , then every linear map f :

V → W can be represented as m × n-matrix. Indeed, for each v ∈ V , v = k 1 v 1 + • • • + k n v n and f (v) = k 1 f (v 1 ) + • • • + k n f (v n )
, by linearity of f . For each v i , f (v i ) can be represented as m × 1 column vector by taking as basis B W . Thus the matrix corresponding to f (w.r.t. B V and B W ) is the one having as i-th column the vector corresponding to f (v i ). In this paper we will use capital letters F, G . . . to denote the matrices corresponding to linear maps f, g . . . in lower case. By multiplying the matrix F for the vector v (in symbols, F ×v) we can compute f (v). More generally, matrix multiplication corresponds to composition of linear maps, in symbols:

g • f = G × F
The product of two vector spaces V, W is written as V × W , and the product of two linear maps f 1 , f 2 is f 1 × f 2 , defined as for functions. It will be clear from the context whether × refer to multipliaction of matrix or product of spaces (or maps). Given a set X, and a vector space V , the set V X (i.e., the set of functions ϕ : X → V ) carries a vector space structure where sum and scalar product are defined point-wise. Hereafter we will use V X to denote both the vector space and the underlying carrier set. Given a linear map

f : V 1 → V 2 , the linear map f X : V X 1 → V X 2 is defined as for functions. If A is a finite set we can conveniently think V A as the product of V with itself for |A|-times (|A| is the cardinality of A). A linear map f : U → V A can be decomposed in a family of maps indexed by A, f = {f a : U → V } a∈A , such that for all u ∈ U , f a (u) = f (u)(a).
For a set X, the set K X ω (i.e., the set of all finite support functions ϕ : X → K) carries a vector space where sum and scalar product are defined in the obvious way. This is called the free vector space generated by X and can be thought of as the space spanned by the elements of X: each vector

k 1 x i1 + k 2 x i2 + • • • + k n x in corresponds to a function ϕ : X → K such that ϕ(x ij ) = k j and for all x / ∈ {x ij }, ϕ(x) = 0; conversely, each finite support function ϕ corresponds to a vector ϕ(x i1 )x i + ϕ(x i2 )x i2 + • • • + ϕ(x in )x in .
A fundamental property holds in the free vector space generated by X: for all functions f from X to the carrier-set of a vector space V , there exists a linear map f ♯ :

K X ω → V that is called the linearization of f . For all v ∈ K X ω , v = k 1 x i1 + k 2 x i2 + • • • + k n x in and f ♯ (v) = k 1 f (x i1 ) + k 2 f (x i2 ) + • • • + k n f (x in ). K X ω f ♯ 8 8 N N N N N N N N N N N N N X f G G ηX y y V Note that f ♯ is the only linear map such that f = f ♯ • η X , where η X (x)
is the function assigning 1 to x and 0 to all the other elements of X.

The kernel ker(f ) of a linear map f :

V → W is the subspace of V containing all the vectors v ∈ V such that f (v) = 0. The image im(f ) of f is the subspace of W containing all the w ∈ W such that w = f (v) for some v ∈ V .
If V has finite dimension, the kernel and the image of f are related by the following equation:

dim(V ) = dim(ker(f )) + dim(im(f )) .
(1)

Given two vector spaces V 1 and V 2 , their intersection V 1 ∩ V 2 is still a vector space, while their union V 1 ∪ V 2 is not.
Instead of union we consider the coproduct of vector spaces: we write

V 1 + V 2 to denote the space span(V 1 ∪ V 2 )
(note that in the category of vector spaces, product and coproduct coincide).

From Weighted Automata to Linear Weighted Automata

We have now all the ingredients to introduce linear weighted automata and a coalgebraic characterization of weighted language equivalence.

Definition 3 (LWA).

A linear weighted automaton (LWA, for short) with input alphabet A over the field K is a coalgebra for the functor L = K × -A : V ect → V ect.

More concretely [START_REF] Boreale | Weighted bisimulation in linear algebraic form[END_REF], a LWA is a triple (V, o, t ), where V is a vector space (representing the states space), o : V → K is a linear map associating to each state its output weight and t : V → V A is a linear map that for each input a ∈ A associates a next state (i.e., a vector) in V . We will write v

1 a → v 2 for t(v 1 )(a) = v 2 .
The behaviour of linear weighted automata is expressed in terms of weighted languages. The language recognized by a vector v ∈ V of a LWA (V, o, t ) is defined for all words a 1 . . .

a n ∈ A * as [[v]] L V (a 1 . . . a n ) = o(v n )
where v n is the vector reached from v through a 1 . . . a n , i.e., v a1 → . . . an → v n . We will often use the following (more compact) definition: for all w ∈ A ⋆ ,

[[v]] L V (w) = o(v), if w = ǫ; [[t(v)(a)]] L V (w ′ ), if w = aw ′ .

Here we use the notation [[-]] L

V because this is the unique L-homomorphism into the final L-coalgebra. In Section 3.3, we will provide a proof for this fact and we will also discuss the exact correspondence with the function l X introduced in Section 2.

Given a weighted automaton (X, o, t ), we can build a linear weighted automaton (K X ω , o ♯ , t ♯ ), where K X ω is the free vector space generated by X and o ♯ and t ♯ are the linearizations of o and t. If X is finite, we can represent t ♯ and o ♯ by the same matrices that we have introduced in the previous section for t and o. By fixing an ordering x 1 , . . . , x n of the states in X, we have a basis for K X ω , i.e., every

vector v ∈ K X ω is equal to k 1 x 1 + • • • + k n
x n and it can be represented as an n × 1-column vector. The values t ♯ (v)(a) and o ♯ (v) can be computed via matrix multiplication as T a × v and O × v.

For a concrete example, look at the weighted automaton (X, o X , t X ) in Fig. 1. The corresponding linear weighted automaton (R X ω , o ♯ X , t ♯ X ) has as state space the space of all the linear combinations of the states in X (i.e., {k

1 x 1 + k 2 x 2 + k 3 x 3 | k i ∈ R}). The function o ♯ X maps v = k 1 x 1 + k 2 x 2 + k 3 x 3 into k 1 o X (x 1 ) + k 2 o X (x 2 ) + k 3 o X (x 3 ), i.e., k 1 + k 2 + k 3 .
By exploiting the correspondence between functions and vectors in K X ω (discussed in Section 3.1), we can write t

♯ X (v)(a) = k 1 t X (x 1 )(a) + k 2 t X (x 2 )(a) + k 3 t X (x 3 )(a) that is k 1 (x 1 + x 2 + x 3 ) + k 2 3x 2 + k 3 3x 3 and t ♯ X (v)(b) = k 1 3x 1 + k 2 3x 1 + k 3 3x 1 .
This can be conveniently expressed in terms of matrix multiplication.

o ♯ X (v) = 1 1 1   k 1 k 2 k 3   t ♯ X (v)(a) =   1 0 0 1 3 0 1 0 3     k 1 k 2 k 3   t ♯ X (v)(b) =   3 3 3 0 0 0 0 0 0     k 1 k 2 k 3   A linear map h : V → W is an L-homomorphism between LWA (V, o V , t V ) and (W, o W , t W ) if the following diagram commutes. V oV ,tV h G G W oW ,tW K × V A id×h A G G K × W A This means that for all v ∈ V, a ∈ A, o V (v) = o W (h(v)) and h(t V (v)(a)) = t W (h(v))(a)
. If V and W have finite dimension, then we can represent all the morphisms of the above diagram as matrices. In this case, the above diagram commutes if and only if for all a ∈ A,

O V = O W × H H × T Va = T Wa × H
where T Va and T Wa are the matrix representation of t V and t W for any a ∈ A.

x 1

x 2 x 3 1 1 1 a, 1 a, -1 a, 1 a, 1 x 1 + x 2 x 2 + x 3 x 1 + x 3 2 2 2 a, 3 2 a, 1 2 a, -3 2 a, 1 a, 1
(R X ω , o ♯ X , t ♯ X ) and (R Y ω , o ♯ Y , t ♯ Y ) are isomorphic.
For a function h : X → Y , the function

K h : K X → K Y (formally introduced in Definition 2) is a linear map. Note that if h is a W-homomorphism between the WA (X, o X , t X ) and (Y, o Y , t Y ), then K h is an L- homomorphism between the LWA (K X , o ♯ X , t ♯ X ) and (K Y , o ♯ Y , t ♯ Y ). For an example, look at the W-homomorphism h : (X, o X , t X ) → (Y, o Y , t Y ) represented by the dotted arrows in Fig. 1. The linear map R h : R X → R Y is represented by the matrix H = (1 1 1) and it is an L-homomorphism between (R X , o ♯ X , t ♯ X ) and (R Y , o ♯ Y , t ♯ Y ).

This can be easily checked by showing that

O X = O Y × H, H × T Xa = T Ya × H and H × T X b = T Y b × H.
Note that two different weighted automata can represent the same (up to isomorphism) linear weighted automaton. As an example, look at the weighted automata (X, o X , t X ) and (Y, o Y , t Y ) in Fig. 4. They represent, respectively, the linear weighted automata

(R X ω , o ♯ X , t ♯ X ) and (R Y ω , o ♯ Y , t ♯ Y
) that are isomorphic. The transitions and the output functions for the two automata are described by the following matrices.

T Xa =   0 0 0 1 1 0 -1 0 1   O X = 1 1 1 T Ya =   3 2 0 1 2 1 2 1 1 2 -3 2 0 -1 2   O Y = 2 2 2
Note that T Xa and T Ya are similar, i.e., they represent the same linear map. This can be immediately checked by showing that T Ya = j -1 • t Xa • j, where j : R Y → R X is the isomorphic map representing the change of bases form Y = (x 1 + x 2 , x 2 + x 3 , x 3 + x 1 ) to X = (x 1 , x 2 , x 3 ) and j -1 : R X → R Y is its inverse. The matrix representation of j and j -1 is the following.

J =   1 0 1 1 1 0 0 1 1   J -1 =   1 2 1 2 -1 2 -1 2 1 2 1 2 1 2 -1 2 1 2   Also O X and O Y represents the same map in different bases. Indeed, O Y = O X × J.
At this point, it is easy to see that the linear isomorphism j

-1 : R X → R Y is an L-homomorphism, because O X = O X × J × J -1 = O Y × J -1 and J -1 × T Xa = J -1 × T Xa × J × J -1 = T Ya × J -1 . Analogously for j : R Y → R X .

Language equivalence and final L-coalgebra

We introduce the final L-coalgebra and we show that the behavioural equivalence ≈ L , induced by the functor L, coincides with weighted language equivalence.

The set of all weighted languages K A * carries a vector space structure: the sum of two languages σ 1 , σ 2 ∈ K A * is the language σ 1 + σ 2 defined for each word w ∈ A * as σ 1 + σ 2 (w) = σ 1 (w) + σ 2 (w); the product of a language σ for a scalar k ∈ K is kσ defined as kσ(w) = k • σ(w); the element 0 of K A * is the language mapping each word into the 0 of K.

The empty function ǫ : K A * → K and the derivative function d :

K A * → (K A * ) A are defined for all σ ∈ K A * , a ∈ A as ǫ(σ) = σ(ǫ) d(σ)(a) = σ a which, by linearity of [[-]] L K X ω , coincides with x ′ ∈X t(x)(a)(x ′ ) • [[x ′ ]] L K X ω (w ′ ). By induction hypothesis [[x ′ ]] L K X ω (w ′ ) = l X (x ′ )(w ′
) and thus the above coincides with

x ′ ∈X t(x)(a)(x ′ ) • l X (x ′ )(w ′ )
that is l X (x)(w).

Proposition 4 Let (X, o, t ) be a WA and (K X ω , o ♯ , t ♯ ) be the corresponding linear weighted automaton. Then, for

all v = k 1 x i1 + • • • + k n x in , [[v]] L K X ω = k 1 l X (x i1 ) + • • • + k n l X (x in ).

PROOF. By induction on w

∈ A * . If w = ǫ, then [[v]] L K X ω (w) = o ♯ (v). Since o ♯ is a linear map and X is a base for K X ω , o ♯ (v) = k 1 o(x i1 ) + • • • + k n o(x in ). For all j, l X (x ij )(ǫ) = o(x ij ), thus k 1 o(x i1 ) + • • • + k n o(x in ) = k 1 l X (x i1 )(w) + • • • + k n l X (x in )(w). If w = aw ′ , then [[v]] L K X ω (w) = [[t ♯ (v)(a)]] L K X ω (w ′ ). Since t ♯ is linear and X is a base for K X ω , then t ♯ (v)(a) = k 1 t(x i1 )(a) + • • • + k n t(x in )(a). For all j, t(x ij )(a) = x ′ ∈X t(x ij )(a)(x ′ ) • x ′ , thus [[t ♯ (v)(a)]] L K X ω (w ′ ) is equal to k 1 x ′ ∈X t(x ij )(a)(x ′ ) • x ′ + • • • + k n x ′ ∈X t(x ij )(a)(x ′ ) • x ′ L K X ω (w ′ ) which, by linearity of [[-]] L K X ω , is equal to k 1 x ′ ∈X t(x ij )(a)(x ′ ) • [[x ′ ]] L K X ω (w ′ ) + • • • + k n x ′ ∈X t(x ij )(a)(x ′ ) • [[x ′ ]] L K X ω (w ′ ) . By induction hypothesis [[x ′ ]] L K X ω (w ′ ) = l X (x ′ )(w ′
) and thus the latter coincides with

k 1 x ′ ∈X t(x ij )(a)(x ′ ) • l X (x ′ )(w ′ ) + • • • + k n x ′ ∈X t X (x ij )(a)(x ′ ) • l X (x ′ )(w ′ ) . By definition, l X (x ij )(w) = x ′ ∈X t(x ij )(a)(x ′ ) • l X (x ′ )(w ′
) and thus we can concisely express the above formula as

k 1 l X (x 1 )(w) + • • • + k n l X (x n )(w).

Linear Bisimulations and Subspaces

We now introduce a convenient characterization of language equivalence by means of linear weighted bisimulations. Differently form ordinary (weighted) bisimulations, these can be seen both as relations and as subspaces. The latter characterization will be exploited in the next section for defining an algorithm for checking language equivalence.

First, we show how to represent relations over a vector space V as sub-spaces of V , following [START_REF] Stark | On behaviour equivalence for probabilistic i/o automata and its relationship to probabilistic bisimulation[END_REF][START_REF] Boreale | Weighted bisimulation in linear algebraic form[END_REF].

Definition 4 (linear relations).

Let U be a sub-space of V . The binary relation R U over V is defined by

v 1 R U v 2 if and only if v 1 -v 2 ∈ U . A relation R is linear if there is a subspace U such that R = R U .
Note that a linear relation is a total equivalence relation on V . Let now R be any binary relation over V . There is a canonical way of turning R into a linear relation, which we describe in the following. The kernel of R (in symbols ker(R)) is the set

{v 1 -v 2 | v 1 R v 2 }. The linear extension of R, denoted R ℓ , is defined by: v 1 R ℓ v 2 if and only if (v 1 -v 2 ) ∈ span(ker(R)).
Lemma 2 Let U be a sub-space of V , then ker(R U ) = U .

According to the above lemma, a linear relation R is completely described by its kernel, which is a sub-space, that is

v 1 R v 2 if and only if (v 1 -v 2 ) ∈ ker(R) . (2)
Conversely, for any sub-space U ⊆ V there is a corresponding linear relation R U whose kernel is U . Hence, without loss of generality, we can identify linear relations on V with sub-spaces of V . For example, by slight abuse of notation, we can write

v 1 U v 2 instead of v 1 R U v 2 ;
and conversely, we will sometimes denote by R the sub-space ker(R). The context will be sufficient to tell whether we are actually referring to a linear relation or to the corresponding sub-space (kernel). Note that the sub-space {0} corresponds to the identity relation on

V , that is R {0} = Id V . In fact: v 1 Id V v 2 iff v 1 = v 2 iff v 1 -v 2 = 0. Similarly, the space V itself corresponds to R V = V × V .
We are now ready to define linear weighted bisimulation. This definition relies on the familiar step-by-step game played on transitions, plus an initial condition requiring that two related states have the same output weight. We call this form of bisimulation linear to stress the difference with the one introduced in Definition 1.

Definition 5 (linear weighted bisimulation

). Let (V, o, t ) be a linear weighted automaton. A linear relation R ⊆ V × V is a linear weighted bisimulation if for all (v 1 , v 2 ) ∈ R, it holds that: (1) o(v 1 ) = o(v 2 ), (2) ∀a ∈ A, t(v 1 )(a) R t(v 2 )(a).

For a concrete example, consider the automaton

(R X ω , o ♯ X , t ♯ X ) in Fig 4. The relation R = {(x 2 , x 3 )} is not linear, because U = {x 2 -x 3 } is not a subspace of R X
ω . However, we can turn R into a linear relation by employing its kernel ker

(R) = {x 2 -x 3 }. The linear extension of R is R ℓ = {(k 1 x 1 + k 2 x 2 + k 3 x 3 , k ′ 1 x 1 + k ′ 2 x 2 + k ′ 3 x 3 ) | k 1 = k ′ 1 and k 2 + k 3 = k ′ 2 + k ′ 3 }.
It is easy to see that R ℓ is a linear weighted bisimulation. The following lemma provides a characterization of linear weighted bisimulation as a subspace. Let us say that a sub-space U is f -invariant if f (U ) ⊆ U . Bisimulations are transition-invariant relations that refine the kernel of the output map o. Lemma 3 Let (V, o, t ) be a LWA and R be linear relation over V . R is a linear weighted bisimulation if and only if

(1) R ⊆ ker(o), (2) R is t a -invariant for each a ∈ A.
This lemma will be fundamental in the next section for defining an algorithm computing the greatest linear weighted bisimulation. In the remainder of this section, we show that the greatest linear weighted bisimulation coincides with the kernel of the final map [[-]] L V . More generally, the kernel of each L-homomorphism is a linear weighted bisimulation R and, viceversa, for each linear weighted bisimulation R there exists an L-homomorphism whose kernel is R.

Proposition 5 Let (V, o V , t V ) be a LWA. If f : V → W is an L-homomorphism (for some LWA (W, o W , t W ))
then ker(f ) is a linear weighted bisimulation. Conversely, if R is a linear weighted bisimulation for (V, o, t ), then there exists a LWA (W, o W , t W ) and an L-homomorphism f : V → W such that ker(f ) = R.

PROOF. First, we suppose that f : V → W is an L-homomorphism and we prove that ker(f ) satisfies ( 1) and (2) of Lemma 3. Take a vector v ∈ ker(f ). Thus, f (v) = 0 and, since o W and t W are linear maps, o W (f (v)) = 0 and t W (f (v))(a) = 0 for all a ∈ A. Since f is an L-homomorphism, we have that [START_REF] Adámek | Abstract and Concrete Categories -The Joy of Cats[END_REF]

o V (v) = o W (f (v)) = 0, i.e., ker(f ) ⊆ ker(o V ) and (2) f (t V (v)(a)) = t W (f (v))(a) = 0 meaning that t V (v)(a) ∈ ker(f ), i.e., ker(f ) is t Va -invariant.
In order to prove the second part, we need to recall quotient spaces and quotient maps from [START_REF] Halmos | Finite dimensional vector spaces[END_REF]. Given a subspace U of V , the equivalence class of v w.r.

t. U is [v] U = {v + u | u ∈ U }. Note that v 1 ∈ [v 2 ] U if and only if v 1 R U v 2 .
The quotient space V /U is the space of all equivalence classes [v] U where scalar product k[v] U is defined as [kv] U and the sum

[v 1 ] U + [v 2 ] U as [v 1 + v 2 ] U .
It is easy to check that these operations are well-defined (i.e., independent from the choice of the representative) and turn V /U into a vector space where the element 0 is U . Most importantly, the quotient function ε U : V → V /U mapping each vector v into [v] U is a linear map such that ker(ε U ) = U . Now, let U be the subspace corresponding to the linear weighted bisimulation R. We can take W = V /U and we

define o W as o W ([v] U ) = o V (v) and t W as t W ([v] U )(a) = [t(v)(a)] U . Note that both o W and t W are well defined: for all v ′ ∈ [v] U = {v +u | u ∈ U }, o W (v ′ ) = o W (v) (since o V (u) = 0 for all u ∈ U ) and t W (v ′ )(a) ∈ [t W (v)(a)] U (since t V (u)(a) ∈ U for all u ∈ U ).
It is also easy to check that they are linear.

Finally, we take f : V → W as ε U and with the previous definition o W and t W is trivial to check that ε U is an L-homomorphism. As said above, its kernel is U .

Theorem 3 Let (V, o, t ) be a LWA and let [[-]] L V : V → K A * be the unique L-morphism into the final coalgebra. Then ker([[-]] L V )
is the largest linear weighted bisimulation on V .

PROOF. First of all, note that by the first part of Proposition 5, ker([[-]] L V ) is a linear weighted bisimulation. Then suppose that R is a linear weighted bisimulation. By the second part of Proposition 5, there exists a LWA (W, o W , t W ) and an L-homomorphism f :

V → W such that R = ker(f ). Now note that, since (W, o W , t W ) is an L-coalgebra there exists an L-homomorphism [[-]] L W : W → K A * to the final coalgebra. Since the composition of two L-homomorphisms is still an L-homomorphism, also [[-]] L W • f : V → K A * is an L-homomorphism. Since [[-]] L V is the unique L-homomorphism from V to K A * , then [[-]] L W • f = [[-]] L V . Finally, R = ker(f ) ⊆ ker([[-]] L W • f ) = ker([[-]] L V ).
The characterization of bisimulations as subspaces seems to be possible in V ect and not in Set because the former category is abelian [START_REF] Freyd | Abelian categories[END_REF]: every map has a kernel that is a subspace and every subspace is the kernel of some map. We leave as future work to study (at a more general level) the categorical machinery allowing to characterize bisimulations as subspaces.

Linear Partition Refinement

In the previous section, we have shown that weighted language equivalence (∼ l ) can be seen as the largest linear weighted bisimulation. In this section, we exploit this characterization in order to provide a "partition refinement" algorithm that allows to compute ∼ l . We will examine below two versions of the algorithm, a forward version (Section 4.1) and a backward one (Section 4.2). The former is straightforward but computationally not very convenient; the latter is more convenient, although it requires the introduction of some extra machinery. In both cases, we must restrict to LWA's where the state space is finite dimension.

A forward algorithm

Lemma 3 suggests that, in order to compute the largest linear weighed bisimulation for a LWA (V, o, t ), one might start from ker(o) and refine it until the condition (2) given in the lemma is satisfied. This is indeed the case.

Proposition 6 (partition refinement, forward version)

Let (V, o, t ) be a LWA. Consider the sequence (R i ) i≥0 of sub-spaces of V defined inductively by R 0 = ker(o) R i+1 = R i ∩ a∈A t(R i )(a) -1 where t(R i )(a) -1 is the space {v ∈ V | t(v)(a) ∈ R i }. Then there is j ≤ dim(V ) such that R j+1 = R j . The largest linear weighted bisimulation is ≈ L = R j .
x 1

x 2 x 3 2 1 1 a, 1 3 a, 1 b, 1 3 b, 3 a, 1/b, 1 x 1 x 2 x 3 2 1 1 a, 1 3 a, 1 b, 1 3 b, 3 a, 1/b, 1 O = 2 1 1 T a =   1 1 3 1 0 0 0 0 0 0   T b =   1 0 0 0 0 3 0 1 3 0   t T a =   1 0 0 1 3 0 0 1 0 0   t T b =   1 0 0 0 0 1 3 0 3 0   Figure 5: A weighted automata (V, o, t ) (left) and its reversed (V, o, t t )
PROOF. The R i 's form a descending chain of sub-spaces of V . The corresponding dimensions form a nonincreasing sequence, hence the existence of j as required is obvious. That R j is a bisimulation follows by applying Lemma 3: indeed, it is obvious that (1) ker(o) ⊇ R j , while as to (2) we have that, since R j+1 = R j , then R j ∩ a∈A t(R j )(a) -1 = R j , i.e., for all a ∈ A, t(R j )(a) ⊆ R j .

We finally show that any linear weighted bisimulation R is included in R j . We do so by proving that for each i, R ⊆ R i , thus, in particular R ⊆ R j . We proceed by induction on i. Again by Lemma 3, we know that R 0 = ker(o) ⊇ R. Assume now R ⊆ R i . For each action a, by Lemma 3 we have that t

(R)(a) ⊆ R, which implies R ⊆ {v ∈ R i | ∀a ∈ A, t(v)(a) ∈ R i } = R i+1 .
Concretely, the algorithm iteratively computes a basis B i for each space R i . This can be done by solving systems of linear equations expressing the constraints in the definition of R i . Since the backward algorithm presented in the next section is computationally more efficient, we avoid to give further details about its implementation and we show, as an example, the algorithm at work with the linear automata (V, o, t ) in Fig. 5.

At the beginning, we compute a basis for R 0 = ker(o). This is

B 0 =      -1 2 1 0   ,   -1 2 0 1      .
In the first iteration, we compute one basis for the space t(R 0 )(a) -1 and one for the space t(R 0 )(b) -1 . These are respectively

B a 1 =      -1 3 1 0   ,   -1 0 1      and B b 1 =      -1 6 1 0   ,   -3 2 0 1      . Then, R 1 is given by the intersection R 0 ∩ t(R 0 )(a) -1 ∩ t(R 0 )(b) -1 . A basis for R 1 is B 1 =      -2 3 1      .
In the second iteration, we compute one basis for the space t(R 1 )(a) -1 and one for the space t(R 1 )(b) -1 . These are respectively

B a 2 =      -1 3 1 0   ,   -1 0 1      and B b 2 =      -2 3 1      . Then, R 2 is the intersection R 1 ∩ t(R 1 )(a) -1 ∩ t(R 0 )(b) -1 . A basis for R 2 is B 2 =      -2 3 1      that is equal to B 1 . Since R 1 = R 2
the algorithm terminates and returns R 1 . Now, in order to check if two vectors v 1 , v 2 ∈ V accept the same weighted language (i.e., v

1 ≈ L v 2 ), we have to look if v 1 -v 2 belongs to R 1 . For instance, x 1 ≈ L 3 2 x 2 + 1 2 x 3 because x 1 -3 2 x 2 -1 2 x 3 ∈ R 1 .
We note that ker(o) in general a large sub-space: since o : V → K with dim(K) = 1, by virtue of equation ( 1) we have that dim(ker(o)) ≥ dim(V ) -1. This might be problematic in the actual computation of the basis of ≈ L . We present an alternative version in the next subsection which will avoid this problem.

A backward algorithm

Two well-known concepts from linear algebra will be relied upon to describe the basic operations of the backward algorithm. More precisely, annihilators will be used to describe the complement of a relation, while transpose maps will be used to describe the operation of "reversing arrows" in an automaton. These operations are carried out within the dual space of V . So we start by reviewing the concept of dual space; an in-depth treatment can be found in e.g. [START_REF] Halmos | Finite dimensional vector spaces[END_REF].

Let K be any field and V a vector space over K. The dual space of V , denoted V ⋆ , is the set of all linear maps V → K, with K seen as a 1-dimensional vector space. The elements of V ⋆ are often called functionals and we use ψ 1 , ψ 2 , . . . to range over them. The sum of two functionals ψ 1 + ψ 2 and the scalar multiplication k • ψ (for k ∈ K) are defined point-wise as expected, and turn V ⋆ into a vector space over K. We will denote functional application ψ(v) as [v, ψ], the bracket notation intending to emphasize certain analogies with inner products. Fix an ordered basis

B = (v 1 , ..., v n ) of V and consider B ⋆ = (v ⋆ 1 , ..., v ⋆ n )
, where the functionals v ⋆ i are specified by [v j , v ⋆ i ] = δ ij for each i and j. Here, δ ij denotes the Kronecker symbol, which equals 1 if i = j and 0 otherwise. It is easy to check that B ⋆ forms a basis of V ⋆ , referred to as the dual basis of B. Hence dim(V ⋆ ) = dim(V ). In particular, the morphism (-)

⋆ : V → V ⋆ that sends each v i into v ⋆ i is an isomorphism between V and V ⋆ . A crucial definition is that of transpose morphism.

Definition 6 (transpose linear map).

Let f : V → V be a linear map. We let the transpose of f be the endomorphism t f :

V ⋆ → V ⋆ defined for all ψ ∈ V ⋆ as t f (ψ) = ψ • f .
It is easy to check that that if F is the matrix representing f in V w.r.t. to B, then the transpose matrix t F represents t f in V ⋆ w.r.t. B ⋆ , whence the terminology and the notation. It is quite expected that, by taking the transpose twice one gets back the original morphism. This is in fact the case, although one has to take care of identifying things up to isomorphism. Denote by V ⋆⋆ the space (V ⋆ ) ⋆ , called double dual of V . There is a natural isomorphism i between V and V ⋆⋆ , given by i : v → [v, -] (note that this isomorphism does not depend on the choice of a basis). In the sequel, we shall freely identify V and V ⋆⋆ up to this isomorphism, i.e. identify v and [v, -] for each v ∈ V . With this identification, one has that t ( t f ) = f . We need another concept from duality theory. Given a subspace U of V , we denote by U o the annihilator of U , the subset of functionals that vanish on U .

Definition 7 (annihilator). For any

U ⊆ V , we let U o = {ψ ∈ V ⋆ | [u, ψ] = 0 for each u ∈ U }.
Once again, the notation makes the analogy with inner products explicit. We use the following properties of annihilators, where U, W are a sub-spaces of V :

(i) U o is a sub-space of V ⋆ ; (ii) (-) o reverses inclusions, i.e. if U ⊆ W then W o ⊆ U o ; (iii) (-) o is an involution, that is (U o ) o = U up
to the natural isomorphism between V and its double dual. These three properties suggest that U o can be regarded as a complement, or negation, of U seen as a relation. Another useful property is: (iv) dim(U o ) + dim(U ) = dim(V ). Transpose morphisms and annihilators are connected via the following property, which is crucial to the development of the algorithm. It basically asserts that f -invariance of R corresponds to t f -invariance of the complementary relation represented by R o . Lemma 4 Let U be a sub-space of V and f be an endomorphism on

V . If U is f -invariant then U o is t f -invariant.
We are now ready to give the backward version of the partition refinement algorithm. An informal preview of the algorithm is as follows. Rather than computing directly the sub-space representing ≈ L , the algorithm computes the sub-space representing the complementary relation. To this end, the algorithm starts from a relation R 0 that is the complement of the relation identifying vectors with equal weights, then incrementally computes the space of all states that are backward reachable from R 0 . The largest bisimulation is obtained by taking the complement of this space. Geometrically, "going backward" means working with the transpose transition functions t t a rather than with t a . Taking the complement of a relation actually means taking its annihilator. This essentially leads one to work within V ⋆ rather than V . Recall that U + W denotes span(U ∪ W ).

Theorem 4 (partition refinement, backward version) Let (V, o, t ) be a LWA. Consider the sequence (R i ) i≥0 of sub-spaces of V ⋆ inductively defined by:

R 0 = ker(o) o R i+1 = R i + a∈A t t a (R i ) . ( 3
)
Then there is

j ≤ dim(L) such that R j+1 = R j . The largest L-bisimulation ≈ L is R o j , modulo the natural isomor- phism between V and V ⋆⋆ . PROOF. Since R 0 ⊆ R 1 ⊆ R 2 ⊆ • • • ⊆ V ⋆ ,
the sequence of the dimensions of these spaces is non-decreasing. As a consequence, for some

j ≤ dim(V ⋆ ) = dim(L), we get dim(R j ) = dim(R j+1 ). Since R j ⊆ R j+1 , this implies R j = R j+1 .
We next show that R o j is an L-bisimulation. Indeed, by the properties of annihilators and up to the natural isomorphism: [START_REF] Adámek | Abstract and Concrete Categories -The Joy of Cats[END_REF]

ker(o) o ⊆ R j implies (ker(o) o ) o = ker(o) ⊇ R o j . Moreover: (2) for any a ∈ A, t t a (R j ) ⊆ t t a (R j ) + R j ⊆ R j+1 = R j implies, by Lemma 4, that t ( t t a (R o j )) = t a (R o j ) ⊆ R o j
; by (a), (b) and Lemma 3, we conclude that R o j is an L-bisimulation. We finally show that any L-bisimulation R is included in R o j . We do so by proving that for each i, S ⊆ R o i , thus, in particular S ⊆ R o j . We proceed by induction on i. Again by Lemma 3, we know that

R o 0 = ker(o) ⊇ R. Assume now R ⊆ R o i , that is, R o ⊇ R i .
For each action a, by Lemma 3 we have that t a (R) ⊆ R, which implies

t t a (R o ) ⊆ R o by Lemma 4. Hence R o ⊇ t t a (R o ) ⊇ t t a (R i )
, where the last inclusion stems from R o ⊇ R i . Since this holds for each a, we have that R o ⊇ a t t a (R i ) + R i = R i+1 . Taking the annihilator of both sides reverses the inclusion and yields the wanted result.

We note that what is being "refined" in the algorithm above are not, of course, the sub-spaces R i , but their complements:

R o 0 ⊇ R o 1 ⊇ • • • ⊇ R o j =≈ L .
In particular, we start with a "small" space R o 0 of dimension ≤ 1: this may represent an advantage in a practical implementation of the algorithm.

To conclude the section, we briefly discuss some practical aspects involved in the implementation of the algorithm. By virtue of (2), checking u ≈ L v, for any pair of vectors v 1 and v 2 , is equivalent to checking v 1v 2 ∈ ker(≈ L ). This can be done by first computing a basis of ≈ L and then checking for linear (in)dependence of v 1v 2 from this basis. Alternatively, and more efficiently, one can check whether

v 1 -v 2 is in R o j , or, more explicitly, whether [v 1 -v 2 , ψ] = 0 for each ψ ∈ R j . This reduces to showing whether [v 1 -v 2 , ψ] = 0 for each ψ ∈ B j
, where B j is a basis for R j . Thus, our task reduces to computing such a basis. To do so, fix any basis B of V and let O and T a (a ∈ A) be the row-vector and matrices representing the weight and transition functions of the LWA in this basis. The concrete computations are carried out representing vectors and functionals in this basis.

Compute a basis B

0 of R 0 . As already discussed, dim(ker(o)) ≥ dim(V ) -1, hence dim(ker(o) o ) ≤ 1. It is readily checked that o ∈ ker(o) o , thus ker(o) o is spanned by o.
We thus set B 0 = {o}. With respect to the chosen basis B, B 0 is represented by {O}. 2. For each i ≥ 0, compute a basis B i+1 of R i+1 . This can be obtained by incrementally joining to B i the functionals t t a (ψ), for a ∈ A and ψ ∈ B i , that are linearly independent from previously joined functionals.

With respect to the basis B, t t a (ψ) is represented by Ψ×T a , where Ψ is the row-vector representing ψ; checking linear independence of t t a (ψ) means hence checking linear independence of Ψ × T a from previously joined row-vectors.

After j ≤ n iterations, one finds a set B j such that B j+1 = B j : this is the basis of R j . We illustrate this algorithm in the example below.

Consider the LWA (V, o, t ) on the left of Figure 5. At the beginning we can set B 0 = {O}. Next, we apply the algorithm to build the B i 's. Manually, the computation of the vectors ΨT a = t ( t T a t Ψ) can be carried out by looking at the transitions of the WA with arrows reversed (in the right of Figure 5). Doing so, we first get OT a = (2 2 3 2) and OT b = (2 1 3 3). Note that OT b is not linearly independent from the other vectors:

OT b = -(2 1 1) + 2(2 2 3 2). Thus B 1 = {(2 1 1), (2 2
3 2)}. In the second iteration, we compute

(2 2 3 2)T a = (2 2 3 2) and (2 2 3 2)T b = (2 2 3 2) and thus B 2 = {(2 1 1), (2 2
3 2)} that is equal to B 1 . The functionals represented by vectors in B 1 are a basis of (≈ L ) o . As an example, let us check that

x 1 ≈ L 3 2 x 2 + 1 2 x 3 .
To this purpose, note that the difference vector

x 1 -3 2 x 2 -1 2 x 3 annihilates B 1 , that is [   1 -3 2 -1 2   , u] = 0 for each u ∈ B 1 , which is equivalent to 2x 1 ≈ L 3 2 x 2 + 1 2 x 3 .
It is quite easy to give an upper bound on the cost of the backward algorithm, in terms of the number of sum and product operations in the underlying field. Let n be the dimension of V . Each time we join a new vector v = Ψ × T a to the basis B, we have a cost of O(n 2 ) for vector-matrix multiplication, plus a cost of O(n 3 ) for checking linear independence of v from B, for a predominant cost of O(n 3 ). Since the operation of joining a vector to the basis cannot be done more than n times, we have a global cost of O(n 4 ). In the case |A| = 1, one can adapt the Arnoldi's iteration algorithm [START_REF] Saad | Iterative Methods for Sparse Linear Systems[END_REF] to compute B, which takes O(n 3 ) operations. It is not clear whether this algorithm can be adapted also to the case |A| 1. In practical cases, the transition matrices tend to be sparse, and the number of iterations after which the algorithms stops may be much less than n. By adopting suitable representations for sparse matrices, these circumstances can be used to lower considerably the practical complexity of the algorithm.

The final sequence and the forward algorithm

The theory of coalgebras also provides a way of constructing final coalgebras by means of final sequences (often referred in literature as terminal sequences) [START_REF] Barr | Terminal coalgebras in well-founded set theory[END_REF]. Many important algorithms for computing behavioural equivalences (such as [START_REF] Kanellakis | Ccs expressions, finite state processes, and three problems of equivalence[END_REF]) can be abstractly described in terms of final sequences.

In this section, we describe the relationship between the forward algorithm (in Proposition 6) and the final sequence of the functor L. The latter is the cochain

1 ! ←-L1 L! ←-L 2 1 L 2 ! ←-. . .
where L n+1 1 is L • (L n 1), L 0 1 = 1 is the final vector space {0}, and ! is the unique morphism from L1 to 1.

Let A * n be the set of all words w ∈ A * with length smaller than n. For each n, L n 1 is isomorphic to K A * n , i.e., the space of functions from A * n to K. Indeed, for n = 1, L1 is by definition K × 1 A = K that is isomorphic to the space of functions from A * 1 = {ǫ} to K; and for n + 1, each k, σ ∈ K × L n (1) A = L n+1 1 can be seen as function

A * n+1 → K mapping ǫ into k and aw (for a ∈ A and w ∈ A * n ) into σ(a)(w). For σ : A * m → K and n ≤ m, the n-restriction of σ is σ ↿ n : A * n → K defined as σ, but in a restricted domain. The morphism L n ! : L n+1 1 → L n 1 maps each σ into σ ↿ n.
The limit of this cochain is K A * together with the maps ζ n : K A * → L n 1 that assign to each weighted language σ its n-restriction σ ↿ n.

K A * ζ2 ζ1 Ø Ø ζ0 × × 1 L1 ! o o L 2 1 L! o o . . . L 2 ! o o
Every L-coalgebra (V, o, t ) determines a cone ! n : V → L n 1 as follows:

• ! 0 : V → 1 is the unique morphism to the final vector space 1,

• ! n+1 : V → L n+1 1 = L(! n ) • o, t .
The latter can be more concretely defined for all v ∈ V and w ∈ K A * n+1 as

! n+1 (v)(w) = o(v), if w = ǫ; ! n (t(v)(a))(w ′ ), if w = aw ′ . Note that the final morphism [[-]] L V : V → K A * (mapping each v ∈ V in the language that it recognizes) is the unique function such that for all n, ζ n • [[-]] L V =! n . K A * ζ2 ζ1 Ø Ø ζ0 × × 1 L1 ! o o L 2 1 L! o o . . . L 2 ! o o V [[-]] L V y y !2 !1 !0 Recall that the L-behavioural equivalence on (V, o, t ) is the kernel of [[-]] L V .
The forward algorithm computes it, by iteratively computing the kernel of the morphisms ! n . Proposition 7 Let (V, o, t ) be a LWA. Let R n be the relation computed by the forward algorithm (Proposition 6). Let ! n : V → L n 1 be the morphisms described above. Then for all natural numbers n, R n = ker(! n+1 ).

PROOF. First of all, note that the kernel of

! 0 : V → 1 is the whole V . The kernel of ! n+1 is the space of v ∈ V such that ! n+1 (v)(w) = 0 for all the words w ∈ A * n+1 , i.e., ker(! n+1 ) = {v ∈ V | o(v) = 0 and ∀a ∈ A, t(v)(a) ∈ ker(! n )}.
By induction on n, we prove that ker(! n+1 ) = R n .

For n = 0, note that ker(!

1 ) = {v ∈ V | o(v) = 0 and ∀a ∈ A, t(v)(a) ∈ ker(! 0 )}. Since ker(! 0 ) = V , ker(! 1 ) = {v ∈ V | o(v) = 0} = R 0 .
As induction hypothesis suppose that ker(

! n ) = R n-1 . Then ker(! n+1 ) = {v ∈ V | o(v) = 0 and ∀a ∈ A, t(v)(a) ∈ R n-1 } = R n .
This result can be seen as an alternative proof of the soundness of the forward algorithm. Indeed, if R j is the result of the algorithm, for all k ≥ j, R k = R j , i.e., ker(! k ) = ker(! j ). Thus R j = n ker(! n ) and, by definition of ! n ,

n ker(! n ) = ker([[-]] L V ).
We note that for the case of |A| = 1, the functor L is isomorphic to

L(V ) = K × V A ∼ = K × V
Moreover, the final L-coalgebra is isomorphic to the set of streams over the field K:

K A * ∼ = K ω
Therefore we shall proceed by recalling from [START_REF] Jan | Rational streams coalgebraically[END_REF] the basics of stream calculus and linear stream differential equations, in Subsections 5.1 and 5.2. Next we shall characterise the final homomorphism, for the case |A| = 1, in Subsection 5.3. Building on [START_REF] Jan | Behavioural differential equations: a coinductive calculus of streams, automata, and power series[END_REF], we shall finally generalise these results for finite alphabets, in Subsection 5.4.

Recalling the basics of stream calculus

We define the set of streams over the field K by

K ω = {σ | σ: N → K}
(where N is the set of natural numbers). We often denote elements σ ∈ K ω by σ = (σ(0), σ(1), σ(2), . . .). We define the stream derivative of a stream σ by σ ′ = (σ(1), σ(2), σ(3), . . .), and the initial value of σ by σ(0).

For k ∈ K, we define the constant stream

[k] = (k, 0, 0, 0, . . .)

which we often denote again by k. Another constant stream is X = (0, 1, 0, 0, 0, . . .)

For σ, τ ∈ K ω and n ∈ ω, the operations of sum and (convolution) product are given by

(σ + τ )(n) = σ(n) + τ (n) , (σ × τ )(n) = n i=0 σ(i) • τ (n -i)
(where, as usual • denotes product of K).

We call a stream π ∈ K ω polynomial if there are n ≥ 0 and a i ∈ K such that

π = a 0 + a 1 X + a 2 X 2 + • • • + a n X n = (a 0 , a 1 , a 2 , .
. . , a n , 0, 0, 0, . . .)

where we write a i X i for [a i ] × X i with X i the i-fold product of X with itself.

A stream σ with σ(0) = 0 has a (unique) multiplicative inverse σ -1 in K ω , satisfying

σ -1 × σ = [1]
As usual, we shall often write 1/σ for σ -1 and σ/τ for σ × τ -1 . Note that the initial value of the sum, product and inverse of streams is given by the sum, product and inverse of their initial values. We call a stream ρ ∈ K ω rational if it is the quotient ρ = σ/τ of two polynomial streams σ and τ with τ (0) = 0.

One can compute a stream from its initial value and derivative by the so-called fundamental theorem of stream calculus [START_REF] Jan | A coinductive calculus of streams[END_REF]: for all σ ∈ K ω ,

σ = σ(0) + (X × σ ′ ) (4)
(writing σ(0) for [σ(0)]).

The fundamental theorem of stream calculus allows us to solve stream differential equations such as

σ ′ = 3 × σ , σ(0) = 1 by computing σ = σ(0) + (X × σ ′ ) = 1 + (X × 3 × σ)
, which leads to the solution σ = 1/(1 -3X) = (1, 3, 3 2 , 3 3 , . . .)

Solving linear systems of stream differential equations

Using some elementary linear algebra notation (matrices and vectors), we next show how to solve linear systems of stream differential equations. For notational convenience, we shall deal with linear systems of dimension 2, which can be straightforwardly generalised to systems of higher dimensions. They are given by the following data:

σ τ ′ = M × σ τ σ τ (0) = N ( 5
)
where M is a 2 × 2-matrix and N is a 1 × 2-matrix over K:

M = m 11 m 12 m 21 m 22 N = n 1 n 2 for m ij , n i ∈ K.
The above notation is really just a short hand for the following system of two stream differential equations:

σ ′ = (m 11 × σ) + (m 12 × τ ) σ(0) = n 1 τ ′ = (m 21 × σ) + (m 22 × τ ) τ (0) = n 2
We can solve such a system of equations by using twice the fundamental theorem of stream calculus (equation ( 4) above), once for σ and once for τ :

σ = σ(0) + (X × σ ′ ) τ = τ (0) + (X × τ ′ )
In matrix notation, the fundamental theorem looks like

σ τ = σ τ (0) + X × σ τ ′
Next we can solve our linear system (5) above by happily calculating as follows:

σ τ = σ τ (0) + X × σ τ ′ = N + X × M × σ τ
This leads to

(I -(X × M )) σ τ = N
where I and X × M are given by

I = 1 0 0 1 X × M = m 11 × X m 12 × X m 21 × X m 22 × X
Finally, we can express the unique solution of our linear system of stream differential equations as follows:

σ τ = (I -(X × M )) -1 × N
The advantage of the matrix notations above now becomes clear: we can compute the inverse of the matrix

(I -(X × M )) = 1 -(m 11 × X) -(m 12 × X) -(m 21 × X) 1 -(m 22 × X)
whose values are simple polynomial streams, by standard linear algebra.

Let us look at an example. For

M = 0 1 -1 2 N = 1 2
our linear system of stream differential equations ( 5) has the following solution:

σ τ = (I -(X × M )) -1 × N = 1 -X X 1 -2X -1 × 1 2 = 1-2X (1-X) 2 X (1-X) 2 -X (1-X) 2 1 (1-X) 2 × 1 2 = 1 (1-X) 2 2-X (1-X) 2
We note that the solutions of linear systems of stream differential equations always consist of rational streams.

Characterising the final morphism: |A| = 1

It is easy to see that when |A| = 1, the final coalgebra for the functor L is (K ω , (-)(0), (-) ′ ) where (-)(0):K ω → K and (-) ′ :K ω → K ω map each stream σ in its initial value σ(0) and in its stream derivative σ ′ . Let (K 2 , o, t ) be a LWA, with linear maps o: K 2 → K and t: K 2 → K 2 that are represented by a 1 × 2-matrix O and by a 2 × 2-matrix T . We will now show how the final homomorphism

K 2 o,t [[-]] L K 2 G G K ω (-)(0),(-) ′ K × K 2 id K ×[[-]] L K 2 G G K × K ω
can be characterised in terms of rational streams. To this end, we define

σ = [[ 1 0 ]] L K 2 τ = [[ 0 1 ]] L K 2
It follows from the commutativity of the diagram above that

σ ′ = [[(T 1 0 )]] L K 2 σ(0) = O 1 0 τ ′ = [[(T 0 1 )]] L K 2 τ (0) = O 0 1
and this can be concisely expressed by the following system:

σ τ ′ = t T × σ τ σ τ (0) = t O
(where the superscript t indicates matrix transpose). These identities present σ and τ as the solution of a linear system of stream differential equations. By the results from Subsection 5.2, it follows that

σ τ = (I -(X × t T )) -1 × t O
which leads to the following general formula for

[[-]] L K 2 : [[ k 1 k 2 ]] L K 2 = k 1 k 2 × (I -(X × t T )) -1 × t O
For instance, if

T = 0 -1 1 2 O = 1 2
we find, using the example with M and N from Subsection 5.2, that

[[ k 1 k 2 ]] L K 2 = k 1 k 2 × (I -(X × T t )) -1 × O t = k 1 k 2 × (I -(X × M )) -1 × N = k 1 k 2 × 1 (1-X) 2 2-X (1-X) 2 = (k 1 + 2k 2 ) -k 2 X (1 -X) 2
Note that the above expression fully characterizes [[-]] L K 2 , in the sense that it maps each v ∈ K 2 in the corresponding rational stream.

Computing ≈ L . We can employ the above characterization in order to compute ≈ L on (K 2 , o, t ). We use the fact that the final homomorphism identifies precisely all equivalent states:

x 1 x 2 ≈ L y 1 y 2 ⇐⇒ [[ x 1 x 2 ]] L K 2 = [[ y 1 y 2 ]] L K 2 ⇐⇒ [[ x 1 -y 1 x 2 -y 2 ]] L K 2 = 0
where the 0 on the right is the stream [0] = (0, 0, 0, . . .). The kernel of the final homomorphism can now be computed using our characterisation above: for all k 1 , k 2 ∈ K,

[[ k 1 k 2 ]] L K 2 = 0 ⇐⇒ (k 1 + 2k 2 ) -k 2 X (1 -X) 2 = 0 ⇐⇒ (k 1 + 2k 2 ) -k 2 X = 0 ⇐⇒ k 1 = 0 and k 2 = 0
As a consequence, we find, for the present example:

x 1 x 2 ≈ L y 1 y 2 ⇐⇒ x 1 x 2 = y 1 y 2

Rational weighted languages

All the results presented above allow to characterize the final homomorphism for weighted automata over an alphabet with a single letter. These results can be generalized in order to deal with alphabets of size greater than one.

Let A be an arbitrary finite alphabet. Recall from Section 3.3 that the final L-coalgebra is (K A * , ǫ, d ) where for all σ ∈ K A * and a ∈ A, ǫ(σ) = σ(ǫ) d(σ)(a) = σ a and σ a denotes the a-derivatives of the language σ. The calculus presented in the previous section for one-variable power series (streams) can be generalized for multiple variable series [START_REF] Jan | Behavioural differential equations: a coinductive calculus of streams, automata, and power series[END_REF], which we will recall next.

There are unique operators on series satisfying the following equations. For all k ∈ K, a, b ∈ A and σ, τ

∈ K A * , Derivative Initial Value Name k a = 0 k(ǫ) = k Constant (X a ) a = 1, (X a ) b = 0 (b = a) X a (ǫ) = 0 Variable (σ + τ ) a = σ a + τ a (σ + τ )(ǫ) = σ(ǫ) + τ (ǫ) Sum (σ × τ ) a = (σ a × τ ) + (σ(ǫ) × τ a ) (σ × τ )(ǫ) = σ(ǫ) × τ (ǫ) Convolution product (σ -1 ) a = -(σ(ǫ) -1 × σ a ) × σ -1 (σ -1 )(ǫ) = σ(ǫ) -1 , if σ(ǫ) = 0 Inverse
A weighted language is rational if it can be constructed from finitely many constants k ∈ K and variables X a , by means of the operators of sum, product, and inverse. Rational languages constitute the class of languages that are recognized by finite dimensional weighted automata.

As for streams, one can compute a series from its initial value and derivatives by the so-called fundamental theorem [START_REF] Jan | Behavioural differential equations: a coinductive calculus of streams, automata, and power series[END_REF]. That is, for all weighted languages σ ∈ K A * :

σ = σ(ǫ) + a∈A X a × σ a (6)
The fundamental theorem allows us to solve equations, similar to what happened above for streams. As an example, take A = {a, b} (weighted languages over two symbols coincide with infinite binary trees), and the following equations

σ a = 3 × σ, σ b = 3 × σ, σ(ǫ) = 1
Applying the fundamental theorem we reason as follows:

σ = σ(ǫ) + (X a × σ a ) + (X b × σ b ) ⇔ σ = 1 + (3X a × σ) + (3X b × σ) ⇔ (1 -3X a -3X b )σ = 1
which leads to the solution σ = (1 -3X a -3X b ) -1 , the tree depicted in the following picture. Note that the above language is exactly the one recognized by the automata in Figure 1. It is also interesting to remark the strong similarity with streams: the formula for the stream (1, 3, 6, 9, . . .) is (1 -3X) -1 . Now that we know how to compute the solution of a single equation, moving to systems of equations is precisely as for streams. Again, for notational convenience, we shall exemplify with linear systems of dimension 2. The goal is to solve

σ τ a = M a × σ τ σ τ (ǫ) = N
where, for each a ∈ A, M a is a 2 × 2-matrix and N is a 1 × 2-matrix over K.

We now solve this system by calculating as follows (similar to the stream case), now using the fundamental theorem for weighted languages, given in equation ( 6):

σ τ = σ τ (ǫ) + a∈A X a × σ τ a = N + a∈A X a × M a × σ τ
This leads to

I - a∈A (X a × M a ) σ τ = N
where I and X a × M a are as before. Finally, we can express the unique solution of our linear system as follows:

σ τ = I - a∈A (X a × M a ) -1 × N
Hence, the only difference with the stream case is that instead of computing the inverse of the matrix I -(X × M ) one needs to compute the inverse of I -a∈A (X a × M ).

Some remarks on computing the inverse of I -a∈A (X a × M ) are now in order. Convolution product on power series in not commutative as soon as A has more than one element (e.g., X a × X b = X b × X a ). Thus, the matrix above is a matrix with entries stemming from a non-commutative ring. Traditional methods (Gaussian elimination, Cramer's rule, . . . ) to compute the inverse of matrices are not applicable and thus one needs to resort to other (more complicated) techniques such as quasi-determinants [START_REF] Gelfand | Quasideterminants[END_REF] or generalized LDU decomposition [START_REF] Francisco Camino | A symbolic algorithm for determining convexity of a matrix function: How to get schur complements out of your life[END_REF].

A function to compute the inverse of a matrix with non-commutative entries is provided in the Mathematica [START_REF]Mathematica[END_REF] package NCAlgebra [START_REF]The NCAlgebra package[END_REF]. The algorithm implemented in the package is directly base in LDU decomposition [START_REF] Francisco Camino | A symbolic algorithm for determining convexity of a matrix function: How to get schur complements out of your life[END_REF]. The matrices we show below were all obtained using the aforementioned package.

For instance, for A = {a, b, c}, if

M a = M c = 2 0 0 0 M b = 0 0.5 0 0.5 N = 1 1 then I -X a × M a -X b × M b -X c × M c = 1 -2X a -2X c -0.5X b 0 1 -0.5X b and (I -X a × M a -X b × M b -X c × M c ) -1 = 1 1-2Xa-2Xc 0.5 1 1-2Xa-2Xc X b 1 1-0.5X b 0 1 -0.5X b The final homomorphism [[-]] L K 2 is represented in the following diagram K 2 o,t [[-]] L K 2 G G K A * ǫ,d K × K 2 A id K ×[[-]] L K 2 A G G K × K A *
where, as usual, o and t = {t a :K 2 → K 2 } a∈A are linear mappings represented by the 1 × 2-row vector O and the 2 × 2-matrixes T a , respectively.

We will show how the final homomorphism [[-]] L K 2 can be characterized in terms of rational weighted languages. To this end, we again define

σ = [[ 1 0 ]] L K 2 τ = [[ 0 1 ]] L K 2
It follows from the commutativity of the diagram above that

σ a = [[(T a 1 0 )]] L K 2 σ(ǫ) = O 1 0 τ a = [[(T a 0 1 )]] L K 2 τ (ǫ) = O 0 1
and this can be concisely expressed by the following system:

σ τ a = t T a × σ τ σ τ (ǫ) = t O It then follows that σ τ = (I - a∈A X a × t T a ) -1 × t O
which leads to the following general formula for

[[-]] L K 2 : [[ k 1 k 2 ]] L K 2 = k 1 k 2 × (I - a∈A X a × t T a ) -1 × t O
For instance, for A = {a, b, c} and

T a = T c = 2 0 0 0 T b = 0 0 0.5 0.5 O = 1 1
we find, using the example above, that

[[ k 1 k 2 ]] L K 2 = k 1 k 2 × a∈A X a × T a t -1 × O t = k 1 k 2 × a∈A X a × T a -1 × N = k 1 k 2 × 1 1-2Xa-2Xc + 0.5 1 1-2Xa-2Xc X b 1 1-0.5X b 1 (1-0.5X b ) = k 1 1 -2X a -2X c + 0.5k 1 1 1 -2X a -2X c X b 1 1 -0.5X b + k 2 (1 -0.5X b )
By generalizing the above arguments from K 2 to any finite dimesion vector space, we obtain the following theorem.

Theorem 5 Let (V, o, t ) be a linear weighted automata with V finite dimension. Then, for all v ∈ V

[[v]] L V = t v × (I - a∈A X a × t T a ) -1 × t O
For an example with a three dimensional state space, we consider the LWA corresponding to the automaton (V, o, t ) in Fig. 5.

[[   k 1 k 2 k 3   ]] L V = k 1 k 2 k 3 × (I - a∈A X a × t T a ) -1 × t O = k 1 k 2 k 3 × (I -    X a + X b 0 0 Xa 3 0 X b 3 X a 3X b 0   ) -1 ×   2 1 1   = k 1 k 2 k 3 ×    1 -X a -X b 0 0 -Xa 3 1 -X b 3 -X a -3X b 1    -1 ×   2 1 1  
The inverse of the matrix in the middle is

M =     1 1-Xa-X b 0 0 ( 1 3 + X b 3 1 1-X 2 b (X b + 1))X a 1 1-Xa-X b 1 + X b 1 1-X 2 b X b X b 3 1 1-X 2 b ( 1 1-X 2 b )(X a + X b X a ) 1 1-Xa-X b 3 1 1-X 2 b X b 1 1-X 2 b     and M ×   2 1 1   =     2 1-Xa-X b ( 1 3 + X b 3 1 1-X 2 b (X b + 1))X a 2 1-Xa-X b + 1 + X b 1 1-X 2 b X b + X b 3 1 1-X 2 b ( 1 1-X 2 b )(X a + X b X a ) 2 1-Xa-X b + 3 1 1-X 2 b X b + 1 1-X 2 b     =   ρ 1 ρ 2 ρ 3   Summarizing [[   k 1 k 2 k 3   ]] L V = k 1 k 2 k 3 ×   ρ 1 ρ 2 ρ 3   (7)
Note that the above expression fully characterizes [[-]] L V , in the sense that it maps each v ∈ V in the rational weighted lanuage that it accepts.

Computing ≈ L . Now, we have a rational expression σ = k 1 ρ 1 + k 2 ρ 2 + k 3 ρ 3 characterizing the final homomorphism and we would like to calculate for which values of k 1 , k 2 and k 3 this expression equals 0. As we have shown before, when |A| = 1, this can be done by syntactically manipulating the rational expression in a standard way. In the general case, because of the non commutativity of the convolution product, this is not trivial at all.

Here, we choose to adopt the following approach: first we compute "some" derivatives σ a , σ b , σ aa , σ ab . . . and then we check for wich k 1 , k 2 and k 3 the initial values σ(ǫ), σ a (ǫ), σ b (ǫ), σ aa (ǫ), σ ab (ǫ) . . . are equal to 0. The following lemma (proved in [START_REF] Berstel | Rational Series and Their Languages[END_REF][START_REF] Jan | Behavioural differential equations: a coinductive calculus of streams, automata, and power series[END_REF]) ensures that we have to compute only finitely many derivatives.

Lemma 5 Rational weighted languages have finitely many linearly independent derivatives.

In our example, we start by taking the initial value of the expression σ itself obtaining σ(ǫ) = 2k 1 + k 2 + k 3 . Then we take the a and b derivatives which give, respectively, the expressions

σ a = k 1 (ρ 1 ) a + k 2 (ρ 2 ) a + k 3 (ρ 3 ) a (8)   ρ 1 ρ 2 ρ 3   a =   2 1-Xa-X b 1 3 2 1-Xa-X b 2 1-Xa-X b   and σ b = k 1 (ρ 1 ) b + k 2 (ρ 2 ) b + k 3 (ρ 3 ) b      ρ 1 ρ 2 ρ 3      b =      2 1-Xa-X b ( 1 3 1 1-X 2 b (X b + 1))X a 2 1-Xa-X b + 1 1-X 2 b X b + 1 3 1 1-X 2 b X b ( 1 1-X 2 b )(X a + X b X a ) 2 1-Xa-X b + X a 1 1-Xa-X b + 3X b 1 1-X 2 b X b + 3 + X b 1 1-X 2 b     
which have initial values σ a (ǫ) = 2k 1 + 2 3 k 2 + 2k 3 and σ b (ǫ) = 2k 1 + 1 3 k 2 + 3k 3 . Now, note that the a derivative, that is the rational expression [START_REF] Francisco Camino | A symbolic algorithm for determining convexity of a matrix function: How to get schur complements out of your life[END_REF], will now always generate the same derivatives for a and b (since the derivatives of 2 1-Xa-X b are the expression itself again; intuitively, this expression represents an infinite binary tree with 2's in every node and hence has left and right subtrees equal to the whole tree). For the b derivative, we take another level of derivatives and obtain, respectively,

σ ba = k 1 (ρ 1 ) ba + k 2 (ρ 2 ) ba + k 3 (ρ 3 ) ba   ρ 1 ρ 2 ρ 3   ba =   2 1-Xa-X b 1 3 2 1-Xa-X b 2 1-Xa-X b   =   ρ 1 ρ 2 ρ 3   a and σ bb = k 1 (ρ 1 ) bb + k 2 (ρ 2 ) bb + k 3 (ρ 3 ) bb      ρ 1 ρ 2 ρ 3      bb =      2 1-Xa-X b ( 1 3 X b 1 1-X 2 b (X b + 1) + 1 3 )X a 2 1-Xa-X b + X b 1 1-X 2 b X b + 1 + 1 3 X b 1 1-X 2 b ( 1 1-X 2 b )(X a + X b X a ) 2 1-Xa-X b + 3 1 1-X 2 b X b + 1 1-X 2 b      =      ρ 1 ρ 2 ρ 3     
The a-derivative coincides with [START_REF] Francisco Camino | A symbolic algorithm for determining convexity of a matrix function: How to get schur complements out of your life[END_REF] and the b derivative coincides with the original expression σ. Therefore, we have found the the system of equations we need to solve: This example also shows that this procedure is in general not more efficient then the forward algorithm. Indeed, the three equations of the above system coincide with the spaces computed by the forward algorithm: the space (of solutions) of σ(ǫ) = 0 is the space spanned by B 0 (in Section 4.1), the space of σ a (ǫ) = 0 is the one spanned by B a 1 , and the space σ a (ǫ) = 0 is the one spanned by B a 2 .

Discussion

In this paper we proposed a novel coalgebraic perspective on weighted automata and their behavioural equivalences. Weighted automata are W-coalgebras, for a functor W on Set, but they can be regarded also as linear weighted automata, that are L-coalgebras for a functor L on V ect. The behavioural equivalence induced by W coincides with weighted bisimilarity, while the equivalence induced by L (≈ L ) with weighted language equivalence.

Weighted languages (i.e. formal power series) form the vectors spaces K A * that carries the final L-coalgebra: for each linear weighted automata (V, o, t ), the unique L-morphism [[-]] L V into the final coalgebra maps each vector v ∈ V into the weighted language in K A * that v accepts. The unique morphism [[-]] L

V is a linear map and its kernel coincides with ≈ L that, when V is finite dimension, can be computed in three different ways. It is important to remark here that the linearity of [[-]] L

V is key ingredient (in all the three approaches) to finitely compute the equivalence on an infinite state space.

Theorem 5 provides an explicit characterization of [[-]] L V by assigning a syntactic expression denoting a rational weighted language to each vector v ∈ V . This characterization can be employed for computing ≈ L but, in general terms, it seems to be inconvenient to be implemented in an automatic prover. The backward algorithm, instead, is very efficient but its presentation is a bit complex since it requires dual spaces and transpose maps. The forward algorithm is easier to explain and we have shown it is closely related to the construction of the final coalgebra.

As a future work, we would like to extend these results to automata with weights on a semiring S (instead of field K). The coalgebraic characterization of weighted bisimilarity can be easily obtained by employing a semiring evaluation functor instead of the field evaluation functor (Definition 2). For weighted language equivalence on semirings, we should define the functor L on the category of semimodules, instead of V ect. The forward algorithm could be extended (by exploiting its relationship with the construction of final coalgebras) in a rather straightforward way, but the convergence in a finite numbers of iterations might be not guaranteed. The other two approaches strongly rely on the properties of fields and vector spaces (such as the existence of the inverse multiplicative or the dual space). Therefore, it seems challenging to extend them to the case of a generic semiring S. If S is a semifield however, then all elements have a multiplicative inverse. An important example of semifield in this context is the tropical semiring [START_REF] Hebisch | Semirings and semifields[END_REF]. Further, when S is a commutative ring, annihilators and transpose maps can be generalized as operations carried out within the dual module (i.e. linear maps from an S-module to S, seen as a module) [START_REF] Rotman | Advanced Modern Algebra[END_REF]. We leave these extensions as future work.

3 a, 3 /b, 3 Figure 1 :

 3331 Figure 1: The weighted automata (X, oX , tX ) and (Y, oY , tY ) (from left to right). The dashed arrow denotes the W-homomorphism h : X → Y . This induces the equivalence relation R h = X × X that equates all the states in X.

Figure 2 :

 2 Figure 2: The states x1 in the above automata recognize the language mapping aa into 2 and the other words into 0.Although they are all language equivalent, they are not bisimilar.

Figure 3 :

 3 Figure 3: From left to right, three weighted automata over R: (X, oX , tX ), (Z, oZ, tZ ) and (Y, oY , tY ). The dashed arrows denotes the W-homomorphisms h1 : X → Z and h2 : Y → Z. The states x1 and y1 are behaviourally equivalent, but they are not W-bisimilar.

2 a, 1 2 a, - 1 2Figure 4 :

 2214 Figure 4: The weighted automata (X, oX , tX ) (left) and (Y, oY , tY ) (right). The corresponding linear weighted automata(R X ω , o ♯ X , t ♯ X ) and (R Y ω , o ♯ Y , t ♯ Y ) are isomorphic.

1 +

 1 k 2 + k 3 = 0 2k 1 + 2 3 k 2 + 2k 3 = 0 2k 1 + 1 3 k 2 + 3k 3 = 0Solving it yields k 1 = -2k 3 and k 2 = 3k 3 . Hence, the kernel of the final homomorphism is the space spanned by the vector what was computed by the forward algorithm in Section 4.1.

Here we are implicitly assuming that C is a concrete category[START_REF] Adámek | Abstract and Concrete Categories -The Joy of Cats[END_REF], i.e., there exists a faithfull functor U : C → Set. By writing x 1 , x

∈ X, we formally mean that x 1 , x 2 ∈ U X and by[[x i ]] G X , we mean U ([[-]] G X )x i .

where σ a :A * → K denotes the a-derivative of σ that is defined for all w ∈ A * as σ a (w) = σ(aw).

Proposition 3

The maps ǫ : K A * → K and d : K A * → (K A * ) A are linear.

PROOF. We show the proof for d. The one for ǫ is analogous.

Let σ 1 , σ 2 be two weighted languages in K A * . Now for all a ∈ A, w ∈ A * , d(σ

Let k be a scalar in K and σ be a weighted language in

Since K A * is a vector space and since ǫ and d are linear maps, (K A * , ǫ, d ) is an L-coalgebra. The following theorem shows that it is final.

Theorem 2 (finality) From every L-coalgebra (V, o, t ) there exists a unique L-homomorphism into (K A * , ǫ, d ).

PROOF. The only function making the above diagram commutes is [[-]] L V , i.e., the function mapping each vector v ∈ V into the weighted language that it recognizes. Hereafter we show that

V is a linear map. By induction on w, we prove that for all

). We can proceed analogously for the scalar product.

Thus, two vectors v 1 , v 2 ∈ V are L-behaviourally equivalent (v 1 ≈ L v 2 ) iff they recognize the same weighted language (as defined in Section 3.2). Proposition 4 below shows that

is the linearization of the function l X : X → K A * (defined in Section 2) or, in other words, is the only linear map making the following diagram commute.

PROOF. We prove it by induction on w

Weighted languages and rationality

We recall from Section 3 that a linear weighted automaton (LWA) is a coalgebra for the functor L = K×-A , i.e., it consists of a vector space V and a linear map o, t :V → K × V A . We saw in Theorem 2 that the final homomorphism

V that is accepted by v. Moreover, the kernel of this morphism is weighted language equivalence (≈ L ) that, when V is finite dimension, can be computed via the linear partition refinement algorithm (shown in Section 4).

The languages in K A * that are accepted by LWA with finite dimension states spaces are called rational weighted languages (which are also known as rational formal power series) and they can be syntactically represented by a language of expressions [START_REF] Jan | Behavioural differential equations: a coinductive calculus of streams, automata, and power series[END_REF].

In this section, we shall directly characterise [[-]] L V by showing the expression of [[v]] L V for each v ∈ V (Theorem 5). Then we shall employ this characterization for computing ≈ L .

We will first treat the special case of LWA's over a one letter alphabet |A| = 1. Next we will show how to treat the general case of an arbitrary (finite) alphabet.