A generalized partition refinement algorithm, instantiated to language equivalence checking for weighted automata

We present a generic algorithm, generalizing partition refinement, for deciding behavioural equivalences for various types of transition systems. In order to achieve this generality, we work with coalgebra, which offers a general framework for modelling different types of state-based systems. The underlying idea of the algorithm is to work on the so-called final chain and to factor out redundant information. If the algorithm terminates, the result of the construction is a representative of the given coalgebra that is not necessarily unique and that allows to precisely answer questions about behavioural equivalence. We instantiate the algorithm to the particularly interesting case of weighted automata over semirings in order to obtain a procedure for checking language equivalence for a large number of semirings. We use fuzzy automata with weights from an l-monoid as a case study.