Tools at the Frontiers of Quantitative Verification

Roman Andriushchenko; Alexander Bork; Carlos E. Budde; Milan Češka; Kush Grover; Ernst Moritz Hahn; Arnd Hartmanns; Bryant Israelsen; Nils Jansen; Joshua Jeppson; Sebastian Junges; Maximilian A. Köhl; Bettina Könighofer; Jan Křetínský; Tobias Meggendorfer; David Parker; Stefan Pranger; Tim Quatmann; Enno Ruijters; Landon Taylor; Matthias Volk; Maximilian Weininger; Zhen Zhang

doi:10.48550/arXiv.2405.13583

Tools at the Frontiers of Quantitative Verification

Roman Andriushchenko
, Alexander Bork
, Carlos E. Budde
, Milan Češka
, Kush Grover
, Ernst Moritz Hahn
, Arnd Hartmanns^*
, Bryant Israelsen
, Nils Jansen
, Joshua Jeppson
, Sebastian Junges
, Maximilian A. Köhl
, Bettina Könighofer
, Jan Křetínský
, Tobias Meggendorfer
, David Parker
, Stefan Pranger
, Tim Quatmann
, Enno Ruijters
, Landon Taylor

Matthias Volk, Maximilian Weininger, Zhen Zhang

^*Corresponding author for this work

Research output: Working paper › Preprint › Academic

24 Downloads (Pure)

Abstract

The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today's active areas and tomorrow's challenges in tool-focused research for quantitative verification.

Original language	English
Publisher	ArXiv.org
Number of pages	59
DOIs	https://doi.org/10.48550/arXiv.2405.13583
Publication status	Published - 22 May 2024

Keywords

This work was part of the MISSION (Models in Space Systems: Integration, Operation, and Networking) project, funded by the European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie Actions grant number 101008233.
cs.LO

Access to Document

10.48550/arXiv.2405.13583Licence: CC BY

2405.13583v1Final published version, 1.38 MBLicence: CC BY

1 Conference contribution

Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report
Andriushchenko, R., Bork, A., Budde, C. E., Češka, M., Grover, K., Hahn, E. M., Hartmanns, A., Israelsen, B., Jansen, N., Jeppson, J., Junges, S., Köhl, M. A., Könighofer, B., Křetínský, J., Meggendorfer, T., Parker, D., Pranger, S., Quatmann, T., Ruijters, E. & Taylor, L. & 3 others, Volk, M., Weininger, M. & Zhang, Z., 1 Nov 2024, TOOLympics Challenge 2023: Updates, Results, Successes of the Formal-Methods Competitions. Beyer, D., Hartmanns, A. & Kordon, F. (eds.). Cham, Switzerland: Springer, p. 90-146 57 p. (Lecture Notes in Computer Science; vol. 14550).
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

Open Access
File
2 Link opens in a new tab Citations (Scopus)

20 Downloads (Pure)

Cite this

Andriushchenko, R., Bork, A., Budde, C. E., Češka, M., Grover, K., Hahn, E. M., Hartmanns, A., Israelsen, B., Jansen, N., Jeppson, J., Junges, S., Köhl, M. A., Könighofer, B., Křetínský, J., Meggendorfer, T., Parker, D., Pranger, S., Quatmann, T., Ruijters, E., ... Zhang, Z. (2024). Tools at the Frontiers of Quantitative Verification. ArXiv.org. https://doi.org/10.48550/arXiv.2405.13583

@techreport{22345eceb36f43e4929c5c39a00040fe,

title = "Tools at the Frontiers of Quantitative Verification",

abstract = " The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today's active areas and tomorrow's challenges in tool-focused research for quantitative verification. ",

keywords = "This work was part of the MISSION (Models in Space Systems: Integration, Operation, and Networking) project, funded by the European Union{\textquoteright}s Horizon 2020 research and innovation programme under Marie Sk{\l}odowska-Curie Actions grant number 101008233., cs.LO",

author = "Roman Andriushchenko and Alexander Bork and Budde, \{Carlos E.\} and Milan {\v C}e{\v s}ka and Kush Grover and Hahn, \{Ernst Moritz\} and Arnd Hartmanns and Bryant Israelsen and Nils Jansen and Joshua Jeppson and Sebastian Junges and K{\"o}hl, \{Maximilian A.\} and Bettina K{\"o}nighofer and Jan K{\v r}et{\'i}nsk{\'y} and Tobias Meggendorfer and David Parker and Stefan Pranger and Tim Quatmann and Enno Ruijters and Landon Taylor and Matthias Volk and Maximilian Weininger and Zhen Zhang",

year = "2024",

month = may,

day = "22",

doi = "10.48550/arXiv.2405.13583",

language = "English",

publisher = "ArXiv.org",

type = "WorkingPaper",

institution = "ArXiv.org",

}

Andriushchenko, R, Bork, A, Budde, CE, Češka, M, Grover, K, Hahn, EM, Hartmanns, A, Israelsen, B, Jansen, N, Jeppson, J, Junges, S, Köhl, MA, Könighofer, B, Křetínský, J, Meggendorfer, T, Parker, D, Pranger, S, Quatmann, T, Ruijters, E, Taylor, L, Volk, M, Weininger, M & Zhang, Z 2024 'Tools at the Frontiers of Quantitative Verification' ArXiv.org. https://doi.org/10.48550/arXiv.2405.13583

TY - UNPB

T1 - Tools at the Frontiers of Quantitative Verification

AU - Andriushchenko, Roman

AU - Bork, Alexander

AU - Budde, Carlos E.

AU - Češka, Milan

AU - Grover, Kush

AU - Hahn, Ernst Moritz

AU - Hartmanns, Arnd

AU - Israelsen, Bryant

AU - Jansen, Nils

AU - Jeppson, Joshua

AU - Junges, Sebastian

AU - Köhl, Maximilian A.

AU - Könighofer, Bettina

AU - Křetínský, Jan

AU - Meggendorfer, Tobias

AU - Parker, David

AU - Pranger, Stefan

AU - Quatmann, Tim

AU - Ruijters, Enno

AU - Taylor, Landon

AU - Volk, Matthias

AU - Weininger, Maximilian

AU - Zhang, Zhen

PY - 2024/5/22

Y1 - 2024/5/22

N2 - The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today's active areas and tomorrow's challenges in tool-focused research for quantitative verification.

AB - The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today's active areas and tomorrow's challenges in tool-focused research for quantitative verification.

KW - This work was part of the MISSION (Models in Space Systems: Integration, Operation, and Networking) project, funded by the European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie Actions grant number 101008233.

KW - cs.LO

U2 - 10.48550/arXiv.2405.13583

DO - 10.48550/arXiv.2405.13583

M3 - Preprint

BT - Tools at the Frontiers of Quantitative Verification

PB - ArXiv.org

ER -

Tools at the Frontiers of Quantitative Verification

Abstract

Keywords

Access to Document

Fingerprint

Research output

Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report

Cite this