概率模型检测器 Storm
软件工程
2020-10-08 v2
摘要
我们介绍概率模型检测器 Storm。Storm 支持对马尔可夫链与马尔可夫决策过程的离散时间和连续时间变体进行分析。Storm 具有三大显著特征：它支持多种马尔可夫模型输入语言，包括 JANI 与 PRISM 建模语言、动态故障树、广义随机 Petri 网以及概率守护命令语言；它具有模块化架构，其中求解器与符号引擎可轻松替换；其 Python API 通过封装 Storm 快速且可扩展的算法，支持快速原型开发。本文报道 Storm 的主要特性并说明如何有效使用。描述了 Storm 的主要区分性功能。最后，给出了 Storm 不同配置在 QComp 2019 基准集上的实证评估。
引用
@article{arxiv.2002.07080,
title = {The Probabilistic Model Checker Storm},
author = {Christian Hensel and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann and Matthias Volk},
journal= {arXiv preprint arXiv:2002.07080},
year = {2020}
}