在拟线性时间内通用地解释行为不等价性

我们提供了一种通用算法，用于构造能够区分具有各类迁移类型（如非确定性、概率性或加权）系统中行为不等价状态的公式；对迁移类型的通用性通过在与集合函子相关的余代数（universal coalgebra 范式）下工作来实现。对于给定系统中的每个行为等价类，我们构造一个恰好在该类中各状态成立的公式。该算法可实例化为确定性有限自动机、迁移系统、标记马尔可夫链以及许多其他类型的系统。其所处逻辑是一种模态逻辑，其模态从函子通用地提取；这些模态可在后处理步骤中系统地翻译为自定义的模态集合。新算法建立在已有的余代数划分精化算法之上。对于具有 $n$ 个状态和 $m$ 条迁移的系统，其运行时间为 $\mathcal{O}((m+n) \log n)$，且所构造公式的 dag 大小具有相同的渐近界。与先前的算法相比，即便对先前已知的特定实例（即迁移系统和马尔可夫链）而言，这也改进了运行时间与公式大小的界限；特别地，迁移系统先前最好的界限为 $\mathcal{O}(m n)$。