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.

On Correctness, Precision, and Performance in Quantitative Verification / Budde, Carlos E.; Hartmanns, Arnd; Klauck, Michaela; Křetínský, Jan; Parker, David; Quatmann, Tim; Turrini, Andrea; Zhang, Zhen. - ELETTRONICO. - 12479:(2021), pp. 216-241. (Intervento presentato al convegno 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020 tenutosi a Rhodes, Greece nel 20–30 October 2020) [10.1007/978-3-030-83723-5_15].

On Correctness, Precision, and Performance in Quantitative Verification

Carlos E. Budde;
2021-01-01

Abstract

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.
2021
Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020
Germany
Springer-Verlag GMBH
978-3-030-83722-8
978-3-030-83723-5
Budde, Carlos E.; Hartmanns, Arnd; Klauck, Michaela; Křetínský, Jan; Parker, David; Quatmann, Tim; Turrini, Andrea; Zhang, Zhen
On Correctness, Precision, and Performance in Quantitative Verification / Budde, Carlos E.; Hartmanns, Arnd; Klauck, Michaela; Křetínský, Jan; Parker, David; Quatmann, Tim; Turrini, Andrea; Zhang, Zhen. - ELETTRONICO. - 12479:(2021), pp. 216-241. (Intervento presentato al convegno 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020 tenutosi a Rhodes, Greece nel 20–30 October 2020) [10.1007/978-3-030-83723-5_15].
File in questo prodotto:
File Dimensione Formato  
QComp_2020_Competition_Report.pdf

accesso aperto

Descrizione: Article camera-ready
Tipologia: Post-print referato (Refereed author’s manuscript)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 678.89 kB
Formato Adobe PDF
678.89 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/314749
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? ND
social impact