PRISM 逻辑运算符
介绍
在PRISM概率模型检测工具中，逻辑运算符是构建属性规范的核心元素。它们用于组合和比较状态或路径上的表达式，从而定义系统需要满足的性质。无论是验证概率性、时序性还是奖励属性，逻辑运算符都扮演着关键角色。本节将详细介绍PRISM支持的逻辑运算符及其使用方法。
PRISM支持以下类型的逻辑运算符：
- 命题逻辑运算符：与（
&）、或（|）、非（!） - 概率运算符：
P（概率）、S（稳态概率）、R（奖励） - 时序逻辑运算符：
U（直到）、F（最终）、G（全局）
命题逻辑运算符
PRISM继承了传统命题逻辑的运算符，用于组合布尔表达式。
1. 与运算符 (&)
表示逻辑“与”，当左右两边的表达式均为真时结果为真。
语法示例：
prism
"A & B" // 当A和B同时为真时成立
实际案例： 验证系统同时满足“温度低于阈值”和“压力正常”：
prism
"temp_low & pressure_ok"
2. 或运算符 (|)
表示逻辑“或”，当任意一边的表达式为真时结果为真。
语法示例：
prism
"error | warning" // 当error或warning为真时成立
3. 非运算符 (!)
表示逻辑“非”，对表达式取反。
语法示例：
prism
"!failure" // 当failure为假时成立
提示
运算符优先级：! > & > |。使用括号可以显式指定优先级，例如 (A | B) & C。
概率运算符
PRISM通过概率运算符描述系统行为的概率性质。
1. P 运算符
用于计算路径属性成立的概率。
语法：
prism
"P=? [path_formula]" // 计算路径公式的概率
示例： 计算系统在10步内达到目标状态的概率：
prism
"P=? [F<=10 goal]"
2. S 运算符
计算稳态概率（长期运行下的概率分布）。
语法：
prism
"S=? [condition]" // 计算稳态下满足条件的概率
示例： 计算系统处于“空闲”状态的稳态概率：
prism
"S=? [idle]"
3. R 运算符
用于分析奖励（或代价）属性。
语法：
prism
"R{"reward_name"}=? [F target]" // 计算达到target前的累积奖励
示例： 计算系统崩溃前的平均能耗：
prism
"R{"energy"}=? [F crashed]"
时序逻辑运算符
PRISM支持**线性时序逻辑（LTL）和计算树逻辑（CTL）**的运算符。
1. U（Until）
表示“直到”关系：A U B 表示“A一直成立，直到B成立”。
示例：
prism
"P>=0.9 [safe U completed]" // 安全状态持续直到任务完成的概率≥90%
2. F（Finally）
表示“最终成立”：F A 等价于 true U A。
示例：
prism
"P=? [F<=5 error]" // 5步内发生错误的概率
3. G（Globally）
表示“全局成立”：G A 表示“A在所有状态下成立”。
示例： 验证系统始终不会崩溃：
prism
"P>=0.99 [G !crashed]"
综合案例
案例：通信协议可靠性
验证一个通信协议满足：
- 消息最终以至少95%的概率被送达；
- 在送达前不会丢失。
PRISM属性规范：
prism
// 条件1：消息最终送达的概率≥95%
"P>=0.95 [F delivered]"
// 条件2：在送达前不丢失的概率≥99%
"P>=0.99 [(!lost) U delivered]"
总结
PRISM的逻辑运算符分为三类：
- 命题逻辑运算符：
&、|、!； - 概率运算符：
P、S、R； - 时序逻辑运算符：
U、F、G。
通过组合这些运算符，可以灵活地定义复杂的系统性质。
练习与资源
练习
- 编写一个属性，验证系统在100步内以至少80%的概率进入“安全模式”。
- 使用
R运算符计算系统在崩溃前的平均运行时间。
扩展阅读
- PRISM官方文档：Properties Specification
- 《Principles of Model Checking》第10章（时序逻辑）