A Diagrammatic Axiomatisation of Behavioural Distance of Nondeterministic Processes

以下是论文《非确定性过程行为距离的图示公理化》（作者：Różowski, Piedeleu, Silva, 和 Zanasi）的详细技术总结。

1. 问题陈述

本文解决了定量比较非确定性过程行为的挑战。

• 背景： 传统的进程代数和自动机理论依赖于布尔等价概念（如双模拟、语言等价）。虽然这些概念很有用，但对于涉及概率或定量方面的现代系统而言往往过于僵化，因为在这些系统中，人们需要衡量两个行为“相距多远”，而不仅仅是判断它们是否相同。
• 具体差距： 尽管行为距离已在概率系统和确定性有限自动机（DFA）中得到研究，但针对非确定性过程（特别是 Milner 图表）仍缺乏一个健全且完备的公理框架。
• 挑战： 非确定性将语义焦点从语言等价转移到了双模拟。现有的代数语法（如带有绑定算子的正则表达式）难以在不依赖复杂替换机制的情况下以组合方式捕捉这些行为。此外，将定量推理扩展到非确定性系统需要处理度量的"Hausdorff 提升”，这在公理化方面在技术上非常困难。

2. 方法论

作者采用图示方法，利用弦图（对称幺半范畴的图形语言）来表示和推理过程行为。

• 语义模型（图表）： 本文聚焦于Milner 图表，它通过将接受状态替换为变量输出，推广了有限状态非确定性自动机（NFA）。其语义定义在配备伪度量结构的正则行为（$\Omega$）范畴上。
• 度量定义： 行为距离通过余代数框架定义。它利用：
  1. 转移提升： 将状态上的度量提升为转移（标记边和变量输出）上的度量。
  2. Hausdorff 提升： 将度量提升为转移集合（以处理非确定性）。
  3. 不动点刻画： 距离是伪度量格上单调算子的最小不动点。它通过双模拟的分层（Hennessy-Milner 逻辑）具体刻画，即如果两个过程在深度 $n$ 上双模拟但在 $n+1$ 上不是，则距离为 $2^{-n}$。
• 语法（弦图）： 作者使用弦图作为语法。这一选择提供了：
  • 无变量表示： 递归通过反馈回路（迹）处理，而非显式的绑定算子和替换。
  • 组合语义： 图表自然地映射到正则行为的范畴结构。
  • Int 构造： 为了处理双向数据流（输入/输出）和反馈回路，作者利用Int 构造将行为的迹幺半范畴转换为紧闭范畴，从而允许局部导线弯曲。

3. 主要贡献

A. 定量推理系统

本文提出了一组定量等式规则（推理系统），用于推导行为距离的界限（$s \equiv_\epsilon t$）。

• 标准度量规则： 自反性、对称性、三角不等式，以及一条“连续性”规则（如果对于所有 $\epsilon' > \epsilon$ 都有 $s \equiv_{\epsilon'} t$，则 $s \equiv_\epsilon t$）。
• 组合规则： 保持非扩张性的顺序组合和并行组合（张量）规则。
• 特定领域规则：
  • (Pref)： 用动作 $a$ 前缀化会将距离减半（$d(a.s, a.t) = \frac{1}{2}d(s, t)$）。这捕捉了区分两个过程需要多一步的直观理解。
  • (Codel)： 没有初始状态（死锁）的图表与空图表的距离为 0。
  • 等式公理： 一组公理（A1-B11）捕捉强双模拟（距离为 0），包括非确定性选择、变量合并和递归（Conway 理论公理）的定律。

B. 健全性与完备性

核心的技术成就在于证明了该推理系统既是健全的又是完备的。

• 健全性（定理 16）： 每一个可推导的定量等式 $f \equiv_\epsilon g$ 都是有效的（即实际行为距离 $d(\llbracket f \rrbracket, \llbracket g \rrbracket) \leq \epsilon$）。
• 完备性（定理 31）： 如果两个图表之间的行为距离 $\leq \epsilon$，则方程 $f \equiv_\epsilon g$ 可以使用提出的规则推导出来。
  • 证明策略： 完备性证明涉及将任意图表转换为范式（表示有限预图表）。然后，它使用推理规则在语法上模拟 Hausdorff 提升和不动点迭代（Kleene 定理）的计算。连续性 (Cont) 规则对于缩小语法近似与精确极限之间的差距至关重要。

C. 范畴结构

本文确立了正则行为范畴（$\text{RegBeh}$）是一个Conway 理论（一种特定类型的迹幺半范畴），并且伪度量结构使其成为伪度量空间范畴（$\text{PMet}$）上的富化范畴。这确保了所有范畴运算（组合、张量、迹/对偶）都是非扩张的。

4. 结果

• 形式刻画： 本文提供了 Milner 图表（带输出的非确定性过程）行为距离的第一个完备公理化。
• 度量的语法模拟： 作者证明，复杂的度量计算（如转移集合之间的 Hausdorff 距离）可以通过弦图的纯语法操作来模拟。
• 示例应用： 本文包含了一个详细的推导，展示了如何证明两个特定图表（一个在两个 'a' 后死锁，另一个具有无限 'a'）之间的距离恰好为 $1/4$。这是通过展开递归并应用两次 (Pref) 规则实现的。

5. 意义

• ** bridging 理论与实践：** 通过从布尔等价转向定量距离，这项工作使得对“几乎等价”这一有意义概念的系统进行更细致的分析成为可能（例如，在近似系统或概率系统的验证中）。
• 统一的图示框架： 使用弦图避免了传统进程代数中变量绑定和替换的复杂性。这暗示了一条通往统一框架的道路，用于公理化各种计算模型（确定性、非确定性、概率性、加权）中的等价性和距离。
• 未来工作的基础： 本文为将这些结果扩展到加权转移系统和概率自动机奠定了基础，在这些领域中行为距离更为关键。它还暗示了在反编译算法推理和带测试的受保护 Kleene 代数（GKAT）中的潜在应用。
• 理论进步： 它将余代数行为度量、定量等式逻辑和图示代数联系起来，展示了这些领域如何整合以解决进程理论中长期存在的问题。

总之，本文成功地将非确定性过程行为距离的抽象、余代数定义转化为具体的、图示的且完全公理化的演算，证明了关于过程行为的定量推理可以完全通过弦图的语法操作来完成。