进程代数

进程项与操作语义 ​

一个简化进程语言可由

$$P::=0\mid a.P\mid P+Q\mid P\parallel Q\mid P\setminus H$$

生成。$0$ 不执行动作，$a.P$ 先执行 $a$ 再成为 $P$，$+$ 是外部或非确定选择，$\parallel$ 是并行组合，隐藏把 $H$ 中动作变为内部 $\tau$。

语义由结构操作规则生成LTS公理库标号转移系统Labeled transition system · Labelled transition system · LTS在状态转移上标记动作，明确路径、可达性、使能动作以及终止与死锁的行为模型。。例如

$$\frac{}{a.P\stackrel{a}{\to }P},\frac{P\stackrel{a}{\to }{P}^{\prime }}{P+Q\stackrel{a}{\to }{P}^{\prime }},$$

并行规则允许组件独立动作，也可规定互补动作 $a,\overline{a}$ 同步为 $\tau$。不同进程代数的通信与选择规则不同，不能只看相似语法符号。

握手协议轨迹 ​

客户端

$$C=send.recv.C$$

反复发送后等待接收；服务端

$$S=\overline{send}.\overline{recv}.S.$$

若互补动作必须握手，组合 $C\parallel S$ 先同步 send，再同步 recv，每轮回到初始组合状态。隐藏握手名后，外部观察可能只看见两个 $\tau$。

若服务端改成 $\overline{recv}.\overline{send}.S$，初态双方等待不同握手，没有转移，形成死锁。两个组件各自都能在某环境运行，不保证组合后协议顺序兼容。

若并行规则还允许 send 在没有服务端时独立发生，模型变成异步或广播式通信，前述死锁可能消失。动作到底必须同步、可独立还是写入缓冲，必须由 SOS 规则决定，不能靠动作名称的自然语言含义。

引入显式 FIFO 时，组合状态需包含队列内容，send 变成入队、recv 变成出队。递归客户端即使控制项有限，未界队列也可生成无限状态图。

选择与并行的代数律 ​

在强互模拟公理库互模拟Bisimulation · Bisimulation relation · Bisimilarity以同一关系双向匹配两个系统的每一步，从而保留分支结构的行为等价。下，选择常满足交换、结合、幂等：

$$P+Q\sim Q+P,P+P\sim P.$$

并行常满足交换和结合到结构同构，但分配律

$$P\parallel (Q+R)\stackrel{?}{\sim }(P\parallel Q)+(P\parallel R)$$

一般会因选择时机和同步环境不同而失败。代数律必须相对于具体操作语义与等价关系证明。

展开律可把有限并行项转换成其当前可执行动作之和，支撑等式推理；递归进程还需 guardedness 等条件保证方程有规范行为解。

行为等价的选择 ​

强 bisimulation 逐步匹配全部动作，连内部 $\tau$ 也不可跳过。弱 bisimulation 允许有限内部步骤被隐藏，更适合实现细化；trace equivalence 更粗，只比较可见动作序列。

等价越粗，可应用的代数替换越多，却可能丢掉死锁、分支时机或发散。若把进程项放入任意上下文，需要等价是 congruence；单纯的 weak bisimilarity 在某些选择算子下需加强为 observational congruence。

验证“两个孤立项等价”不自动允许在协议任意位置替换。上下文可能通过同步动作观察原先隐藏的分支。

failure semantics 不只记录 trace，还记录执行该 trace 后进程可稳定拒绝的事件集合。进程“内部选择只接受 $a$ 或只接受 $b$”与“始终同时提供 $a,b$”可以有相同短 trace，却有不同 refusal；对死锁自由接口，后者差异至关重要。

must testing 量化所有内部计算：若某个内部选择会永久发散，哪怕另一个分支成功，测试也不一定必然通过。may testing 只需存在成功运行，保证更弱。选择等价前应先确定需求量词。

CCS、CSP 与 ACP 边界 ​

CCS 强调互补端口同步和 restriction，CSP 使用事件同步、trace/failure/divergence 语义，ACP 以通信函数和代数公理组织组合。它们共享进程代数思想，不是同一套操作符的不同拼写。

进程代数描述离散交互行为，不自动带时间、概率、资源消耗或共享内存弱序。相应扩展需要改变语义和等价概念。

模型检查可对有限状态进程项展开 LTS；递归和数据参数可能产生无限状态，代数语法有限不等于状态图有限。

递归与唯一解 ​

递归方程 $X=a.X$ 描述无限重复动作。guarded recursion 要求递归变量位于动作前缀之后，使有限观察深度逐步揭示行为，并支持相应行为等价下的唯一解原理。

未 guarded 的 $X=X+P$ 可能有许多解，不能仅凭代数移项选一个“最自然”进程。工具用命名定义时仍需检查递归语义是最小、最大还是操作规则生成的进程图。

发散进程 $DIV=\tau .DIV$ 在弱 trace 观察下可能看似什么都不做，却会永久占据执行。若规格关心 must testing、响应或资源，必须采用 divergence-sensitive 语义。

递归 operational semantics 常用 unfolding rule：若定义体展开后可做 $a$，递归常量也可做 $a$。实现若每次展开都复制完整语法树，会无限增长；状态图生成应按递归变量共享节点，同时确保参数化递归的不同实参仍被区分。

开放环境的测试边界 ​

一个进程的可见动作往往还需环境握手。testing equivalence 把进程放入观察者上下文，并比较可能成功或必然成功；它能区分仅靠内部非确定“偶尔成功”和所有调度都能成功。

这说明单一 equivalence 不是进程代数的附属细节，而是决定哪些代数律和替换推论成立的语义选择。

隐藏操作还可能把原本外部可控的选择变成内部选择，从而改变 testing 结果。代数化简若先隐藏再使用外部选择律，必须确认该律对 $\tau$ 分支仍成立。

参考资料

• Robin Milner, Communication and Concurrency, Prentice Hall, 1989, Chs. 1–7。
• C. A. R. Hoare, Communicating Sequential Processes, Prentice Hall, 1985, Chs. 1–5。
• J. C. M. Baeten, “A Brief History of Process Algebra,” Theoretical Computer Science 335(2–3), 2005, pp. 131–146。