pith. sign in

arxiv: 2606.21444 · v1 · pith:YVGSOPIFnew · submitted 2026-06-19 · 💻 cs.LO

Verification of Parametric Markov Automata under Time-bounded Reachability

Kevin van de Glind , Matthias Volk , Tim Willemse This is my paper

Pith reviewed 2026-06-26 12:37 UTC · model grok-4.3

classification 💻 cs.LO
keywords parametric Markov automatatime-bounded reachabilitysynthesis problemsdiscretizationparametric Markov decision processesmodel checkingformal verificationparameter space partitioning
0
0 comments X

The pith

Parametric Markov automata can be discretized to parametric Markov decision processes to solve two synthesis problems for time-bounded reachability up to arbitrary precision.

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

The paper introduces parametric Markov automata to model uncertainty in transition rates that are not fully known. It defines two synthesis problems: determining whether some parameter valuation makes a time-bounded reachability property hold or fail, and partitioning the entire parameter space into regions that satisfy or violate the property. The method first discretizes the parametric Markov automaton into a parametric Markov decision process and then computes probability bounds on the discretized model. These bounds suffice to answer both synthesis questions once accumulated discretization and analysis errors are driven below any chosen threshold. Experiments in the Storm model checker confirm that the approach terminates with the required precision, with discretization identified as the dominant cost.

Core claim

By converting a parametric Markov automaton into a parametric Markov decision process through discretization, upper and lower bounds on time-bounded reachability probabilities can be computed; these bounds become tight enough, as error terms are reduced, to decide existence of satisfying valuations and to partition the parameter space into satisfying and violating regions for any requested precision.

What carries the argument

Discretization step that turns a parametric Markov automaton into a parametric Markov decision process whose reachability bounds are then analyzed to control accumulated error.

If this is right

  • Both the existence and the partitioning synthesis problems become decidable up to any chosen precision.
  • The accumulated discretization and numerical errors can be reduced without bound by increasing refinement.
  • The method is implemented inside the Storm model checker and terminates on the tested benchmarks.
  • Performance is limited primarily by the cost of the initial discretization step.

Where Pith is reading between the lines

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

  • The same discretization-plus-bounding technique could be reused for other time-dependent properties once the underlying pMDP analysis is extended.
  • Parameter-space partitioning yields explicit regions that could guide controller synthesis or robust design under rate uncertainty.
  • If the discretization error bound is tightened further, the approach might scale to models with more parameters before hitting computational limits.

Load-bearing premise

Discretization must preserve the original reachability probability bounds tightly enough that the total error can be driven below any given threshold without creating artifacts that change the synthesis answers.

What would settle it

A concrete parametric Markov automaton for which repeated refinement of the discretization still leaves an error interval that straddles the decision threshold for the synthesis problem, producing an inconclusive or incorrect answer.

Figures

Figures reproduced from arXiv: 2606.21444 by Kevin van de Glind, Matthias Volk, Tim Willemse.

Figure 1
Figure 1. Figure 1: (a) Parametric MA with nondeterministic transitions in [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Satisfaction relations. Problem statement. Now that pMA are formally defined, we provide a formal problem definition. In contrast to MA, the analysis of pMA also needs to reason about the parameter valuations. We solve two main problems for time-bounded reachability properties: (1) satisfaction verification checks whether there exists a valuation in the region which satisfies/violates the given property, a… view at source ↗
Figure 3
Figure 3. Figure 3: Outline of the process for different synthesis problems. [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Violinplot of probabilities for 104 pMA instantiations on Jobs benchmark with R = [1, 3]2 ; horizontal lines are the approximate discretization bounds. Definition 6 (Approximate discretized pMA). Given discretization step δ > 0, N ∈ N>0, and pMA M = (S, A, s0, →,⇒). The approximate discretized parametric Markov Automaton is given by Mδ N = (S, A, s0, P′ ), where: P ′ (s, s′ ) = ( (1 − PN k=0 (−λ(s))k k! )p… view at source ↗
Figure 5
Figure 5. Figure 5: Parameter synthesis on stream2-4 under different satisfaction relations. with Figure 2b, the fraction of satisfying valuations for the robust satisfaction relation is always at least as large as that for the demonic relation [PITH_FULL_IMAGE:figures/full_fig_p015_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Ratio of decided area over runtime for pMA benchmarks. [PITH_FULL_IMAGE:figures/full_fig_p016_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Parameter synthesis on stream2-4 under different satisfaction relations. (a) Demonic (b) Robust [PITH_FULL_IMAGE:figures/full_fig_p020_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Parameter synt. on readers-writers5 under different satisfaction relations [PITH_FULL_IMAGE:figures/full_fig_p020_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Parameter synthesis on jobs5-2 under different satisfaction relations. (a) Demonic (b) Robust [PITH_FULL_IMAGE:figures/full_fig_p021_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Paramet. synt. on flexible-manufacturing3 under diff. satisf. relations. (a) Demonic (b) Robust [PITH_FULL_IMAGE:figures/full_fig_p021_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Parameter synthesis on polling under different satisfaction relations [PITH_FULL_IMAGE:figures/full_fig_p021_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Parameter synthesis on polling9 pCTMC [PITH_FULL_IMAGE:figures/full_fig_p022_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Parameter synthesis on tandem pCTMC [PITH_FULL_IMAGE:figures/full_fig_p022_13.png] view at source ↗
read the original abstract

Analysis of Markov models is of high importance for formal verification. Until now, analysis of Markov Automata required them to be fully specified, which is a considerable restriction as rates may be unknown or influenced by uncertainty of the environment. We introduce parametric Markov Automata (pMA) to capture this uncertainty with parametric transition functions. On these parametrized models, two different synthesis problems for time-bounded reachability properties are considered: I) Does there exist a valuation in the parameter space such that the instantiated model satisfies/violates the property, and II) given the parameter space, how can it be partitioned into satisfying and violating regions? Our approach comprises two steps: I) The pMA is discretized to a parametric Markov decision process (pMDP), and II) through analysis of the pMDP, bounds are obtained for the reachability probability in the parametric MA. This approach solves the above problems up to a specified precision, as the accumulated error terms can be made arbitrarily small. We implemented the approach using the Storm model checker. Our experimental evaluation shows that the main performance bottlenecks originate from the discretization of the pMA.

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

1 major / 0 minor

Summary. The paper introduces parametric Markov Automata (pMA) to capture uncertainty in transition rates. It defines two synthesis problems for time-bounded reachability properties: (I) existence of a parameter valuation making the instantiated model satisfy or violate the property, and (II) partitioning the parameter space into satisfying and violating regions. The method discretizes the pMA into a pMDP, then analyzes the pMDP to derive bounds on reachability probabilities; the abstract asserts that accumulated discretization error terms can be driven below any given threshold. The approach is implemented in the Storm model checker, with experiments identifying discretization as the main performance bottleneck.

Significance. If the error-control claim holds with uniform bounds over the parameter space, the work would extend existing MA verification techniques to models with uncertain rates, directly supporting synthesis queries that arise in practice. The Storm implementation and the experimental identification of discretization as the bottleneck are concrete strengths that would aid reproducibility and future optimization.

major comments (1)
  1. [Abstract] Abstract: the central claim that 'the accumulated error terms can be made arbitrarily small' is load-bearing for both synthesis problems being solved 'up to a specified precision,' yet the text provides neither an explicit error-bound formula nor a derivation showing how the discretization step (uniformization or time-stepping) interacts with parametric rates whose supremum is taken over the entire parameter space.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and for highlighting the need for greater clarity on the error-control argument that underpins the precision claims.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the central claim that 'the accumulated error terms can be made arbitrarily small' is load-bearing for both synthesis problems being solved 'up to a specified precision,' yet the text provides neither an explicit error-bound formula nor a derivation showing how the discretization step (uniformization or time-stepping) interacts with parametric rates whose supremum is taken over the entire parameter space.

    Authors: We agree that the abstract and surrounding text would benefit from an explicit error-bound formula and a short derivation addressing the interaction with the supremum over the parameter space. The technical development already selects the discretization step size on the basis of the supremum rate, but the manuscript does not isolate and display the resulting uniform bound. We will therefore add a concise statement of the error formula (including the dependence on the supremum rate) together with a one-paragraph derivation sketch, either in the abstract or in a new paragraph of the introduction, and we will cross-reference the detailed proofs in Sections 4–5. revision: yes

Circularity Check

0 steps flagged

No circularity; derivation reduces to independent pMDP analysis

full rationale

The paper presents a two-step reduction: discretize pMA to pMDP, then obtain reachability bounds via pMDP analysis, with the claim that accumulated discretization errors can be driven below any threshold. No equations or steps are shown that define a quantity in terms of itself, rename a fit as a prediction, or rely on self-citation for a uniqueness result. The error controllability is asserted as a property of the discretization (standard for MA), not derived from the target synthesis answers. This is a normal non-circular reduction to an external analysis problem.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The approach rests on standard properties of Markov automata and MDPs plus the claim that discretization error is controllable; no free parameters beyond the user-specified precision are mentioned.

axioms (1)
  • domain assumption Markov automata can be discretized to MDPs while preserving reachability probabilities up to controllable error.
    Invoked in the two-step approach described in the abstract.
invented entities (1)
  • parametric Markov Automaton (pMA) no independent evidence
    purpose: Model with parametric transition rates to capture uncertainty.
    New modeling formalism introduced to extend standard MA.

pith-pipeline@v0.9.1-grok · 5729 in / 1328 out tokens · 15724 ms · 2026-06-26T12:37:54.039722+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

39 extracted references · 21 canonical work pages

  1. [1]

    In: ATVA

    Ashok, P., Butkova, Y., Hermanns, H., Kretínský, J.: Continuous-time Markov decisions based on partial exploration. In: ATVA. Lecture Notes in Com- puter Science, vol. 11138, pp. 317–334. Springer (2018). https://doi.org/10.1007/ 978-3-030-01090-4_19

    2018

  2. [2]

    Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Verifying continuous time Markov chains. In: CAV. Lecture Notes in Computer Science, vol. 1102, pp. 269–276. Springer (1996). https://doi.org/10.1007/3-540-61474-5_75

    work page doi:10.1007/3-540-61474-5_75 1996

  3. [3]

    In: QAPL

    Braitling, B., Fioriti, L.M.F., Hatefi, H., Wimmer, R., Becker, B., Hermanns, H.: MeGARA: Menu-based game abstraction and abstraction refinement of Markov automata. In: QAPL. EPTCS, vol. 154, pp. 48–63 (2014). https://doi.org/10.4204/ EPTCS.154.4

    2014

  4. [4]

    In: TACAS (2)

    Butkova, Y., Fox, G.: Optimal time-bounded reachability analysis for concurrent systems. In: TACAS (2). Lecture Notes in Computer Science, vol. 11428, pp. 191–

  5. [5]

    In: Vojnar, T., Zhang, L

    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

  6. [6]

    In: QEST

    Butkova, Y., Hartmanns, A., Hermanns, H.: A modest approach to modelling and checking Markov automata. In: QEST. Lecture Notes in Computer Science, vol. 11785, pp. 52–69. Springer (2019). https://doi.org/10.1007/978-3-030-30281-8_4

    work page doi:10.1007/978-3-030-30281-8_4 2019

  7. [7]

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

    Butkova, Y., Hatefi, H., Hermanns, H., Krcál, J.: Optimal continuous time Markov decisions. In: ATVA. 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

  8. [8]

    In: TACAS(2)

    Butkova, Y., Wimmer, R., Hermanns, H.: Long-run rewards for Markov automata. In: TACAS(2). Lecture Notes in ComputerScience, vol.10206, pp. 188–203(2017). https://doi.org/10.1007/978-3-662-54580-5_11

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

  9. [9]

    Acta Informatica54(6), 589– 623 (2017)

    Ceska, M., Dannenberg, F., Paoletti, N., Kwiatkowska, M., Brim, L.: Precise pa- rameter synthesis for stochastic biochemical systems. Acta Informatica54(6), 589– 623 (2017). https://doi.org/10.1007/S00236-016-0265-2

    work page doi:10.1007/s00236-016-0265-2 2017

  10. [10]

    In: TACAS (2)

    Ceska, M., Jansen, N., Junges, S., Katoen, J.P.: Shepherding hordes of Markov chains. In: TACAS (2). Lecture Notes in Computer Science, vol. 11428, pp. 172–

  11. [11]

    https://doi.org/10.1007/978-3-030-17465-1_10

    Springer (2019). https://doi.org/10.1007/978-3-030-17465-1_10

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

  12. [12]

    In: TACAS

    Ceska, M., Pilar, P., Paoletti, N., Brim, L., Kwiatkowska, M.Z.: PRISM-PSY: precise GPU-accelerated parameter synthesis for stochastic systems. In: TACAS. Lecture Notes in Computer Science, vol. 9636, pp. 367–384. Springer (2016). https://doi.org/10.1007/978-3-662-49674-9_21

    work page doi:10.1007/978-3-662-49674-9_21 2016

  13. [13]

    In: ICTAC

    Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. In: ICTAC. Lecture Notes in Computer Science, vol. 3407, pp. 280–294. Springer (2004). https://doi.org/10.1007/978-3-540-31862-0_21

    work page doi:10.1007/978-3-540-31862-0_21 2004

  14. [14]

    IEEE Transactions on reliability41(3), 363–377 (2002)

    Dugan, J.B., Bavuso, S.J., Boyd, M.A.: Dynamic fault-tree models for fault- tolerant computer systems. IEEE Transactions on reliability41(3), 363–377 (2002)

    2002

  15. [15]

    In: LICS

    Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS. pp. 342–351. IEEE Computer Society (2010). https://doi.org/10. 1109/LICS.2010.41

    2010

  16. [16]

    Garling, D.J.: A Course in Mathematical Analysis: Volume 2, Metric and Topolog- ical Spaces, Functions of a Vector Variable, chap. 12. Cambridge University Press (2014)

    2014

  17. [17]

    Master’s thesis, Universität des Saarlandes (2018)

    Gros, T.P.: Markov Automata taken by Storm. Master’s thesis, Universität des Saarlandes (2018)

    2018

  18. [18]

    In: NASA Formal Methods

    Guck, D., Han, T., Katoen, J.P., Neuhäußer, M.R.: Quantitative timed analy- sis of interactive Markov chains. In: NASA Formal Methods. Lecture Notes in 18 Kevin van de Glind, Matthias Volk, and Tim A.C. Willemse Computer Science, vol. 7226, pp. 8–23. Springer (2012). https://doi.org/10.1007/ 978-3-642-28891-3_4

    2012

  19. [19]

    Guck, D., Hatefi, H., Hermanns, H., Katoen, J.P., Timmer, M.: Analysis of timed and long-run objectives for Markov automata. Log. Methods Comput. Sci.10(3) (2014). https://doi.org/10.2168/LMCS-10(3:17)2014

    work page doi:10.2168/lmcs-10(3:17)2014 2014

  20. [20]

    In: NASA Formal Methods

    Hahn, E.M., Han, T., Zhang, L.: Synthesis for PCTL in parametric Markov decision processes. In: NASA Formal Methods. Lecture Notes in Computer Science, vol. 6617, pp. 146–161. Springer (2011). https://doi.org/10.1007/ 978-3-642-20398-5_12

    2011

  21. [21]

    In: SETTA

    Hahn, E.M., Hartmanns, A.: A comparison of time- and reward-bounded proba- bilistic model checking techniques. In: SETTA. Lecture Notes in Computer Science, vol. 9984, pp. 85–100 (2016). https://doi.org/10.1007/978-3-319-47677-3_6

    work page doi:10.1007/978-3-319-47677-3_6 2016

  22. [22]

    Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. Int. J. Softw. Tools Technol. Transf.13(1), 3–19 (2011). https: //doi.org/10.1007/S10009-010-0146-X

    work page doi:10.1007/s10009-010-0146-x 2011

  23. [23]

    Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: A web-based probabilistic model checker. In: FM. Lecture Notes in Computer Science, vol. 8442, pp. 312–317. Springer (2014). https://doi.org/10.1007/978-3-319-06410-9_22

    work page doi:10.1007/978-3-319-06410-9_22 2014

  24. [24]

    In: RTSS

    Han, T., Katoen, J.P., Mereacre, A.: Approximate parameter synthesis for proba- bilistic time-bounded reachability. In: RTSS. pp. 173–182. IEEE Computer Society (2008). https://doi.org/10.1109/RTSS.2008.19

    work page doi:10.1109/rtss.2008.19 2008

  25. [25]

    In: TACAS

    Hartmanns, A., Hermanns, H.: The modest toolset: An integrated environment for quantitative modelling and verification. In: TACAS. Lecture Notes in Com- puter Science, vol. 8413, pp. 593–598. Springer (2014). https://doi.org/10.1007/ 978-3-642-54862-8_51

    2014

  26. [26]

    In: QEST

    Hartmanns, A., Katoen, J.P., Kohlen, B., Spel, J.: Tweaking the odds in proba- bilistic timed automata. In: QEST. Lecture Notes in Computer Science, vol. 12846, pp. 39–58. Springer (2021). https://doi.org/10.1007/978-3-030-85172-9_3

    work page doi:10.1007/978-3-030-85172-9_3 2021

  27. [27]

    In: TACAS (1)

    Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quan- titative verification benchmark set. In: TACAS (1). Lecture Notes in Com- puter Science, vol. 11427, pp. 344–350. Springer (2019). https://doi.org/10.1007/ 978-3-030-17462-0_20

    2019

  28. [28]

    Elec- tron

    Hatefi, H., Hermanns, H.: Model checking algorithms for Markov automata. Elec- tron. Commun. Eur. Assoc. Softw. Sci. Technol.53(2012). https://doi.org/10. 14279/TUJ.ECEASST.53.783

    2012

  29. [29]

    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

  30. [30]

    Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality, Lec- ture Notes in Computer Science, vol. 2428. Springer (2002). https://doi.org/10. 1007/3-540-45804-2

    2002

  31. [31]

    Formal Methods Syst

    Junges, S., Ábrahám, E., Hensel, C., Jansen, N., Katoen, J.P., Quatmann, T., Volk, M.: Parameter synthesis for Markov models: covering the parameter space. Formal Methods Syst. Des.62(1), 181–259 (2024). https://doi.org/10.1007/ S10703-023-00442-X

    2024

  32. [32]

    In: LICS

    Katoen, J.P.: The probabilistic model checking landscape. In: LICS. pp. 31–45. ACM (2016). https://doi.org/10.1145/2933575.2934574

    work page doi:10.1145/2933575.2934574 2016

  33. [33]

    Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of proba- bilistic real-time systems. In: CAV. Lecture Notes in Computer Science, vol. 6806, pp. 585–591. Springer (2011). https://doi.org/10.1007/978-3-642-22110-1_47 Verification of parametric Markov Automata 19

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

  34. [34]

    ACM Trans

    Marsan, M.A., Conte, G., Balbo, G.: A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems. ACM Trans. Comput. Syst.2(2), 93–122 (1984). https://doi.org/10.1145/190.191

    work page doi:10.1145/190.191 1984

  35. [35]

    SIAM Journal on Control6(2), 266–280 (May 1968)

    Miller, B.L.: Finite state continuous time Markov decision processes with a finite planning horizon. SIAM Journal on Control6(2), 266–280 (May 1968). https:// doi.org/10.1137/0306020

    work page doi:10.1137/0306020 1968

  36. [36]

    Neuhäußer, M.R.: Model checking nondeterministic and randomly timed systems. Ph.D. thesis, RWTH Aachen University (2010)

    2010

  37. [37]

    In: FoSSaCS

    Neuhäußer, M.R., Stoelinga, M., Katoen, J.P.: Delayed nondeterminism in continuous-time Markov decision processes. In: FoSSaCS. Lecture Notes in Com- puter Science, vol. 5504, pp. 364–379. Springer (2009). https://doi.org/10.1007/ 978-3-642-00596-1_26

    2009

  38. [38]

    In: ATVA

    Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.P.: Parameter syn- thesis for Markov models: Faster than ever. In: ATVA. Lecture Notes in Computer Science,vol.9938,pp.50–67(2016).https://doi.org/10.1007/978-3-319-46520-3_4

    work page doi:10.1007/978-3-319-46520-3_4 2016

  39. [39]

    Cengage (2021) 20 Kevin van de Glind, Matthias Volk, and Tim A.C

    Stewart, J., Clegg, D., Watson, S.: Calculus: early transcendentals. Cengage (2021) 20 Kevin van de Glind, Matthias Volk, and Tim A.C. Willemse A Parameter synthesis figures We provide the parameter synthesis results for all considered models. Visual- izations for the pMA models under both the demonic and robust satisfaction relation are given in Figures ...

    2021