STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis
STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis
复制标题
DOI：
10.1007/978-3-030-25540-4_31
复制
发表时间：
2019-06
期刊：
影响因子：
--
通讯作者：
Thakur Neupane;C. Myers;C. Madsen;Hao Zheng;Zhen Zhang
中科院分区：
文献类型：
--
作者：
Thakur Neupane;C. Myers;C. Madsen;Hao Zheng;Zhen Zhang
随机模型检验是一种分析具有概率特征的系统的技术。然而，它的可伸缩性受到限制，因为实际应用程序的概率模型通常具有非常大或无限的状态空间。本文提出了一种新的无限状态CTMC模型检查器——STAMINA，它具有改进的可扩展性。它使用一种新的状态空间逼近方法，将大的、可能是无限状态的CTMC模型简化为有限状态表示，这些表示适用于现有的随机模型检查器。它集成了一种新的属性引导状态扩展方法，提高了分析精度。该工具在几个基准示例上的演示显示，与部署类似近似方法的最先进的CTMC模型检查器相比，该工具在分析效率和准确性方面取得了令人满意的结果。
Stochastic model checking is a technique for analyzing systems that possess probabilistic characteristics. However, its scalability is limited as probabilistic models of real-world applications typically have very large or infinite state space. This paper presents a new infinite state CTMC model checker, STAMINA, with improved scalability. It uses a novel state space approximation method to reduce large and possibly infinite state CTMC models to finite state representations that are amenable to existing stochastic model checkers. It is integrated with a new property-guided state expansion approach that improves the analysis accuracy. Demonstration of the tool on several benchmark examples shows promising results in terms of analysis efficiency and accuracy compared with a state-of-the-art CTMC model checker that deploys a similar approximation method.