STMC: Statistical Model Checker with Stratified and Antithetic Sampling
STMC: Statistical Model Checker with Stratified and Antithetic Sampling
复制标题
DOI：
10.1007/978-3-030-53291-8_23
复制
发表时间：
2020-06-16
期刊：
影响因子：
--
通讯作者：
Viswanathan M
中科院分区：
文献类型：
--
作者：
Roohi N;Wang Y;West M;Dullerud GE;Viswanathan M
是一个统计模型检查器，它使用对偶和分层抽样技术来减少样本数量，从而减少决策所需的时间。该工具能够统计验证任何黑盒概率系统，可以模拟，对任何属性的概率界限，可以评估系统的各个执行。我们已经评估了我们的工具在许多例子，并比较它与符号和统计算法。当层数较多时，我们的算法平均减少了3倍以上的样本数。此外，作为一个统计模型检查器，能够验证远远超出当前符号模型检查器范围的模型。在大型系统（多达州）上，能够检查100%的基准系统，而中现有的符号方法仅在13%的系统上成功。该工具、安装说明、基准测试和运行基准测试的脚本都可以作为开源在线获得。
is a statistical model checker that uses antithetic and stratified sampling techniques to reduce the number of samples and, hence, the amount of time required before making a decision. The tool is capable of statistically verifying any black-box probabilistic system that can simulate, against probabilistic bounds on any property that can evaluate over individual executions of the system. We have evaluated our tool on many examples and compared it with both symbolic and statistical algorithms. When the number of strata is large, our algorithms reduced the number of samples more than 3 times on average. Furthermore, being a statistical model checker makes able to verify models that are well beyond the reach of current symbolic model checkers. On large systems (up to states) was able to check 100% of benchmark systems, compared to existing symbolic methods in , which only succeeded on 13% of systems. The tool, installation instructions, benchmarks, and scripts for running the benchmarks are all available online as open source.
登录
查看更多内容
影响因子：
0.9
作者：
Agha, Gul;Palmskog, Karl
通讯作者：
Palmskog, Karl
影响因子：
0.8
作者：
Wang, Yu;Roohi, Nima;Dullerud, Geir E.
通讯作者：
Dullerud, Geir E.
影响因子：
--
作者：
WALD, A
通讯作者：
WALD, A
DOI：
10.1109/tcad.2005.852033
发表时间：
2005-10-01
影响因子：
2.9
作者：
Norman, G;Parker, D;Shukla, S
通讯作者：
Shukla, S
影响因子：
4.5
作者：
Fan, JQ;Zhang, CM;Zhang, J
通讯作者：
Zhang, J