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.

翻译：我们针对使用划分精化方法判定标记迁移系统上互模拟关系的顺序算法与并行算法，给出了时间下界。对于顺序算法，下界为 $\Omega((m \mkern1mu {+} \mkern1mu n ) \mkern-1mu \log \mkern-1mu n)$；对于并行算法，下界为 $\Omega(n)$，其中 $n$ 表示状态数，$m$ 表示迁移数。这些下界通过分析确定性迁移系统族得到——在顺序情形中最终涉及两个动作，而在并行算法中仅涉及一个动作。对于单动作确定性迁移系统，可使用与划分精化根本不同的技术顺序判定互模拟关系。具体而言，Paige、Tarjan 和 Bonic 针对该特定情况提出了一个线性算法。我们利用"预言机"概念证明，该方法无助于开发更快的通用互模拟判定算法。对于并行算法，也存在可应用这些技术的类似情形。