Fast Coalgebraic Bisimilarity Minimization

TL;DR

This paper introduces a generic, efficient algorithm for coalgebraic bisimilarity minimization applicable to a wide range of automata types, improving scalability and implementation efficiency over specialized methods.

Contribution

The authors develop a universal algorithm for coalgebraic minimization that is both general and efficient, capable of handling large systems across various automaton types.

Findings

Algorithm makes at most O(m log n) calls to functor-specific actions.

The implementation often outperforms specialized algorithms in time and memory.

Can handle larger automata than existing specialized tools.

Abstract

Coalgebraic bisimilarity minimization generalizes classical automaton minimization to a large class of automata whose transition structure is specified by a functor, subsuming strong, weighted, and probabilistic bisimilarity. This offers the enticing possibility of turning bisimilarity minimization into an off-the-shelf technology, without having to develop a new algorithm for each new type of automaton. Unfortunately, there is no existing algorithm that is fully general, efficient, and able to handle large systems. We present a generic algorithm that minimizes coalgebras over an arbitrary functor in the category of sets as long as the action on morphisms is sufficiently computable. The functor makes at most $\mathcal{O}(m \log n)$ calls to the functor-specific action, where $n$ is the number of states and $m$ is the number of transitions in the coalgebra. While more specialized algorithms can be asymptotically faster than our algorithm (usually by a factor of $\mathcal{O}(\frac{m}{n})$), our algorithm is especially well suited to efficient implementation, and our tool Boa often uses much less time and memory on existing benchmarks, and can handle larger automata, despite being more generic.