TY - GEN
T1 - The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models
T2 - 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019
AU - Hahn, Ernst Moritz
AU - Hartmanns, Arnd
AU - Hensel, Christian
AU - Klauck, Michaela
AU - Klein, Joachim
AU - Křetínský, Jan
AU - Parker, David
AU - Quatmann, Tim
AU - Ruijters, Enno
AU - Steinmetz, Marcel
N1 - Publisher Copyright:
© 2019, The Author(s).
PY - 2019
Y1 - 2019
N2 - Quantitative formal models capture probabilistic behaviour, real-time aspects, or general continuous dynamics. A number of tools support their automatic analysis with respect to dependability or performance properties. QComp 2019 is the first, friendly competition among such tools. It focuses on stochastic formalisms from Markov chains to probabilistic timed automata specified in the Jani model exchange format, and on probabilistic reachability, expected-reward, and steady-state properties. QComp draws its benchmarks from the new Quantitative Verification Benchmark Set. Participating tools, which include probabilistic model checkers and planners as well as simulation-based tools, are evaluated in terms of performance, versatility, and usability. In this paper, we report on the challenges in setting up a quantitative verification competition, present the results of QComp 2019, summarise the lessons learned, and provide an outlook on the features of the next edition of QComp.
AB - Quantitative formal models capture probabilistic behaviour, real-time aspects, or general continuous dynamics. A number of tools support their automatic analysis with respect to dependability or performance properties. QComp 2019 is the first, friendly competition among such tools. It focuses on stochastic formalisms from Markov chains to probabilistic timed automata specified in the Jani model exchange format, and on probabilistic reachability, expected-reward, and steady-state properties. QComp draws its benchmarks from the new Quantitative Verification Benchmark Set. Participating tools, which include probabilistic model checkers and planners as well as simulation-based tools, are evaluated in terms of performance, versatility, and usability. In this paper, we report on the challenges in setting up a quantitative verification competition, present the results of QComp 2019, summarise the lessons learned, and provide an outlook on the features of the next edition of QComp.
UR - http://www.scopus.com/inward/record.url?scp=85064915499&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-17502-3_5
DO - 10.1007/978-3-030-17502-3_5
M3 - Conference contribution
AN - SCOPUS:85064915499
SN - 9783030175016
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 69
EP - 92
BT - Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS
A2 - Steffen, Bernhard
A2 - Huisman, Marieke
A2 - Kordon, Fabrice
A2 - Beyer, Dirk
PB - Springer Verlag
Y2 - 6 April 2019 through 11 April 2019
ER -