One desideratum is the existence of a partition refinement algorithm for
computing the weighted language equivalence \(\sim _l\) , at least for finitely
generated semimodules. Unfortunately, the results from Bonchi et al. [1]} do not carry over to our semimodule setting. One
reason for this is the well known fact that weighted language equivalence is
undecidable for finite-state weighted automata over the tropical semiring
 [2]}, [3]}. Instead, we offer an abstract procedure
via the final chain whose limit exists in \(\mathsf {SMod}\) . We restrict ourselves
to finitely generated Artinian semimodules, those satisfying the
descending chain condition for subsemimodules. The limit of the final chain is shown
to be isomorphic to the final coalgebra for the functor \(\mathcal {L}\)  essentially
following the reasoning in [1]}. It is well known that
if the final chain stabilizes at an object that object is isomorphic to the
final coalgebra. For any \(K\) -linear weighted automaton there is a cone to the
final chain such that the kernel of the arrows in the cone constitute a sequence
of \(K\) -linear relations. We show that these \(K\) -linear relations converge to
\(\mathcal {L}\) -bisimulation, i.e., language equivalence, in a finite number of steps in
case the state space of the automaton is a finitely generated Artinian
semimodule (Section ). Unfortunately, this does not give us an
algorithm for computing the bisimilarity relation as this involves solving
\(K\) -linear equations using Gaussian elimination, say. The latter is not possible in
general for semirings as this depends on the existence of the multiplicative
inverse in \(K\) . But for specific semirings this can indeed lead to algorithms
proposed in the past, a summary of which can be found in König and Küpper [5]}.
