Effective Stochastic Automata Model Checking by Interval Abstraction (extended version)

问题陈述
随机自动机（Stochastic Automata, SA）是一种用于建模可靠且高性能系统的形式化方法，其中组件故障、维护和服役时间遵循一般连续概率分布（例如 Weibull 分布、均匀分布），而非连续时间马尔可夫链（CTMC）或广义随机 Petri 网（GSPN）所要求的指数分布。虽然 SA 提供了对非马尔可夫系统更真实的表示，但由于连续时间、一般分布和非确定性选择的结合，其分析具有挑战性。

现有的分析方法面临显著的局限性：

• 统计模型检测（SMC）： 如 Fig 等工具采用蒙特卡洛模拟，但它们受限于（弱）确定性 SA，即最小和最大可达概率一致的 SA。它们无法处理一般的非确定性 SA。
• 分析方法： 针对一般 SA 的现有算法（例如 Bryans 等人的算法）依赖于“区域树”（region trees），这需要嵌套积分，随着模型深度的增加，计算量会变得难以承受；或者使用离散化方法，但缺乏工具支持。其他形式化方法如随机混合自动机（SHA）或随机计时自动机（STA）虽然存在，但其模型检测往往因混合可达性的复杂性或数字时钟语义（固定时间步长）的僵化而面临可扩展性问题。

方法论
本文提出了首个专门针对 SA 的、通用的且有效的基于**区间抽象（interval abstraction）**的模型检测方法。核心方法是将无限状态的 SA 转换为一个过近似（overapproximates）原始语义的有限马尔可夫决策过程（MDP）。

1. 区间抽象： 该方法并非通过离散化从连续概率分布（CPD）中采样的结果，而是将每个分布的支持集划分为有限的一组区间。

   • 从 CPD 中采样一个值的过程被替换为一个两步过程：（1）基于该区间的概率质量进行离散概率选择；（2）在给定区间内进行连续的非确定性选择。
   • 这将 SA 转换为一个 MDP，其状态追踪当前位置以及包含活动定时器可能值的区间。

2. 大时间步长语义（Big Time Steps Semantics）： 该方法利用了 SA 的“大时间步长”语义。转换仅在定时器到期或卫语句（guard set）被满足时发生，而不是在每一个无穷小的时间步长处发生。这避免了其他语义中存在的“稠密时间”（dense time）复杂性。

   • 抽象通过区间进行传播。当定时器到期时，系统转换到一个新状态，其中定时器的区间被更新或重置。
   • 由于位置数量是有限的，且区间的组合数量由用户定义的划分所固定，因此生成的 MDP 是有限的。

3. 过近似与界限：

   • MDP 的策略可以从区间内选择精确的值，而原始 SA 语义涉及随机选择。这引入了非确定性，从而过近似了原始系统。
   • 因此，在 MDP 上计算最大可达概率会得到 SA 的上界，而计算最小可达概率则得到下界。
   • 作者证明，随着区间变得越来越小，近似误差预计会降低，尽管在使用所有划分策略时并不保证单调性。

4. 工具与形式化语言：

   • 作者扩展了 Modest 建模语言和 Jani 中间格式以支持 SA，包括定时器声明和卫语句。
   • 一个用 Rust 实现的原型工具执行区间抽象，构建 MDP，并使用价值迭代（Value Iteration, VI）计算界限。

核心贡献

• 首个专用 SA 模型检测器： 本文提出了第一个用于对一般 SA 进行模型检测的工具化方法，且不受确定性子类限制。
• 用于 SA 的区间抽象： 它将区间抽象（此前用于 SHA）专门应用于 SA，将连续概率选择替换为离散概率后接连续非确定性选择，从而产生一个有限的 MDP。
• 形式正确性： 作者提供了形式化证明（定理 1），确立了 MDP 的可达概率对 SA 真实概率的界限关系（$p_{min}^{MDP} \le p_{min}^{SA} \le p_{max}^{SA} \le p_{max}^{MDP}$）。
• 语言扩展： 对 Modest 和 Jani 的扩展为 SA 提供了用户友好的高级建模接口和标准化的模型交换方式。
• 原型实现： 一个基于 Rust 的原型展示了该方法的可行性。

实验结果
作者在三组示例上评估了该原型：

1. 小型 SA 模型： 包括运行示例以及区分策略类的文献模型。该工具成功计算出的界限能够紧密近似真实概率（例如，使用每个区间 0.0125 的概率，用 [0.245, 0.755] 逼近 0.25 和 0.75）。
2. 排队模型： 带有缓冲区限制的非马尔可夫 M/M/1 和 Weibull/E6/1 排队模型。尽管生成了包含数百万状态的 MDP（例如约 330 万个状态），该工具在标准笔记本电脑上运行不到 3 分钟即可完成分析。
3. 文件服务器模型： 与使用数字时钟处理 STA 的 mcsta 工具进行比较。
   • 对于均匀分布，SA 方法在不到 mcsta 30% 的运行时间内实现了更高的精度，这主要是因为“大时间步长”语义导致的 MDP 比数字时钟方法（强制要求时长为 1 的时间步长）显著更小。
   • 对于指数分布，mcsta 的固定宽度区间表现优于原型中的等概率区间，这凸显了区间生成策略对性能的影响。作者指出，在他们的方案中可以对每个定时器进行区间细化，而数字时钟则受限于固定宽度的约束。

意义与主张
本文声称引入了一种通用且有效的 SA 模型检测方法，该方法对输入模型几乎没有限制。

• 可扩展性： 实验结果表明，该方法在处理非平凡示例时具有良好的扩展性，能够处理拥有数十万到数百万个 MDP 状态的模型，而之前的分析技术无法管理这些模型。
• 实用性： 尽管目前是一个原型，但该工具对于规模合理的 SA 运行良好，并能为安全性和性能分析提供有用的界限。
• 灵活性： 该方法支持各种连续分布（均匀分布、指数分布、Erlang 分布、Weibull 分布）以及复杂的特性，如定时器竞争（timer races）和非确定性选择。

作者对细化过程保持谦逊，指出虽然较小的区间通常会提高精度，但由于目前的划分策略，这种关系并非严格单调，且形式化的收敛性证明仍是一个开放性挑战。他们将这项工作定位为未来性能优化工具以及动态故障树和时间限制属性扩展的基础。