On Correctness, Precision, and Performance in Quantitative Verification -- QComp 2020 Competition Report
On Correctness, Precision, and Performance in Quantitative Verification -- QComp 2020 Competition Report
复制标题
论定量验证的正确性、精确性和性能——QComp 2020竞赛报告
DOI：
10.1007/978-3-030-83723-5_15
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Zhang, Zhen
中科院分区：
文献类型：
--
作者：
Budde, Carlos E;Hartmanns, Arnd;Klauck, Michaela;Kretinsky, Jan;Parker, David;Quatmann, Tim;Turrini, Andrea;Zhang, Zhen
定量验证工具为随机和定时系统的正式模型计算概率、预期回报或稳态值。通常无法有效地获得精确的结果，因此大多数工具在迭代算法中使用浮点运算来近似感兴趣的数量。因此，正确性由所需的精度定义，并决定性能。在本文中，我们报告了在QComp 2020中进行的这些权衡的实验评估：第二次定量形式模型分析工具的友好竞争。我们调查的精度范围从确切的理性结果，统计置信度的声明，提供的九个参与工具。他们产生了一个性能评估，使用五个轨道不同的正确性标准，其中我们提出的结果。
Quantitative verification tools compute probabilities, expected rewards, or steady-state values for formal models of stochastic and timed systems. Exact results often cannot be obtained efficiently, so most tools use floating-point arithmetic in iterative algorithms that approximate the quantity of interest. Correctness is thus defined by the desired precision and determines performance. In this paper, we report on the experimental evaluation of these trade-offs performed in QComp 2020: the second friendly competition of tools for the analysis of quantitative formal models. We survey the precision guarantees—ranging from exact rational results to statistical confidence statements—offered by the nine participating tools. They gave rise to a performance evaluation using five tracks with varying correctness criteria, of which we present the results.