pith. sign in

arxiv: 2606.17811 · v1 · pith:EMAUO7XOnew · submitted 2026-06-16 · 💻 cs.LO

UMB: A Unified Markov Binary Format for Probabilistic Model Checking (extended version)

Roman Andriushchenko , Arnd Hartmanns , Joshua Jeppson , Sebastian Junges , Tobias Meggendorfer , David Parker , Tim Quatmann , Maximilian Weininger This is my paper

Pith reviewed 2026-06-26 22:30 UTC · model grok-4.3

classification 💻 cs.LO
keywords probabilistic model checkingbinary file formatexplicit-state modelsmodel interoperabilityMarkov modelsfile exchangePython library
0
0 comments X

The pith

A binary format built on bit-level primitives unifies representation and exchange of probabilistic systems for model checking.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces the UMB format to solve the absence of a shared low-level representation for probabilistic models. Existing tools rely on custom textual formats that create interoperability barriers and reading-writing overhead. UMB encodes a general mathematical model of probabilistic systems using a small set of bit-level primitive data structures, yielding an efficient and extensible explicit-state file format. The format ships with a Python library for model handling and validation plus cross-tool infrastructure, and has been adopted by multiple tools to support new workflows.

Core claim

UMB provides a clean, unified, and efficient explicit-state file format for representing a wide range of probabilistic systems, based on a general underlying mathematical model and encoded using a small set of bit-level primitive data structures.

What carries the argument

The UMB format, which encodes models via bit-level primitive data structures on top of a general mathematical model of probabilistic systems.

If this is right

  • Interoperability between probabilistic model checking tools increases because models can be exchanged without custom converters.
  • Overhead from writing and reading model files decreases due to the compact binary encoding.
  • New practical use cases become feasible through the supplied Python library and continuous validation infrastructure.
  • Adoption by prominent tools allows shared model repositories and cross-tool experiments.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Standard benchmarks could be distributed once in UMB rather than duplicated across tool-specific formats.
  • Future tools could be written to read UMB directly, reducing the need for high-level language parsers in some workflows.
  • The format's extensibility via bit-level primitives may support emerging model types without breaking existing readers.

Load-bearing premise

A single binary format built on bit-level primitives can represent the full range of probabilistic systems handled by existing tools without significant loss of performance or expressiveness.

What would settle it

A concrete probabilistic system from an existing tool that cannot be losslessly encoded in UMB or that produces measurably slower model-checking times after conversion to and from the format.

Figures

Figures reproduced from arXiv: 2606.17811 by Arnd Hartmanns, David Parker, Joshua Jeppson, Maximilian Weininger, Roman Andriushchenko, Sebastian Junges, Tim Quatmann, Tobias Meggendorfer.

Figure 1
Figure 1. Figure 1: An annotated transition system (left) and an MDP resulting from annotat [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Summary of our format efficiency experiments. From left to right, we [PITH_FULL_IMAGE:figures/full_fig_p010_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Summary of our format efficiency experiments for [PITH_FULL_IMAGE:figures/full_fig_p019_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Comparison of model checking time of Prism (left), mcsta (middle), and Storm (right) when using UMB vs. a high-level language. Timings in seconds. is consistently faster compared to high-level inputs across all tools, sometimes by several orders of magnitude [PITH_FULL_IMAGE:figures/full_fig_p020_4.png] view at source ↗
read the original abstract

This paper presents the unified Markov binary (UMB) format, an efficient, extensible, and well-supported explicit-state file format for representing a wide range of probabilistic systems. UMB addresses the problem that, while probabilistic model checking tools often support common high-level modelling languages, there is no effective mechanism for exchanging low-level model representations. In practice, textual, tool-specific formats are used, hampering interoperability and resulting in large overheads in writing and reading model files. UMB provides a clean, unified, and efficient solution, based on a general underlying mathematical model, and encoded using a small set of bit-level primitive data structures. The format has already been adopted by prominent tools and comes with a convenient Python library for reading, manipulating, creating, and validating models, plus infrastructure for cross-tool installation and continuous validation. We report on both the efficiency of the file format and the new practical use cases that it facilitates.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper presents the Unified Markov Binary (UMB) format, a binary explicit-state file format for a wide range of probabilistic models (DTMCs, CTMCs, MDPs, parametric). It claims to solve interoperability problems caused by tool-specific textual formats by providing an efficient, extensible representation based on a general underlying mathematical model encoded with a small set of bit-level primitive data structures. The work reports adoption by prominent tools, a supporting Python library for reading/manipulating/validating models, and infrastructure for cross-tool use, along with efficiency results and new practical use cases.

Significance. If the format achieves its claimed generality and efficiency without loss of expressiveness or performance for the full range of models, it would reduce I/O overhead in probabilistic model checking workflows and enable standardized model exchange across tools.

major comments (2)
  1. [Abstract] Abstract and evaluation sections: the central claims of efficiency, extensibility, and successful representation of the full range of probabilistic systems (including parametric and continuous-time models) are asserted without quantitative benchmarks, error measurements, file-size comparisons, or I/O timing data against existing tool-specific formats; this evidence is load-bearing for the efficiency and adoption claims.
  2. [Encoding and model mapping sections] Sections describing the bit-level encoding and mathematical model mapping: the paper does not detail how transition probabilities/rates are stored (e.g., IEEE floats vs. fixed-width rationals) or how parametric/symbolic parameters and unbounded rates are handled within the claimed small set of primitives; if additional structures are required, this undermines the 'small set' and 'no significant loss of expressiveness' assertions.
minor comments (1)
  1. The Python library and validation infrastructure are described at a high level; concrete usage examples or API signatures would improve clarity for readers intending to adopt the format.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback. We address each major comment below, indicating revisions where appropriate to strengthen the manuscript.

read point-by-point responses

  1. Referee: [Abstract] Abstract and evaluation sections: the central claims of efficiency, extensibility, and successful representation of the full range of probabilistic systems (including parametric and continuous-time models) are asserted without quantitative benchmarks, error measurements, file-size comparisons, or I/O timing data against existing tool-specific formats; this evidence is load-bearing for the efficiency and adoption claims.

    Authors: The evaluation section does report efficiency results and new use cases enabled by UMB, consistent with the abstract summary. We agree, however, that the presentation would be strengthened by additional explicit quantitative data such as direct file-size and I/O timing comparisons against tool-specific formats. We will revise the evaluation section to include these benchmarks. revision: yes

  2. Referee: [Encoding and model mapping sections] Sections describing the bit-level encoding and mathematical model mapping: the paper does not detail how transition probabilities/rates are stored (e.g., IEEE floats vs. fixed-width rationals) or how parametric/symbolic parameters and unbounded rates are handled within the claimed small set of primitives; if additional structures are required, this undermines the 'small set' and 'no significant loss of expressiveness' assertions.

    Authors: The format is built on a small set of bit-level primitives that encode the required data types for probabilities, rates, and parametric models without loss of expressiveness. We will add explicit clarification in the revised encoding and model-mapping sections describing the storage of transition probabilities/rates and the handling of parametric and continuous-time elements. revision: yes

Circularity Check

0 steps flagged

No circularity: format specification with no derivation chain

full rationale

This paper defines a binary file format (UMB) for exchanging explicit-state probabilistic models. It contains no mathematical derivations, equations, predictions, fitted parameters, or uniqueness theorems. The central claims concern design choices for bit-level primitives, extensibility, and tool adoption; these are presented as engineering decisions rather than results derived from prior self-citations or self-definitional steps. No load-bearing argument reduces to its own inputs by construction. The paper is self-contained as a specification document.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The paper introduces a data format rather than a mathematical theory; no free parameters, axioms, or invented physical entities are described in the abstract.

pith-pipeline@v0.9.1-grok · 5715 in / 1044 out tokens · 32600 ms · 2026-06-26T22:30:40.743575+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

46 extracted references · 34 canonical work pages

  1. [1]

    In: Beyer, D., Hartmanns, A., Kordon, F

    Andriushchenko, R., Bork, A., Budde, C.E., Češka, M., Hahn, E.M., Hartmanns, A., Israelsen, B., Jansen, N., Jeppson, J., Junges, S., Köhl, M.A., Könighofer, B., Křetínský, J., Meggendorfer, T., Parker, D., Pranger, S., Quatmann, T., Ruijters, E., Taylor, L., Volk, M., Weininger, M., Zhang, Z.: Tools at the frontiers of quantitative verification: QComp 202...

    work page doi:10.1007/978-3-031-67695-6_4 2023

  2. [2]

    In: Silva, A., Leino, K.R.M

    Andriushchenko, R., Ceska, M., Junges, S., Katoen, J.P., Stupinský, S.: PAYNT: A tool for inductive synthesis of probabilistic programs. In: Silva, A., Leino, K.R.M. (eds.) 33rd International Conference on Computer Aided Verification (CAV 2021). Lecture Notes in Computer Science, vol. 12759, pp. 856–869. Springer (2021). https://doi.org/10.1007/978-3-030-...

    work page doi:10.1007/978-3-030-81685-8_40 2021

  3. [3]

    In: Groote, J.F., Larsen, K.G

    Ashok, P., Jackermeier, M., Kretínský, J., Weinhuber, C., Weininger, M., Yadav, M.: dtControl 2.0: Explainable strategy representation via decision tree learning steered by experts. In: Groote, J.F., Larsen, K.G. (eds.) 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021). Lecture Notes in Compute...

    work page doi:10.1007/978-3-030-72013-1_17 2021

  4. [4]

    In: Bouajjani, A., Holík, L., Wu, Z

    Azeem, M., Evangelidis, A., Kretínský, J., Slivinskiy, A., Weininger, M.: Optimistic and topological value iteration for simple stochastic games. In: Bouajjani, A., Holík, L., Wu, Z. (eds.) 20th International Symposium on Automated Technology for Veri- fication and Analysis (ATVA 2022). Lecture Notes in Computer Science, vol. 13505, pp. 285–302. Springer ...

    work page doi:10.1007/978-3-031-19992-9_18 2022

  5. [5]

    In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R

    Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook UMB: Unified Markov Binary Format for Probabilistic Model Checking 12 of Model Checking, pp. 963–999. Springer (2018).https://doi.org/10.1007/ 978-3-319-10575-8_28

    2018

  6. [6]

    MIT Press (2008)

    Baier, C., Katoen, J.P.: Principles of model checking. MIT Press (2008)

    2008

  7. [7]

    Formal Methods Syst

    Beyer, D., Kanav, S., Kleinert, T., Richter, C.: Construction of verifier combinations from off-the-shelf components. Formal Methods Syst. Des.66(1), 99–130 (2025). https://doi.org/10.1007/S10703-024-00449-Y

    work page doi:10.1007/s10703-024-00449-y 2025

  8. [8]

    IEEE Trans

    Bohnenkamp, H.C., D’Argenio, P.R., Hermanns, H., Katoen, J.P.: MoDeST: A compositional modeling formalism for hard and softly timed systems. IEEE Trans. Software Eng.32(10), 812–830 (2006).https://doi.org/10.1109/TSE.2006.104

    work page doi:10.1109/tse.2006.104 2006

  9. [9]

    In: Legay, A., Margaria, T

    Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: quantitative model and tool interaction. In: Legay, A., Margaria, T. (eds.) 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017). Lecture Notes in Computer Science, vol. 10206, pp. 151–168 (2017).https://doi.org/10...

    work page doi:10.1007/978-3-662-54580-5_9 2017

  10. [10]

    In: Margaria, T., Steffen, B

    Budde, C.E., Hartmanns, A., Klauck, M., Kretínský, J., Parker, D., Quatmann, T., Turrini, A., Zhang, Z.: On correctness, precision, and performance in quantitative verification - QComp 2020 competition report. In: Margaria, T., Steffen, B. (eds.) 9th International Symposium on Leveraging Applications of Formal Methods, Verifi- cation and Validation (ISoLA...

    work page doi:10.1007/978-3-030-83723-5_15 2020

  11. [11]

    In: Vojnar, T., Zhang, L

    Butkova, Y., Fox, G.: Optimal time-bounded reachability analysis for concurrent systems. In: Vojnar, T., Zhang, L. (eds.) 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019). Lecture Notes in Computer Science, vol. 11428, pp. 191–208. Springer (2019). https://doi.org/10.1007/978-3-030-17465-1_11

    work page doi:10.1007/978-3-030-17465-1_11 2019

  12. [12]

    ACM Trans

    Butkova, Y., Hartmanns, A., Hermanns, H.: A Modest approach to Markov au- tomata. ACM Trans. Model. Comput. Simul.31(3), 14:1–14:34 (2021).https: //doi.org/10.1145/3449355

    work page doi:10.1145/3449355 2021

  13. [13]

    In: Finkbeiner, B., Pu, G., Zhang, L

    Butkova, Y., Hatefi, H., Hermanns, H., Krcál, J.: Optimal continuous time Markov decisions. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) 13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015). Lecture Notes in Computer Science, vol. 9364, pp. 166–182. Springer (2015).https://doi. org/10.1007/978-3-319-24953-7_12

    work page doi:10.1007/978-3-319-24953-7_12 2015

  14. [14]

    Condon, A.: The complexity of stochastic games. Inf. Comput.96(2), 203–224 (1992).https://doi.org/10.1016/0890-5401(92)90048-K

    work page doi:10.1016/0890-5401(92)90048-k 1992

  15. [15]

    In: Baier, C., Tinelli, C

    David, A., Jensen, P.G., Larsen, K.G., Mikucionis, M., Taankvist, J.H.: Uppaal Stratego. In: Baier, C., Tinelli, C. (eds.) 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015). Lecture Notes in Computer Science, vol. 9035, pp. 206–211. Springer (2015).https: //doi.org/10.1007/978-3-662-46681-0_16

    work page doi:10.1007/978-3-662-46681-0_16 2015

  16. [16]

    In: 25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010)

    Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: 25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010). pp. 342–351. IEEE Computer Society (2010).https://doi.org/10.1109/ LICS.2010.41

    2010

  17. [17]

    In: Dutle, A., Muñoz, C.A., Narkawicz, A

    Fehnker, A., Chaudhary, K.: Twenty percent and a few days – optimising a Bitcoin majority attack. In: Dutle, A., Muñoz, C.A., Narkawicz, A. (eds.) 10th International NASA Formal Methods Symposium (NFM 2018). Lecture Notes in Computer Science, vol. 10811, pp. 157–163. Springer (2018).https://doi.org/10.1007/ 978-3-319-77935-5_11 UMB: Unified Markov Binary ...

    2018

  18. [18]

    Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf.15(2), 89–107 (2013).https://doi.org/10.1007/S10009-012-0244-Z

    work page doi:10.1007/s10009-012-0244-z 2011

  19. [19]

    Givan, R., Leach, S.M., Dean, T.L.: Bounded-parameter Markov decision processes. Artif. Intell.122(1-2), 71–109 (2000).https://doi.org/10.1016/S0004-3702(00) 00047-3

    work page doi:10.1016/s0004-3702(00 2000

  20. [20]

    In: Gotsman, A., Sokolova, A

    Gros, T.P., Hermanns, H., Hoffmann, J., Klauck, M., Steinmetz, M.: Deep statistical model checking. In: Gotsman, A., Sokolova, A. (eds.) 40th IFIP WG 6.1 Inter- national Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2020). Lecture Notes in Computer Science, vol. 12136, pp. 96–114. Springer (2020).https://doi.org/1...

    work page doi:10.1007/978-3-030-50086-3_6 2020

  21. [21]

    In: Goodloe, A., Person, S

    Guck, D., Han, T., Katoen, J.P., Neuhäußer, M.R.: Quantitative timed analy- sis of interactive Markov chains. In: Goodloe, A., Person, S. (eds.) 4th Interna- tional NASA Formal Methods Symposium (NFM 2012). Lecture Notes in Com- puter Science, vol. 7226, pp. 8–23. Springer (2012).https://doi.org/10.1007/ 978-3-642-28891-3_4

    2012

  22. [22]

    In: Vojnar, T., Zhang, L

    Hahn, E.M., Hartmanns, A., Hensel, C., Klauck, M., Klein, J., Kretínský, J., Parker, D., Quatmann, T., Ruijters, E., Steinmetz, M.: The 2019 comparison of tools for the analysis of quantitative formal models - (QComp 2019 competition report). In: Vojnar, T., Zhang, L. (eds.) 25th International Conference on Tools and Algorithms for the Construction and An...

    work page doi:10.1007/978-3-030-17502-3_5 2019

  23. [23]

    Formal Methods Syst

    Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.P.: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods Syst. Des. 43(2), 191–232 (2013).https://doi.org/10.1007/S10703-012-0167-Z

    work page doi:10.1007/s10703-012-0167-z 2013

  24. [24]

    In: Ábrahám, E., Havelund, K

    Hartmanns, A., Hermanns, H.: The Modest Toolset: An integrated environment for quantitative modelling and verification. In: Ábrahám, E., Havelund, K. (eds.) 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014). LNCS, vol. 8413, pp. 593–598. Springer (2014). https://doi.org/10.1007/978-3-642-54862-8_51

    work page doi:10.1007/978-3-642-54862-8_51 2014

  25. [25]

    In: Finkbeiner, B., Pu, G., Zhang, L

    Hartmanns, A., Hermanns, H.: Explicit model checking of very large MDP using partitioning and secondary storage. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) 13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015). Lecture Notes in Computer Science, vol. 9364, pp. 131–147. Springer (2015).https://doi.org/10.1007/978-...

    work page doi:10.1007/978-3-319-24953-7_10 2015

  26. [26]

    In: Krötzsch, M., Stepanova, D

    Hartmanns, A., Hermanns, H.: A Modest Markov automata tutorial. In: Krötzsch, M., Stepanova, D. (eds.) Reasoning Web – 15th International Summer School 2019, Tutorial Lectures. Lecture Notes in Computer Science, vol. 11810, pp. 250–276. Springer (2019).https://doi.org/10.1007/978-3-030-31423-1_8

    work page doi:10.1007/978-3-030-31423-1_8 2019

  27. [27]

    Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: The revised practitioner’s guide to MDP model checking algorithms. Int. J. Softw. Tools Technol. Transf. (2026).https://doi.org/10.1007/s10009-026-00848-y

    work page doi:10.1007/s10009-026-00848-y 2026

  28. [28]

    In: Vojnar, T., Zhang, L

    Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantita- tive verification benchmark set. In: Vojnar, T., Zhang, L. (eds.) 25th International Conference on Tools and Algorithms for the Construction and Analysis of Sys- tems (TACAS 2019). Lecture Notes in Computer Science, vol. 11427, pp. 344–350. Springer (2019).https://doi.org/10....

    work page doi:10.1007/978-3-030-17462-0_20 2019

  29. [29]

    Hensel, C.: The probabilistic model checker Storm: symbolic methods for proba- bilistic model checking. Ph.D. thesis, RWTH Aachen University, Germany (2018), http://publications.rwth-aachen.de/record/752011 UMB: Unified Markov Binary Format for Probabilistic Model Checking 14

    2018

  30. [30]

    Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf.24(4), 589–610 (2022). https://doi.org/10.1007/S10009-021-00633-Z

    work page doi:10.1007/s10009-021-00633-z 2022

  31. [31]

    In: Kiyavash, N., Mooij, J.M

    Ho, Q.H., Feather, M.S., Rossi, F., Sunberg, Z., Lahijanian, M.: Sound heuristic search value iteration for undiscounted POMDPs with reachability objectives. In: Kiyavash, N., Mooij, J.M. (eds.) 40th Conference on Uncertainty in Artificial Intelligence (UAI 2024). Proceedings of Machine Learning Research, vol. 244, pp. 1681–1697. PMLR (2024),https://proce...

    2024

  32. [32]

    In: Jansen, N., Tribastone, M

    Jeppson, J., Volk, M., Israelsen, B., Roberts, R., Williams, A., Buecherl, L., Myers, C.J., Zheng, H., Winstead, C., Zhang, Z.: STAMINA in C++: modernizing an infinite-state probabilistic model checker. In: Jansen, N., Tribastone, M. (eds.) 20th International Conference on Quantitative Evaluation of Systems (QEST 2023). Lecture Notes in Computer Science, ...

    work page doi:10.1007/978-3-031-43835-6_7 2023

  33. [33]

    In: Gurfinkel, A., Ganesh, V

    Johannsen, C., Nukala, K., Dureja, R., Irfan, A., Shankar, N., Tinelli, C., Vardi, M.Y., Rozier, K.Y.: The MoXI model exchange tool suite. In: Gurfinkel, A., Ganesh, V. (eds.) 36th International Conference on Computer Aided Verification (CAV 2024). Lecture Notes in Computer Science, vol. 14681, pp. 203–218. Springer (2024). https://doi.org/10.1007/978-3-0...

    work page doi:10.1007/978-3-031-65627-9_10 2024

  34. [34]

    Kaelbling, L.P., Littman, M.L., Cassandra, A.R.: Planning and acting in partially observable stochastic domains. Artif. Intell.101(1-2), 99–134 (1998).https://doi. org/10.1016/S0004-3702(98)00023-X

    work page doi:10.1016/s0004-3702(98)00023-x 1998

  35. [35]

    In: Bertrand, N., Dubslaff, C., Klüppelholz, S

    Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking: Applica- tions and trends. In: Bertrand, N., Dubslaff, C., Klüppelholz, S. (eds.) Principles of Formal Quantitative Analysis. Lecture Notes in Computer Science, vol. 15760, pp. 158–173. Springer (2025).https://doi.org/10.1007/978-3-031-97439-7_7

    work page doi:10.1007/978-3-031-97439-7_7 2025

  36. [36]

    In: Gopalakrishnan, G., Qadeer, S

    Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of prob- abilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) 23rd In- ternational Conference on Computer Aided Verification (CAV 2011). Lecture Notes in Computer Science, vol. 6806, pp. 585–591. Springer (2011). https: //doi.org/10.1007/978-3-642-22110-1_47

    work page doi:10.1007/978-3-642-22110-1_47 2011

  37. [37]

    Kwiatkowska, M.Z., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282(1), 101–150 (2002).https://doi.org/10.1016/S0304-3975(01)00046-9

    work page doi:10.1016/s0304-3975(01)00046-9 2002

  38. [38]

    Leerkes, P., Melse, I., Heck, L., Volk, M., Junges, S.: Stormvogel: Probabilistic model checking for almost everyone. Tech. rep., Radboud University Nijmegen (2025),https://hdl.handle.net/2066/325553

    2025

  39. [39]

    In: Gurfinkel, A., Ganesh, V

    Meggendorfer, T., Weininger, M.: Playing games with your PET: extending the partial exploration tool to stochastic games. In: Gurfinkel, A., Ganesh, V. (eds.) 36th International Conference on Computer Aided Verification (CAV 2024). Lecture Notes in Computer Science, vol. 14683, pp. 359–372. Springer (2024).https: //doi.org/10.1007/978-3-031-65633-0_16

    work page doi:10.1007/978-3-031-65633-0_16 2024

  40. [40]

    prismmodelchecker.org/manual/Appendices/ExplicitModelFiles

    PRISM developers: PRISM explicit model format specification, https://www. prismmodelchecker.org/manual/Appendices/ExplicitModelFiles

  41. [41]

    prismmodelchecker.org/manual/ThePRISMLanguage

    PRISM developers: PRISM modelling language documentation, https://www. prismmodelchecker.org/manual/ThePRISMLanguage

  42. [42]

    Nesterov, Y

    Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Pro- gramming. Wiley Series in Probability and Statistics, Wiley (1994). https: //doi.org/10.1002/9780470316887

    work page doi:10.1002/9780470316887 1994

  43. [43]

    SIAM (2003) UMB: Unified Markov Binary Format for Probabilistic Model Checking 15

    Saad, Y.: Iterative Methods for Sparse Linear Systems. SIAM (2003) UMB: Unified Markov Binary Format for Probabilistic Model Checking 15

    2003

  44. [44]

    Proceedings of the National Academy of Sciences 39(10), 1095–1100 (1953).https://doi.org/10.1073/pnas.39.10.1095

    Shapley, L.S.: Stochastic games. Proceedings of the National Academy of Sciences 39(10), 1095–1100 (1953).https://doi.org/10.1073/pnas.39.10.1095

    work page doi:10.1073/pnas.39.10.1095 1953

  45. [45]

    Storm developers: DRN format description, https://www.stormchecker.org/ documentation/background/drn.html

  46. [46]

    format-version

    Waddoups, N., Boe, J., Hartmanns, A., Basu, P., Roy, S., Chakraborty, K., Zhang, Z.: Probabilistic verification for modular network-on-chip systems. In: 27th International Conference on Verification, Model Checking, and Abstract Inter- pretation (VMCAI 2026). Lecture Notes in Computer Science, Springer (2026). https://doi.org/10.1007/978-3-032-15700-3_18 ...

    work page doi:10.1007/978-3-032-15700-3_18 2026