mCRL2 进程表达式语法详解

进程表达式基础概念

mCRL2 是一种形式化建模语言，专门用于描述并发系统的行为。在这个框架中，进程(Process)是最核心的实体，用于表示系统或组件的行为模式。

基本语法结构

进程表达式由一系列动作(Action)通过操作符组合而成。最基本的操作符包括：

• 顺序组合 .：表示动作的先后顺序
• 选择组合 +：表示行为的分支选择

例如：

act a, b, c;
proc P = a . b . c;  // 顺序执行a、b、c
     Q = a + b;      // 选择执行a或b

递归定义

进程可以通过递归定义来表达无限行为：

act read, write;
proc P = read . write . P;  // 不断重复读写
init P;  // 系统从P开始执行

高级进程特性

多动作(Multi-action)

mCRL2 允许将多个动作组合成一个原子性的多动作，使用 | 分隔：

act read, write;
proc P = (read | write) . P;  // 读写同时发生

多动作是解决状态空间爆炸问题的有效手段，通过将相关动作组合，可以减少系统状态数量。

特殊进程元素

• tau：表示不可见的内部动作
• delta：表示死锁，进程无法继续执行

数据与进程的交互

带参数的进程

进程可以携带数据参数，形成数据驱动的行为：

act tick;
proc Clock(n: Nat) = tick . Clock(n + 1);
init Clock(0);  // 从0开始计数

条件控制

使用条件表达式可以创建分支行为：

act tick, reset;
proc Clock(n: Nat) = 
  (n < 99) -> tick . Clock(n + 1) <> tick . Clock(0)  // 模100计数
  + (n < 50) -> reset . Clock(0);  // 条件重置

求和操作符

sum 操作符表示从某个域中选择值：

act read, write: Nat;
proc Buffer = sum n: Nat . read(n) . write(n) . Buffer;  // 读取并回写任意自然数

并发与通信

并行组合

|| 操作符表示进程并行执行：

a || b  // 等价于 a.b + b.a + a|b

并行组合会产生所有可能的交错执行序列，这可能导致状态空间急剧增长。

通信机制

mCRL2 提供了专门的通信控制机制：

1. comm：定义哪些动作必须通信
2. allow：指定允许的动作集合
3. block：阻止特定动作

示例通信模式：

allow({c}, 
  comm({send|read -> c}, 
    send(n) || sum m: Nat . read(m) . q(m)
  )
)

进程变换操作

重命名与隐藏

• rename：改变动作名称
• hide：使动作对外不可见

隐藏操作常用于抽象内部行为：

hide({internal}, 
  allow({external, internal}, 
    comm({a|b -> internal}, 
      P || Q
    )
  )
)

时间相关进程

mCRL2 支持时间约束，使用 @ 操作符指定动作执行时间：

Clock(t: Real) = tick@(t + 1) . Clock(t + 1);  // 每秒tick一次

时间约束可以用于建模超时等场景：

sum t: Real . fire@t . sum u: Real. (u <= 5) -> water@(t + u)  // 火灾后5秒内必须喷水

最佳实践建议

1. 合理使用多动作减少状态空间
2. 对无限域求和时添加适当约束条件
3. 通信操作符应按 comm → allow → hide 的顺序使用
4. 时间约束可用于验证系统时序特性
5. 隐藏内部动作后可使用分支互模拟进行状态空间约简

通过掌握这些进程表达式语法，开发者可以精确描述各种并发系统的行为特性，为后续的形式化验证和分析奠定基础。