Efficient and Modular Coalgebraic Partition Refinement

TL;DR

This paper introduces a generic, efficient coalgebraic partition refinement algorithm that can handle various system types, achieving optimal runtime and enabling flexible system analysis and verification.

Contribution

It presents a novel, generic coalgebraic partition refinement algorithm with optimal complexity, adaptable to multiple system types and combining existing systems efficiently.

Findings

Runs in O(m log n) time for finite coalgebras

Matches the best known algorithms for various systems

Provides a flexible toolbox for system analysis

Abstract

We present a generic partition refinement algorithm that quotients coalgebraic systems by behavioural equivalence, an important task in system analysis and verification. Coalgebraic generality allows us to cover not only classical relational systems but also, e.g. various forms of weighted systems and furthermore to flexibly combine existing system types. Under assumptions on the type functor that allow representing its finite coalgebras in terms of nodes and edges, our algorithm runs in time $\mathcal{O}(m\cdot \log n)$ where $n$ and $m$ are the numbers of nodes and edges, respectively. The generic complexity result and the possibility of combining system types yields a toolbox for efficient partition refinement algorithms. Instances of our generic algorithm match the run-time of the best known algorithms for unlabelled transition systems, Markov chains, deterministic automata (with fixed alphabets), Segala systems, and for color refinement.