PRISM 时间属性
引言
在概率模型检查中，时间属性用于描述系统在特定时间范围内的行为。PRISM支持对连续时间马尔可夫链（CTMC）和马尔可夫决策过程（MDP）等模型的时间相关性质进行形式化规约和验证。本节将介绍PRISM中时间属性的语法、语义及实际应用。
时间属性基础
PRISM的时间属性通过PCTL（概率计算树逻辑）或CSL（连续随机逻辑）扩展表达，主要分为两类：
- 瞬时概率（Transient Probability）：系统在特定时间点满足某条件的概率。
- 稳态概率（Steady-state Probability）：系统在长期运行后满足某条件的概率。
语法结构
prism
// 瞬时概率
P=? [ F<=T "目标状态" ]
// 稳态概率
S=? [ "状态条件" ]
其中 T 为时间界限，F 表示“最终”（Future）。
瞬时概率示例
分析一个简单CTMC模型（如队列系统）在时间 T=5 时处于“队列满”状态的概率：
prism
// 模型定义（省略部分代码）
module Queue
state : [0..10] init 0;
[] state < 10 -> 0.5 : (state'=state+1);
[] state > 0 -> 1.0 : (state'=state-1);
endmodule
// 属性查询
P=? [ F<=5 state=10 ]
输出结果：0.217（表示5个单位时间后队列满的概率为21.7%）。
稳态概率示例
计算同一队列系统长期运行时空闲（state=0）的概率：
prism
S=? [ state=0 ]
输出结果：0.333（稳态时空闲概率约33.3%）。
时间界限操作符
PRISM支持更复杂的时间界限表达式：
F<=T：在时间T内最终满足条件。F[T1..T2]：在时间区间[T1,T2]内满足条件。
prism
// 查询“系统在时间3到7之间首次达到状态5”的概率
P=? [ F[3..7] state=5 ]
实际案例：网络协议超时
假设一个网络协议在超时时间为 T=10 时重传数据包，验证其成功传输的概率：
prism
// 模型定义（简化）
module Protocol
attempts : [0..3] init 0;
[] attempts<3 -> 0.9 : (attempts'=0) // 成功
+ 0.1 : (attempts'=attempts+1); // 失败
endmodule
// 查询“10秒内成功传输”的概率
P=? [ F<=10 attempts=0 ]
提示
在CTMC中，时间单位通常由模型的速率参数决定。确保时间界限 T 与模型的实际时间尺度匹配。
总结
| 属性类型 | 语法示例 | 适用场景 |
|---|---|---|
| 瞬时概率 | P=? [ F<=T "cond" ] | 短期行为分析 |
| 稳态概率 | S=? [ "cond" ] | 长期稳定性评估 |
| 时间区间 | F[T1..T2] | 阶段性事件验证 |
练习与扩展
- 修改队列模型，比较
state=5在T=2和T=8时的瞬时概率差异。 - 为协议模型添加超时速率参数，观察其对
P=? [ F<=10 attempts=0 ]的影响。
备注
进一步学习：参考PRISM官方文档中的时间属性章节。