PRISM 模型转换技术

引言

PRISM模型转换技术是将现实系统抽象为PRISM支持的数学模型的关键步骤。本节将介绍如何将不同计算模型转换为PRISM规范，包括状态空间转换、概率分布映射和时序特性处理。

为什么需要模型转换？

实际系统往往采用混合建模方式，而PRISM需要标准化的输入格式。转换技术帮助我们：

• 统一不同来源的模型描述
• 适配PRISM的模型检查算法
• 保持语义等价性

基础转换原理

1. 状态空间转换

所有PRISM模型都基于离散状态空间，转换时需要：

示例：将温度连续区间离散化

// 原始范围: 20.0-25.0°C
// 离散化为5个状态
formula temp_state = (temp < 21.0) ? 0 : 
                    (temp < 22.0) ? 1 :
                    (temp < 23.0) ? 2 :
                    (temp < 24.0) ? 3 : 4;

2. 概率分布处理

不同模型类型的转换重点：

源模型类型	目标模型类型	关键转换操作
DTMC	MDP	添加非确定性选择
CTMC	DTMC	均匀化处理
MDP	DTMC	策略固定

具体转换技术

DTMC → MDP 转换

通过引入非确定性选择扩展模型：

prism

// 原始DTMC模块
module example
    s : [0..1] init 0;
    [] s=0 -> 0.5:(s'=0) + 0.5:(s'=1);
    [] s=1 -> 1:(s'=0);
endmodule

// 转换后MDP
module example_mdp
    s : [0..1] init 0;
    [action1] s=0 -> 0.5:(s'=0) + 0.5:(s'=1);
    [action2] s=0 -> 0.8:(s'=0) + 0.2:(s'=1);
    [] s=1 -> 1:(s'=0);
endmodule

CTMC → DTMC 均匀化

通过引入最大退出率实现转换：

1. 计算所有状态的最大退出率 q_max
2. 添加自循环概率 1 - q/q_max

prism

// 原始CTMC (速率q1=2.0, q2=1.0)
module ctmc
    s : [0..1] init 0;
    [] s=0 -> 2.0:(s'=1);
    [] s=1 -> 1.0:(s'=0);
endmodule

// 均匀化后DTMC (q_max=2.0)
module uniformized
    s : [0..1] init 0;
    [] s=0 -> 1.0:(s'=1) + 1.0:(s'=0);  // 2.0/2.0=1.0, 1-1=0 → 实际应为1.0:(s'=1)
    [] s=1 -> 0.5:(s'=0) + 0.5:(s'=1);  // 1.0/2.0=0.5
endmodule

注意

均匀化会引入时间缩放，需要调整时间相关属性的验证方式。

实际应用案例

网络协议重传机制建模

原始系统描述：

• 数据包发送成功率60%
• 失败后最多重试3次
• 每次重试间隔1-3秒随机

转换为PRISM MDP模型：

prism

module sender
    attempts : [0..3] init 0;
    sending : bool init true;
    
    [send] sending & attempts<3 -> 
        0.6:(sending'=false) + 
        0.4:(attempts'=min(attempts+1,3));
    
    [retry] !sending -> 
        1/3:(sending'=true) & (attempts'=0) +
        1/3:(sending'=true) & (attempts'=0) +
        1/3:(sending'=true) & (attempts'=0);
endmodule

总结与练习

关键要点

• 模型转换需要保持行为等价性
• 不同模型类型转换的侧重点不同
• 均匀化是CTMC→DTMC的标准方法
• 非确定性引入是DTMC→MDP的核心

推荐练习

1. 将以下CTMC转换为DTMC：

   状态A →(速率3.0)→ 状态B
   状态B →(速率1.5)→ 状态A

2. 为简单的交通灯系统（固定周期切换）创建MDP模型，允许传感器触发提前切换

扩展阅读

• PRISM手册第7章 "Model Types"
• 《Principles of Model Checking》第10章
• 均匀化算法原始论文 (Jensen, 1953)