Efficient and Modular Coalgebraic Partition-Refinement

ABSTRACT. This talk presents joint work with U. Dorsch, S. Milius and L. Schröder on a generic algorithm combining the following aspects: (1) Partition refinement: In a state based system, partition refinement identifies all states that exhibit the same behaviour. The notion of "same behaviour" of course heavily depends on the concrete type of system worked with and thus is a parameter in the form described next. (2) Coalgebras for a fixed endofunctor H model state based systems with transition structure according to H. E. g. H-coalgebras for HX = 2 × X^A are deterministic automata, whereas for HX = Powerset(A × X), the H-coalgebras are labelled transition systems. With assumptions on H, we obtain: (3) Efficiency: Given an H-coalgebra with n states and m edges, the generic algorithm runs in O((m + n) · log n). Even though the assumptions on H are restrictive, our algorithm minimizes transition systems and weighted systems (with possibly negative weights) in O((m + n) · log n), deterministic finite automata (for a fixed alphabet) in O(n · log n), matching up with the respectively best algorithms for these systems. (4) Modularity is given since we can combine existing transition structures by sequencing, products, or coproducts. Hence, the generic algorithm handles labelled transition systems and deterministic finite automata with non-fixed alphabet slightly slower than existing specific implementations, but for Segala Systems we obtain a new minimization method in O((m + n) · log(m + n)) which is slightly faster than the best known specific implementation. This talk presents the results of a CONCUR 2017 paper and an extended journal version currently under review for the associated special issue.

Authors

• Thorsten Wißmann

Keywords

No keywords are indexed for this paper.