技术摘要：弱模拟等价与耦合相似性的极小化与规范化商

问题陈述

标记转换系统（LTS）是各种高级规范语言的基础语义模型。处理状态空间爆炸问题的一种常用技术是商化（quotienting），即合并等价状态以生成一个更小的、在语义上等价的系统。虽然对于强双模拟（strong bisimilarity）、分支双模拟（branching bisimilarity）和迹等价（trace equivalence）而言，商化函数及其性质（规范性和极小性）已得到充分研究，但其在**弱模拟等价（weak simulation equivalence）和耦合相似性（coupled similarity）**下的行为仍有待探索。

现有关于其他等价关系的结论显示出不同的成功程度：

• 对于双模拟，商化是规范的（在同构意义下唯一）且是极小的。
• 对于迹等价，极小商可能不是唯一的，且计算其复杂度为 PSPACE 完全。
• 对于弱模拟和耦合相似性，目前尚不清楚是否存在规范商或极小商，其计算复杂度也尚未确立。

本文研究了弱模拟等价 ($\equiv_S$) 和耦合相似性 ($\equiv_{CS}$) 的规范商与极小商的存在性，并分析了寻找它们的计算复杂度。

方法论

作者开发了抽象程序，将任意 LTS 转换为其等价类的代表。该方法依赖于基于模拟偏序属性和特定 $\tau$-律（控制不可观测动作的公理）的一系列变换。

1. 全称商与冗余消除

过程始于 $\forall$-商，它合并所有等价状态。然而，仅靠这一点是不够的，因为它可能会引入“惰性”转换（在等价状态之间的转换）和“重复”转换。

• 覆盖转换（Covered Transitions）： 作者将“重复转换”的概念推广为覆盖转换。如果存在另一个转换 $p' \xrightarrow{\alpha} q'$ 使得 $p$ 可以通过 $\tau$-步到达 $p'$ 且 $q$ 被 $q'$ 模拟（$q \sqsubseteq_x q'$），则称转换 $p \xrightarrow{\alpha} q$ 是被覆盖的。
• 移除覆盖转换可以保持等价性并减少状态空间，但所得的 LTS 不一定具有规范性或极小性。

2. $\tau$-去饱和化（为了规范性）

为了实现规范性，本文引入了基于公理 $\tau.x = x$ 和 $\tau.(\tau.x + y) = \tau.x + y$ 的 $\tau$-去饱和化（$\tau$-desaturation）。

• 操作： 如果状态 $p$ 有一个到 $q$ 的 $\tau$-转换（$p \xrightarrow{\tau} q$），则移除该转换，并将 $p$ “饱和”为 $q$ 的所有传出转换。对于耦合相似性，这要求 $q$ 必须有一个传出的 $\tau$-转换。
• 效果： 该变换消除了连续的 $\tau$-转换，并减少了指向状态的传入转换。重复应用该操作会终止，从而产生一个**去饱和（desaturated）**的 LTS。
• 结果： 通过结合 $\forall$-商、$\tau$-去饱和化、覆盖转换移除以及不可达状态移除，作者定义了一个**简化（reduced）的 LTS。他们证明了任何两个等价的简化 LTS 都是同构的，从而确立了规范商（canonical quotient）**的存在性。

3. $\tau$-饱和化（为了极小性）

为了实现极小性，作者引入了逆向操作：$\tau$-饱和化（$\tau$-saturation）。

• 操作： 如果 $q \sqsubseteq_x p$，则可以添加一个 $\tau$-转换 $p \xrightarrow{\tau} q$。这可能会使现有的转换变得“可被覆盖”，从而允许移除它们。
• 优化挑战： 选择添加哪些 $\tau$-转换具有非确定性。不同的选择会导致不同的简化结果。选择最优的 $\tau$-饱和步骤以实现最大化简化的问题被证明等价于集合覆盖问题（Set Cover Problem）。
• 算法： 极小商程序首先计算规范商，然后识别每个状态的“可被覆盖”转换。它为每个状态求解一个集合覆盖实例，以确定添加 $\tau$-转换的最少集合，从而能够移除最大数量的其他转换。

核心贡献与结果

1. 规范商的存在性

本文证明了对于弱模拟等价和耦合相似性，规范商均存在。

• 定理 4.4： 两个简化 LTS（去饱和、无覆盖转换、无不可达状态、无惰性转换、无等价状态）是等价的，当且仅当它们是同构的。
• 算法 1： 提供了一个计算该规范商的多项式时间程序。

2. 极小商的复杂度

本文确立了计算极小商（具有字典序最小的状态数和转换数的商）是 NP 完全的。

• 定理 5.5： 关于 $\equiv_x$ 的极小化是 NP 难的。这是通过从集合覆盖问题进行归约来证明的。
• 启示： 与双模拟极小化（多项式时间）不同，对于模拟等价，寻找绝对最小的等价 LTS 在一般情况下是计算上难以处理的。
• 算法 2： 描述了一个通过利用集合覆盖问题的预言机（oracle）来计算极小商的程序。虽然该算法本身不是多项式时间的（由于存在 NP 难的子问题），但它允许使用最先进的集合覆盖求解器。为这些求解器生成的实例通常很小（受限于状态的出度）。

3. 与双模拟的区别

这些结果强调了与双模拟的根本分歧：

• 对于双模拟，极小商是唯一的且可在多项式时间内计算。
• 对于模拟等价，极小商可能不是唯一的（对于同一个等价类，可以存在多个非同构的极小 LTS），且寻找它是 NP 完全的。

重要性与主张

本文声称将商化的理论理解扩展到了研究较少的双模拟和迹等价之外。

• 泛化： 该方法泛化了“重复转换”的概念，并利用特定于模拟偏序的 $\tau$-律来推导规范形式。
• 实用性： 虽然寻找绝对极小商是 NP 完全的，但所提出的方法允许从业者利用高效的集合覆盖求解器来实现显著的状态空间缩减，因为在 LTS 极小化中出现的特定实例通常规模较小。
• 谦逊性： 作者明确指出，他们的结果依赖于弱模拟和耦合相似性的特定 $\tau$-律。他们并不声称这些结果可以推广到整个线性时间-分支时间谱，这表明不同的等价关系可能需要不同的 $\tau$-律和变换策略。

总之，本文提供了获得弱模拟和耦合相似性的规范商与极小商的首个抽象程序，并将前者表征为多项式时间可计算，后者表征为 NP 完全。