论文标题
概率模型检查器风暴
The Probabilistic Model Checker Storm
论文作者
论文摘要
我们介绍概率模型检查器风暴。 Storm支持Markov连锁店和Markov决策过程的离散和连续时间变体的分析。 Storm具有三个主要的区别特征。它支持Markov模型的多种输入语言，包括Jani和Prism建模语言，动态故障树，广义的随机培养皿网和概率的守护命令语言。它具有模块化设置，可以轻松交换求解器和符号发动机。它的Python API允许通过封装Storm的快速可扩展算法来快速进行原型。本文报告了Storm的主要特征，并解释了如何有效使用它们。描述了风暴的主要区别功能。最后，提出了对QCOMP 2019基准集中风暴不同配置的经验评估。
We present the probabilistic model checker Storm. Storm supports the analysis of discrete- and continuous-time variants of both Markov chains and Markov decision processes. Storm has three major distinguishing features. It supports multiple input languages for Markov models, including the JANI and PRISM modeling languages, dynamic fault trees, generalized stochastic Petri nets, and the probabilistic guarded command language. It has a modular set-up in which solvers and symbolic engines can easily be exchanged. Its Python API allows for rapid prototyping by encapsulating Storm's fast and scalable algorithms. This paper reports on the main features of Storm and explains how to effectively use them. A description is provided of the main distinguishing functionalities of Storm. Finally, an empirical evaluation of different configurations of Storm on the QComp 2019 benchmark set is presented.
