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.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