Tools and Algorithms for Sound Multi-Objective Probabilistic Model Checking

Lecture notes in computer science, pp. 189–210

Abstract

Abstract 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 MO-PMC capabilities, showing in particular that they produce consistent results.

Authors 3

1. Arnd Hartmanns

   University of Twente

   Affiliation as printed

   University of Twente, Enschede, The Netherlands

2. Tim Quatmann Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

3. Mark van Wijk corresponding

   University of Twente

   Affiliation as printed

   University of Twente, Enschede, The Netherlands