Thorsten Wißmann ; Ulrich Dorsch ; Stefan Milius ; Lutz Schröder - Efficient and Modular Coalgebraic Partition Refinement

lmcs:6055 - Logical Methods in Computer Science, January 31, 2020, Volume 16, Issue 1 - https://doi.org/10.23638/LMCS-16(1:8)2020
Efficient and Modular Coalgebraic Partition RefinementArticle

Authors: Thorsten Wißmann ORCID; Ulrich Dorsch ; Stefan Milius ; Lutz Schröder ORCID

    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.


    Volume: Volume 16, Issue 1
    Published on: January 31, 2020
    Accepted on: January 27, 2020
    Submitted on: January 27, 2020
    Keywords: Computer Science - Data Structures and Algorithms,Computer Science - Logic in Computer Science

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1888 times.
    This article's PDF has been downloaded 594 times.