跳到主要内容

PRISM 模型学习

介绍​

PRISM（Probabilistic Symbolic Model Checker）是一个用于建模和分析概率系统的工具，支持离散/连续时间马尔可夫链（DTMC/CTMC）、马尔可夫决策过程（MDP）等模型。本节将介绍如何用PRISM语言构建模型，并通过案例演示其应用。

关键概念
  • 概率模型：描述系统在不同状态间转移的概率行为。
  • PRISM语言：基于模块化状态描述，支持变量、同步动作和概率/非确定性选择。

基础模型结构​

PRISM模型由模块（Modules）、变量（Variables）和命令（Commands）组成。以下是一个简单的DTMC模型示例：

prism
// 两状态天气模型 (DTMC)
dtmc

module Weather
  sunny : [0..1] init 1; // 初始为晴天（1=晴天，0=雨天）

  [] sunny=1 -> 0.7 : (sunny'=1) + 0.3 : (sunny'=0); // 保持晴天或转为雨天
  [] sunny=0 -> 0.4 : (sunny'=0) + 0.6 : (sunny'=1); // 保持雨天或转为晴天
endmodule

输出分析：通过PRISM验证"长期处于晴天的概率"：

prism
P=? [ F (steadyState) & sunny=1 ]

进阶模型技术​

1. 同步动作与多模块交互​

多个模块通过同步标签（如 [action]）协调动作。例如，一个故障恢复系统：

prism
module Server
  state : [0..2] init 0; // 0=运行, 1=故障, 2=恢复中
  [fail] state=0 -> 0.01 : (state'=1); // 故障概率1%
  [recover] state=1 -> 1 : (state'=2); // 开始恢复
endmodule

module RepairTeam
  idle : bool init true;
  [recover] idle=true -> (idle'=false); // 同步恢复动作
endmodule

2. 代价与奖励​

PRISM支持在模型中附加奖励（Rewards），用于量化性能指标：

prism
rewards "Energy"
  [act] state=0 : 5; // 执行动作消耗5单位能量
endrewards

验证总期望能耗：

prism
R{"Energy"}=? [ C<=100 ] // 100步内的累计能耗

实际案例：网络协议分析​

分析一个简单的ARQ（自动重传请求）协议，其中数据包有10%丢失概率：

prism
module Sender
  sent : bool init false;
  [send] !sent -> 0.9 : (sent'=true) + 0.1 : (sent'=false);
  [ack] sent -> (sent'=false);
endmodule

module Receiver
  [send] true -> (received'=true); // 接收数据包
  [ack] received -> (received'=false);
endmodule

验证"数据包最终成功传输的概率"：

prism
P=? [ F sent=false & received=false ] // 传输完成

总结与练习​

关键点总结​

  1. PRISM模型通过模块和命令描述概率行为。
  2. 同步动作实现复杂系统交互。
  3. 奖励机制扩展了定量分析能力。

练习建议​

  1. 修改天气模型，增加"多云"状态（概率自行设定）。
  2. 为ARQ协议添加超时重传机制（提示：使用时钟变量）。
扩展学习