Quantitative Verification Benchmark Set

The Quantitative Verification Benchmark Set is a collection of probabilistic models – Markov models, fault trees, stochastic Petri nets and others – to serve as a benchmark set for the benefit of algorithm and tool developers as well as the foundation of QComp.

Available Materials

The benchmark set comprises benchmark models, properties for verification, and tool results.

Models

The benchmark set's models are

• formal: they have an unambiguous, mathematically defined semantics in terms of discrete- or continuous-time Markov chains (DTMC or CTMC), Markov decision processes (MDP), Markov automata (MA) or probabilistic timed automata (PTA);
• portable: they are provided both in their original modelling language – e.g. the PRISM language or Modest – as well as the JANI exchange format for model exchange between tools (and we keep a list of JANI converters);
• scalable: most models are parameterised, allowing their underlying state spaces to be scaled from a few hundred to billions of states;
• diverse: the repository includes models from different areas – such as probabilistic model checking, dependability evaluation, and probabilistic planning – that were built for very different analysis approaches and tools; and
• open: all models and data are open-access and may be used subject to the terms of the CC-BY 4.0 license.

Properties

Every model is accompanied by a set of properties: queries for quantities of interest to be computed by analysis tools. The benchmark set collects models with queries for unbounded and bounded reachability probabilities, for unbounded and bounded variants of various forms of expected accumulated rewards, and for steady-state values.

Results

Alongside its various models, the repository also provides tool results: property values and performance data obtained by applying different tools to the models across different hardware configurations.

Reproducibility

Throughout, all data necessary for reproducibility is available, for example the command lines used to convert the models from their original modelling language into JANI or the precise hardware and runtime configuration that a set of results was obtained in.

Openness

The benchmark set is hosted on GitHub and accepts contributions.