Group colloquium: QComp 2019: The First Friendly Competition of Tools for the Analysis of Quantitative Formal Models

When: March 21, 2019, 15:45-16:30

Where: Ravelijn 2503

Who: Arnd Hartmanns

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 was the first friendly competition among such tools. It focused on stochastic models from Markov chains to probabilistic timed automata specified in the JANI model exchange format, and on simple probabilistic reachability, expected-reward and steady-state properties. QComp drew its benchmarks from the new Quantitative Verification Benchmark Set. Participating tools, which include probabilistic model checkers and planners as well as simulation-based tools, were evaluated in terms of performance, versatility, and usability. In this talk, I will 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.