A coalgebraic perspective on minimization, determinization and behavioural metrics

Coalgebra offers a unified theory of state based systems, including infinite streams, labelled transition systems and deterministic automata. In this paper, we use the coalgebraic view on systems to derive, in a uniform way, abstract procedures for checking behavioural equivalence in coalgebras, which perform (a combination of) minimization and determinization in the system. First, we show that for coalgebras on categories equipped with factorization structures, there exists an abstract procedure for equivalence checking. For instance, when considering epi-mono factorizations in the category of sets and functions, this procedure corresponds to the usual (coalgebraic) minimization algorithm and two states are behaviourally equivalent iff they are mapped to the same state in the minimized coalgebra. Second, motivated by several examples, we consider coalgebras on categories without suitable factorization structures: under certain conditions, it is possible to apply the above procedure after transforming coalgebras with reflections. This transformation can be thought of as some kind of determinization. Finally, we show that the result of the procedure also induces a pseudo-metric on the states, in such a way that the distance between each pair of states is minimized.