On correctness, precision, and performance in quantitative verification: QComp 2020 Competition Report
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...
| Main Authors: | , , , , , , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Springer
2021
|
| _version_ | 1826308534499803136 |
|---|---|
| author | Budde, CE Hartmanns, A Klauck, M Křetínský, J Parker, D Quatmann, T Turrini, A Zhang, Z |
| author_facet | Budde, CE Hartmanns, A Klauck, M Křetínský, J Parker, D Quatmann, T Turrini, A Zhang, Z |
| author_sort | Budde, CE |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T07:20:54Z |
| format | Conference item |
| id | oxford-uuid:1cec3ee2-a20f-4d00-b696-85a79e97ec75 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T07:20:54Z |
| publishDate | 2021 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:1cec3ee2-a20f-4d00-b696-85a79e97ec752022-10-13T14:54:25ZOn correctness, precision, and performance in quantitative verification: QComp 2020 Competition ReportConference itemhttp://purl.org/coar/resource_type/c_5794uuid:1cec3ee2-a20f-4d00-b696-85a79e97ec75EnglishSymplectic ElementsSpringer2021Budde, CEHartmanns, AKlauck, MKřetínský, JParker, DQuatmann, TTurrini, AZhang, ZQuantitative 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. |
| spellingShingle | Budde, CE Hartmanns, A Klauck, M Křetínský, J Parker, D Quatmann, T Turrini, A Zhang, Z On correctness, precision, and performance in quantitative verification: QComp 2020 Competition Report |
| title | On correctness, precision, and performance in quantitative verification: QComp 2020 Competition Report |
| title_full | On correctness, precision, and performance in quantitative verification: QComp 2020 Competition Report |
| title_fullStr | On correctness, precision, and performance in quantitative verification: QComp 2020 Competition Report |
| title_full_unstemmed | On correctness, precision, and performance in quantitative verification: QComp 2020 Competition Report |
| title_short | On correctness, precision, and performance in quantitative verification: QComp 2020 Competition Report |
| title_sort | on correctness precision and performance in quantitative verification qcomp 2020 competition report |
| work_keys_str_mv | AT buddece oncorrectnessprecisionandperformanceinquantitativeverificationqcomp2020competitionreport AT hartmannsa oncorrectnessprecisionandperformanceinquantitativeverificationqcomp2020competitionreport AT klauckm oncorrectnessprecisionandperformanceinquantitativeverificationqcomp2020competitionreport AT kretinskyj oncorrectnessprecisionandperformanceinquantitativeverificationqcomp2020competitionreport AT parkerd oncorrectnessprecisionandperformanceinquantitativeverificationqcomp2020competitionreport AT quatmannt oncorrectnessprecisionandperformanceinquantitativeverificationqcomp2020competitionreport AT turrinia oncorrectnessprecisionandperformanceinquantitativeverificationqcomp2020competitionreport AT zhangz oncorrectnessprecisionandperformanceinquantitativeverificationqcomp2020competitionreport |