进程演算 进程演算是描述并发系统行为的形式化模型，侧重于进程间的通信和交互。下面从基础概念到理论扩展逐步展开： 基本概念：进程与动作 进程 代表一个独立的计算单元，例如程序线程或分布式系统组件。 动作 是进程的基本操作，分为两类： 发送动作 （如 a!v 表示通过通道 a 发送值 v ）； 接收动作 （如 a?x 表示通过通道 a 接收值并存入变量 x ）。 进程构造算子 进程通过算子组合成更复杂的行为： 前缀 （ α.P ）：执行动作 α 后继续执行进程 P 。 选择 （ P + Q ）：非确定性地执行 P 或 Q 。 并行组合 （ P | Q ）： P 和 Q 并发执行，可通过共享通道交互。 限制 （ (νa)P ）：将通道 a 的作用域限制在 P 内，实现信息隐藏。 递归 （ rec X. P ）：允许定义无限行为的进程（ X 为进程变量）。 通信与同步 当进程 a!v.P 与 a?x.Q 并行时，它们通过通道 a 同步：值 v 从发送方传递到接收方，系统演变为 P | Q[v/x] （替换 x 为 v ）。 同步机制避免了共享内存的竞争条件，强调消息传递。 语义模型：互模拟与等价性 互模拟 是进程间行为等价的判定工具：若两个进程能相互模拟对方的每一步动作，则它们等价。 强弱互模拟 ：强互模拟要求动作完全匹配；弱互模拟忽略内部不可见动作（如 τ ）。 扩展变体与应用 π-演算 ：引入通道传递能力（通道作为通信内容），支持动态拓扑变化。 应用场景 ：协议验证（如TCP握手）、分布式算法建模、安全协议分析（通过限制算子隔离敏感通道）。 通过以上步骤，进程演算将并发系统抽象为可推理的代数结构，为形式化验证提供基础。