We have shown that weighted language equivalence \(\sim _l\)  coincides with the
largest \(K\) -linear bisimulation \(\approx _\mathcal {L}\)  on a \(K\) -LWA.
Boreale [1]} and Bonchi et al. [2]} had proposed two versions of a partition refinement
algorithm for finding the largest linear weighted bisimulation on a linear
weighted automaton. Their algorithms were based on the identification of the
linear bisimulations as certain subspaces of the vector space of a linear
weighted automaton over a field. Unfortunately, this algorithm cannot, in
general, be lifted to the semiring-semimodule framework even for finitely
generated semimodules because unlike vector spaces finitely generated
semimodules in general are not Artinian. An Artinian semimodule is one
that satisfies the descending chain property, i.e., there is no infinite
descending chain of subsemimodules ordered by inclusion. For example, the
semimodule \((\mathbb {N},+,0)\)  over the semiring \((\mathbb {N},+,.,0,1)\)  is not Artinian
since the subsemimodules \(2\mathbb {N}\supset 4\mathbb {N}\supset 8\mathbb {N}\ldots \)  form an infinite
descending chain. Even with an Artinian module the procedure is not effective as
it depends on solving linear equations, which requires a multiplicative inverse
in \(K\) . It is also known that weighted language equivalence is undecidable for
finite-state weighted automata over the tropical semiring \((\mathbb {N}\cup \lbrace \infty \rbrace ,\min ,+,\infty ,0)\) 
 [3]}, [4]}.
