Correct Probabilistic Model Checking with Floating-Point Arithmetic

Arnd Hartmanns

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)
5 Downloads (Pure)


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.

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part II
EditorsDana Fisman, Grigore Rosu
PublisherSpringer Nature
Number of pages19
ISBN (Electronic)978-3-030-99527-0
ISBN (Print)978-3-030-99526-3
Publication statusPublished - 2022
Event28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022 - Munich , Germany
Duration: 2 Apr 20227 Apr 2022
Conference number: 28

Publication series

NameLecture Notes in Computer Science


Conference28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022
Abbreviated titleTACAS 2022


  • This work was part of the MISSION (Models in Space Systems: Integration, Operation, and Networking) project, funded by the European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie Actions grant number 101008233.

Cite this