Tools and Algorithms for Sound Multi-Objective Probabilistic Model Checking (Long Tool Paper)

Practical verification tasks often involve multiple goals, such as maximising an expected reward within a specified reliability threshold. Algorithms to solve such multi-objective probabilistic model checking (MO-PMC) problems were developed over a decade ago, and are implemented by multiple tools. However, the algorithms are unsound in general—at best delivering some underapproximation of the true result—and the implementations are unreliable, with different tools producing inconsistent results. In this paper, we present the first implementations of recently-developed sound MO-PMC algorithms that bound the true result from above and below, in two independent tools. We discuss ways to consistently treat infinite rewards and extend the algorithms with relative-error termination criteria. On the practical side, we add support for multi-objective properties to the Jani interchange format for tool interoperability, and extend the Quantitative Verification Benchmark Set with multi-objective problems. Based on the latter, we conduct an extensive experimental evaluation of the two tools’ new sound MOPMC capabilities, showing in particular that they produce consistent results.