Fast Coalgebraic Bisimilarity Minimization

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.