发表机构
Kyoto University; National Institute of Informatics（京都大学; 信息学国立研究所）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对概率模型检测的状态空间爆炸问题，提出规范引导的路径捷径化方法，聚焦马尔可夫链与ω-正则属性，经Storm基准评估，该方法在复杂规范实例上性能优于基准。
AI 中文摘要
鉴于许多嵌入式系统具有安全关键性质，其安全保障至关重要。由于此类系统通常是随机的，概率模型检测成为一项尤为重要的技术。然而，存在一个众所周知的可扩展性问题，即状态空间爆炸，尤其在验证复杂属性时更为突出。为缓解该问题，我们针对概率系统提出了规范引导的路径捷径化方法，聚焦于马尔可夫链（MCs）与ω-正则属性。核心思路是：当待验证属性固定时，马尔可夫链中的某些转移序列可替换为单个转移，且不会改变满足概率，从而可缩减马尔可夫链的状态空间。我们实现了所提出的路径捷径化方法，并以Storm作为基准模型检测器，评估其对概率模型检测性能的贡献。结果表明，我们的方法通常优于基准方法，尤其在具有复杂规范的基准实例上表现突出。
英文摘要
Given the safety-critical nature of many embedded systems, their safety assurance is essential. Because such systems are typically stochastic, probabilistic model checking is a particularly important technique. However, there is a well-known scalability issue due to state-space explosion, especially when verifying complex properties. To mitigate this issue, we propose specification-guided path shortcutting for probabilistic systems, focusing on Markov chains (MCs) and $ω$-regular properties. The key idea is that, when the verified property is fixed, certain sequences of transitions in an MC can be replaced with a single transition without changing the satisfaction probability, and thus, we can reduce the state space of the MC. We implement the proposed path shortcutting and evaluate its contribution to the performance of probabilistic model checking, using Storm as the baseline model checker. The results suggest that our approach often outperforms the baseline, particularly on benchmark instances with complex specifications.
CommentsTo Appear in EMSOFT2026
