Partition refinement is a method for minimizing automata and transition systems of various types. Recently, we have developed a partition refinement algorithm that is generic in the transition type of the given system and matches the run time of the best known algorithms for many concrete types of systems, e.g. deterministic automata as well as ordinary, weighted, and probabilistic (labelled) transition systems. Genericity is achieved by modelling transition types as functors on sets, and systems as coalgebras. In the present work, we refine the run time analysis of our algorithm to cover additional instances, notably weighted automata and, more generally, weighted tree automata, substantially improving the asymptotic run time of the best known algorithms.

We have implemented our algorithm in a generic tool CoPaR that is easily instantiated to concrete system types. Moreover, the algorithm and the tool are modular, and so are immediately applicable to new types of systems that are obtained by composing pre-implemented basic types. Experiments show that even for complex system types, the tool is able to handle systems with millions of transitions.

See the PDF of our poster and also the slides of my presentation.