一句话：证明了使用划分精化的顺序与并行双模拟判定算法的时间下界，分别为 Ω((m+n) log n) 与 Ω(n)。
该论文研究标记迁移系统上判定双模拟（bisimulation）的划分精化算法的时间复杂度下界。作者构造并分析若干确定性迁移系统族，顺序情形最终只需两种动作，并行情形只需一种动作，从而证明：顺序划分精化算法的下界为 Ω((m+n) log n)，并行算法为 Ω(n)，其中 n 为状态数、m 为迁移数。对于单动作确定性系统，双相似性可用 Paige、Tarjan 与 Bonic 的线性算法判定，这说明划分精化并非必要。作者借助 oracle 概念表明，该特殊技术无法直接推广为更快的通用双模拟判定算法；并行情形也存在类似情况。
We provide time lower bounds for sequential and parallel algorithms deciding bisimulation on labeled transition systems that use partition refinement. For sequential algorithms this is $\Omega((m \mkern1mu {+} \mkern1mu n ) \mkern-1mu \log \mkern-1mu n)$ and for parallel algorithms this is $\Omega(n)$, where $n$ is the number of states and $m$ is the number of transitions. The lowerbounds are obtained by analysing families of deterministic transition systems, ultimately with two actions in the sequential case, and one action for parallel algorithms. For deterministic transition systems with one action, bisimilarity can be decided sequentially with fundamentally different techniques than partition refinement. In particular, Paige, Tarjan, and Bonic give a linear algorithm for this specific situation. We show, exploiting the concept of an oracle, that this approach is not of help to develop a faster generic algorithm for deciding bisimilarity. For parallel algorithms there is a similar situation where these techniques may be applied, too.
@article{paperbot2217,
title = {Lowerbounds for Bisimulation by Partition Refinement},
author = {Jan Friso Groote and Jan Martens and Erik. P. de Vink},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 2},
year = {2023},
doi = {10.46298/lmcs-19(2:10)2023}
}