一句话：提出通用余代数划分细化算法，按行为等价商化系统，复杂度 O(m log n)，并统一多种系统类型。
本文研究按行为等价对系统进行商化的问题，这是系统分析与验证中的基础任务。作者提出通用的余代数划分细化算法：在类型函子可将其有限余代数表示为节点和边的假设下，算法时间复杂度为 O(m log n)，n、m 分别为节点数和边数。余代数的抽象层次不仅能覆盖经典关系系统，还能统一处理加权系统、马尔可夫链、确定性自动机、Segala 系统等，并支持灵活组合已有系统类型。该通用复杂度结果与类型组合能力构成高效划分细化算法工具箱；实例在无标号迁移系统、马尔可夫链、固定字母表确定性自动机和颜色细化等系统上达到已知最佳运行时间。
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.Comment: Extended journal version of the conference paper arXiv:1705.08362. Beside reorganization of the material, the introductory section 3 is entirely new and the other new section 7 contains new mathematical results
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1806-05654,
title = {Efficient and Modular Coalgebraic Partition Refinement},
author = {Thorsten Wißmann and Ulrich Dorsch and Stefan Milius and Lutz Schröder},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 1},
year = {2020},
doi = {10.23638/lmcs-16(1:8)2020}
}