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

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.1007/978-3-031-67695-6_4

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

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 TaylorMatthias Volk, Maximilian Weininger, Zhen Zhang

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

1 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
Title of host publication	TOOLympics Challenge 2023
Subtitle of host publication	Updates, Results, Successes of the Formal-Methods Competitions
Editors	Dirk Beyer, Arnd Hartmanns, Fabrice Kordon
Place of Publication	Cham, Switzerland
Publisher	Springer
Pages	90-146
Number of pages	57
ISBN (Electronic)	978-3-031-67695-6
ISBN (Print)	978-3-031-67694-9
DOIs	https://doi.org/10.1007/978-3-031-67695-6_4
Publication status	Published - 2025
Event	3rd International TOOLympics Challenge, TOOLympics 2023 - Paris, France Duration: 22 Apr 2023 → 27 Apr 2023 Conference number: 3

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	14550
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	3rd International TOOLympics Challenge, TOOLympics 2023
Abbreviated title	TOOLympics 2023
Country/Territory	France
City	Paris
Period	22/04/23 → 27/04/23
Other	Part of the 26th European Joint Conferences on Theory and Practice of Software, ETAPS 2023

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.
2025 OA procedure

Access to Document

10.1007/978-3-031-67695-6_4

978-3-031-67695-6_4Final published version, 985 KBLicence: Taverne

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. (2025). Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. In D. Beyer, A. Hartmanns, & F. Kordon (Eds.), TOOLympics Challenge 2023: Updates, Results, Successes of the Formal-Methods Competitions (pp. 90-146). (Lecture Notes in Computer Science; Vol. 14550). Springer. https://doi.org/10.1007/978-3-031-67695-6_4

Andriushchenko, Roman ; Bork, Alexander ; Budde, Carlos E. et al. / Tools at the Frontiers of Quantitative Verification : QComp 2023 Competition Report. TOOLympics Challenge 2023: Updates, Results, Successes of the Formal-Methods Competitions. editor / Dirk Beyer ; Arnd Hartmanns ; Fabrice Kordon. Cham, Switzerland : Springer, 2025. pp. 90-146 (Lecture Notes in Computer Science).

@inproceedings{8ba42a6b1663414fbea86316ad0811f9,

title = "Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report",

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{\textquoteright}s active areas and tomorrow{\textquoteright}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., 2025 OA procedure",

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",

note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.; 3rd International TOOLympics Challenge, TOOLympics 2023, TOOLympics 2023 ; Conference date: 22-04-2023 Through 27-04-2023",

year = "2025",

doi = "10.1007/978-3-031-67695-6_4",

language = "English",

isbn = "978-3-031-67694-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "90--146",

editor = "Dirk Beyer and Arnd Hartmanns and Fabrice Kordon",

booktitle = "TOOLympics Challenge 2023",

address = "Germany",

}

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 2025, Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. in D Beyer, A Hartmanns & F Kordon (eds), TOOLympics Challenge 2023: Updates, Results, Successes of the Formal-Methods Competitions. Lecture Notes in Computer Science, vol. 14550, Springer, Cham, Switzerland, pp. 90-146, 3rd International TOOLympics Challenge, TOOLympics 2023, Paris, France, 22/04/23. https://doi.org/10.1007/978-3-031-67695-6_4

Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. / Andriushchenko, Roman; Bork, Alexander; Budde, Carlos E. et al.
TOOLympics Challenge 2023: Updates, Results, Successes of the Formal-Methods Competitions. ed. / Dirk Beyer; Arnd Hartmanns; Fabrice Kordon. Cham, Switzerland: Springer, 2025. p. 90-146 (Lecture Notes in Computer Science; Vol. 14550).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Tools at the Frontiers of Quantitative Verification

T2 - 3rd International TOOLympics Challenge, TOOLympics 2023

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

N1 - Conference code: 3

PY - 2025

Y1 - 2025

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 - 2025 OA procedure

UR - http://www.scopus.com/inward/record.url?scp=85209935115&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-67695-6_4

DO - 10.1007/978-3-031-67695-6_4

M3 - Conference contribution

AN - SCOPUS:85209935115

SN - 978-3-031-67694-9

T3 - Lecture Notes in Computer Science

SP - 90

EP - 146

BT - TOOLympics Challenge 2023

A2 - Beyer, Dirk

A2 - Hartmanns, Arnd

A2 - Kordon, Fabrice

PB - Springer

CY - Cham, Switzerland

Y2 - 22 April 2023 through 27 April 2023

ER -

Andriushchenko R, Bork A, Budde CE, Češka M, Grover K, Hahn EM et al. Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. In Beyer D, Hartmanns A, Kordon F, editors, TOOLympics Challenge 2023: Updates, Results, Successes of the Formal-Methods Competitions. Cham, Switzerland: Springer. 2025. p. 90-146. (Lecture Notes in Computer Science). Epub 2024 Nov 1. doi: 10.1007/978-3-031-67695-6_4