Coalgebra Encoding for Efficient Minimization

TL;DR

This paper presents an extension of a generic coalgebraic minimization algorithm, incorporating transition structure computation and reachability analysis, with theoretical guarantees and linear runtime.

Contribution

It introduces a fully integrated coalgebraic minimization algorithm and tool, extending previous work with new features and theoretical insights.

Findings

The extended algorithm computes transition structures on minimized states.

Reachability computation is integrated with linear runtime.

Theoretical conditions for coalgebra encodings are established.

Abstract

Recently, we have developed an efficient generic partition refinement algorithm, which computes behavioural equivalence on a state-based system given as an encoded coalgebra, and implemented it in the tool CoPaR. Here we extend this to a fully fledged minimization algorithm and tool by integrating two new aspects: (1) the computation of the transition structure on the minimized state set, and (2) the computation of the reachable part of the given system. In our generic coalgebraic setting these two aspects turn out to be surprisingly non-trivial requiring us to extend the previous theory. In particular, we identify a sufficient condition on encodings of coalgebras, and we show how to augment the existing interface, which encapsulates computations that are specific for the coalgebraic type functor, to make the above extensions possible. Both extensions have linear run time.