Publication Details
Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report
Andriushchenko Roman, Ing. (DITS)
ARND, H.
JUNGES, S.
KŘETÍNSKÝ, J.
Quantitative verification, Markov chains, Markov decision processes, Timed
automata.
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.
@inproceedings{BUT196667,
author="ČEŠKA, M. and ANDRIUSHCHENKO, R. and ARND, H. and JUNGES, S. and KŘETÍNSKÝ, J.",
title="Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report",
booktitle="International TOOLympics Challenge",
year="2024",
series="Lecture Notes in Computer Science",
pages="90--146",
publisher="Springer Nature Switzerland AG",
address="Cham",
doi="10.1007/978-3-031-67695-6\{_}4",
isbn="978-3-031-67694-9"
}