跳到主要内容

PRISM 结果可视化工具

介绍​

PRISM（Probabilistic Symbolic Model Checker）是用于分析概率系统的工具，而结果可视化是其核心功能之一。通过图表、曲线和直方图等形式，PRISM能直观展示模型验证结果（如概率、期望值等），帮助用户理解复杂数据。本章将介绍PRISM支持的多种可视化方法及其应用场景。

基础可视化类型​

PRISM提供以下主要可视化方式：

  1. 时间序列图：展示随时间或参数变化的概率/期望值。
  2. 直方图：比较离散状态下的结果分布。
  3. 参数扫描图：分析模型参数对结果的影响。
提示

在PRISM GUI中，可视化功能默认自动启用，也可通过命令行工具生成数据后导入第三方工具（如Python或MATLAB）进一步处理。

示例1：时间序列图​

场景描述​

假设我们有一个简单的马尔可夫链模型，需要分析系统在10步内达到目标状态的概率变化。

PRISM 代码​

模型定义（model.pm）：

prism
dtmc
module System
  s : [0..2] init 0;
  [] s=0 -> 0.6 : (s'=1) + 0.4 : (s'=2);
  [] s=1 -> 0.7 : (s'=0) + 0.3 : (s'=2);
  [] s=2 -> 1 : (s'=2);
endmodule

属性查询（props.pctl）：

prism
P=? [ F<=10 s=2 ]

可视化步骤​

  1. 在PRISM GUI中加载模型和属性文件。
  2. 执行验证后，结果将自动显示为时间序列图：

示例2：参数扫描图​

场景描述​

分析模型参数（如转移概率）对最终结果的影响。

PRISM 代码​

修改模型为参数化版本：

prism
dtmc
const double p;
module System
  s : [0..2] init 0;
  [] s=0 -> p : (s'=1) + (1-p) : (s'=2);
  [] s=1 -> 0.7 : (s'=0) + 0.3 : (s'=2);
endmodule

操作步骤​

  1. 在GUI中选择"Experiment" → "Parametric"。
  2. 设置参数p范围为[0,1]，步长0.1。
  3. 执行扫描后生成曲线图，显示不同p值对应的P(F s=2)。

实际案例：网络可靠性分析​

问题描述​

评估一个三节点网络的可靠性，其中每条链路有独立故障概率。

关键步骤​

  1. 构建CTMC模型描述网络状态。
  2. 查询属性：R{"reliability"}=? [ C<=T ]（T时间内系统可靠的概率）。
  3. 可视化结果：
警告

注意坐标轴范围设置！默认自动缩放可能导致小变化不明显，建议手动调整yAxis范围以突出差异。

高级技巧​

导出数据​

PRISM支持将结果导出为CSV或MATLAB格式：

prism
# 命令行示例
prism model.pm props.pctl -exportresults result.csv

自定义绘图​

使用Python处理导出的数据：

python
import matplotlib.pyplot as plt
import pandas as pd
data = pd.read_csv("result.csv")
data.plot(x="param", y="probability")
plt.show()

总结​

PRISM的可视化工具能显著提升概率模型验证结果的可解释性。关键要点：

  • 时间序列图适合展示动态过程
  • 参数扫描揭示系统敏感性
  • 导出功能支持进一步定制分析

延伸练习​

  1. 修改示例1中的初始概率，观察图形变化。
  2. 尝试在参数扫描中同时调整两个参数，生成三维曲面图。

附加资源​

  • PRISM官方文档：可视化章节
  • 《概率模型检验》第6章（可视化分析方法）