Probabilistic model checking computes probabilities and expected values related to designated behaviours of interest in Markov models. As a formal verification approach, it is applied to critical systems; thus we trust that probabilistic model checkers deliver correct results. To achieve scalability and performance, however, these tools use finite-precision floating-point numbers to represent and calculate probabilities and other values. As a consequence, their results are affected by rounding errors that may accumulate and interact in hard-to-predict ways. In this paper, we show how to implement fast and correct probabilistic model checking by exploiting the ability of current hardware to control the direction of rounding in floating-point calculations. We outline the complications in achieving correct rounding from higher-level programming languages, describe our implementation as part of the Modest Toolset's 'mcsta' model checker, and exemplify the tradeoffs between performance and correctness in an extensive experimental evaluation across different operating systems and CPU architectures.


翻译:概率模型检查计算了与Markov模型中指定感兴趣的行为相关的概率和预期值。 作为一种正式的核查方法,它适用于关键系统; 因此,我们相信概率模型检查器能够产生正确的结果。 然而,为了实现可缩放性和性,这些工具使用有限精度浮点数来表示和计算概率和其他值。 因此,它们的结果会受到可能以难以预测的方式累积和互动的四舍五入错误的影响。 在本文中,我们展示了如何通过利用当前硬件的能力来控制浮动点计算四舍五入方向来实施快速和正确的概率模型检查。 我们概述了从更高层次的编程语言中正确四舍五入的复杂情况,描述我们作为“ Modest Toolet” 的“mcsta” 模型检查器的一部分的执行情况,并举例说明在不同操作系统和CPU结构的广泛实验性评估中业绩与正确性之间的权衡。

0
下载
关闭预览

相关内容

ACM/IEEE第23届模型驱动工程语言和系统国际会议,是模型驱动软件和系统工程的首要会议系列,由ACM-SIGSOFT和IEEE-TCSE支持组织。自1998年以来,模型涵盖了建模的各个方面,从语言和方法到工具和应用程序。模特的参加者来自不同的背景,包括研究人员、学者、工程师和工业专业人士。MODELS 2019是一个论坛,参与者可以围绕建模和模型驱动的软件和系统交流前沿研究成果和创新实践经验。今年的版本将为建模社区提供进一步推进建模基础的机会,并在网络物理系统、嵌入式系统、社会技术系统、云计算、大数据、机器学习、安全、开源等新兴领域提出建模的创新应用以及可持续性。 官网链接:http://www.modelsconference.org/
专知会员服务
28+阅读 · 2021年8月2日
专知会员服务
38+阅读 · 2020年9月6日
耶鲁大学《分布式系统理论》笔记,491页pdf
专知会员服务
44+阅读 · 2020年7月29日
专知会员服务
61+阅读 · 2020年3月4日
【新书】Python编程基础,669页pdf
专知会员服务
186+阅读 · 2019年10月10日
Hierarchically Structured Meta-learning
CreateAMind
23+阅读 · 2019年5月22日
Unsupervised Learning via Meta-Learning
CreateAMind
41+阅读 · 2019年1月3日
spinningup.openai 强化学习资源完整
CreateAMind
6+阅读 · 2018年12月17日
【NIPS2018】接收论文列表
专知
5+阅读 · 2018年9月10日
条件GAN重大改进!cGANs with Projection Discriminator
CreateAMind
8+阅读 · 2018年2月7日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
【推荐】RNN/LSTM时序预测
机器学习研究会
25+阅读 · 2017年9月8日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
强化学习族谱
CreateAMind
26+阅读 · 2017年8月2日
强化学习 cartpole_a3c
CreateAMind
9+阅读 · 2017年7月21日
Arxiv
0+阅读 · 2021年12月13日
Arxiv
6+阅读 · 2017年7月17日
VIP会员
相关资讯
Hierarchically Structured Meta-learning
CreateAMind
23+阅读 · 2019年5月22日
Unsupervised Learning via Meta-Learning
CreateAMind
41+阅读 · 2019年1月3日
spinningup.openai 强化学习资源完整
CreateAMind
6+阅读 · 2018年12月17日
【NIPS2018】接收论文列表
专知
5+阅读 · 2018年9月10日
条件GAN重大改进!cGANs with Projection Discriminator
CreateAMind
8+阅读 · 2018年2月7日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
【推荐】RNN/LSTM时序预测
机器学习研究会
25+阅读 · 2017年9月8日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
强化学习族谱
CreateAMind
26+阅读 · 2017年8月2日
强化学习 cartpole_a3c
CreateAMind
9+阅读 · 2017年7月21日
Top
微信扫码咨询专知VIP会员