Correct Probabilistic Model Checking with Floating-Point Arithmetic

TL;DR

This paper presents a method to ensure correct probabilistic model checking by controlling floating-point rounding, improving accuracy without sacrificing performance, and demonstrates its implementation in the Modest Toolset's 'mcsta' model checker.

Contribution

It introduces a technique to achieve fast and correct probabilistic model checking by exploiting hardware-controlled floating-point rounding, addressing a key accuracy issue in the field.

Findings

Correct rounding can be achieved using hardware features.

Implementation in 'mcsta' demonstrates practical viability.

Tradeoffs between performance and correctness are analyzed.

Abstract

Probabilistic model checking computes probabilities and expected values related to designated behaviours of interest in Markov models. As a formal verification approach, it is applied to critical systems; thus we trust that probabilistic model checkers deliver correct results. To achieve scalability and performance, however, these tools use finite-precision floating-point numbers to represent and calculate probabilities and other values. As a consequence, their results are affected by rounding errors that may accumulate and interact in hard-to-predict ways. In this paper, we show how to implement fast and correct probabilistic model checking by exploiting the ability of current hardware to control the direction of rounding in floating-point calculations. We outline the complications in achieving correct rounding from higher-level programming languages, describe our implementation as part of the Modest Toolset's 'mcsta' model checker, and exemplify the tradeoffs between performance and correctness in an extensive experimental evaluation across different operating systems and CPU architectures.