Efficient and Modular Coalgebraic Partition Refinement
2020
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.
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
0
References
0
Citations
NaN
KQI