pith. sign in

arxiv: 1907.08491 · v1 · pith:3APMAXFMnew · submitted 2019-07-19 · 💻 cs.LO

Are Parametric Markov Chains Monotonic?

Jip Spel , Sebastian Junges , Joost-Pieter Katoen This is my paper

Pith reviewed 2026-05-24 19:01 UTC · model grok-4.3

classification 💻 cs.LO
keywords parametric Markov chainsmonotonicityreachability probabilitiesparameter synthesispre-ordergraph algorithmsprobabilistic model checking
0
0 comments X

The pith

A pre-order on states built from graph structure and local probabilities suffices to check monotonicity of reachability probabilities in parametric Markov chains.

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

The paper develops an algorithm that decides whether reachability probabilities grow or shrink with changes to parameters in a parametric Markov chain. It builds a pre-order on the states using only the chain's graph and the probabilities on its outgoing edges, then checks whether this pre-order satisfies a condition that guarantees monotonicity for selected parameters. When the check succeeds, the method avoids expensive symbolic computation and accelerates subsequent parameter synthesis. Experiments on standard benchmarks show that the check often succeeds and yields speed-ups of orders of magnitude over a symbolic baseline.

Core claim

Reachability probabilities in parametric Markov chains are monotonic in selected parameters precisely when a pre-order constructed solely from the underlying graph and the local transition probabilities satisfies a simple, efficiently checkable condition.

What carries the argument

Pre-order on states derived from graph structure and local transition probabilities, serving as a sufficient condition for monotonicity of reachability probabilities.

If this is right

  • When the pre-order condition holds, reachability probabilities are guaranteed monotonic in the tested parameters.
  • Monotonicity confirmation lets parameter synthesis replace symbolic methods with faster, monotonicity-aware search.
  • The linear-time pre-order check runs on the explicit graph and succeeds on several published benchmarks.
  • Synthesis time drops by orders of magnitude once monotonicity is established for the relevant parameters.

Where Pith is reading between the lines

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

  • The same graph-based pre-order might be reusable to certify monotonicity for other quantitative properties such as expected rewards.
  • If the pre-order test fails, the chain may still be monotonic for restricted parameter ranges that the current method does not yet detect.
  • The structural insight encoded in the pre-order could guide the design of monotonicity-preserving abstractions for larger models.

Load-bearing premise

The pre-order built from the graph and local probabilities is sufficient to certify monotonicity without inspecting the full parameter space or any symbolic expression.

What would settle it

A parametric Markov chain in which the pre-order condition holds for a parameter yet direct numerical evaluation shows that the reachability probability is not monotonic in that parameter.

Figures

Figures reproduced from arXiv: 1907.08491 by Jip Spel, Joost-Pieter Katoen, Sebastian Junges.

Figure 1
Figure 1. Figure 1: Three simple pMCs Definition 1 (Multivariate monotonic function). A function f : R n → R is monotonic increasing in xi on set R ⊂ R n, denoted f↑ R xi , if f(a) ≤ f(a + b · ei) ∀a ∈ R ∀b ∈ R≥0. A function f is monotone decreasing in xi on R, denoted f↓ R xi , if (−f)↑ R xi . A function f is monotone increasing (decreasing) on R, denoted f↑ R (f↓ R), if f↑ R xi (f↓ R xi ) for all xi ∈ x, respectively. If fu… view at source ↗
Figure 2
Figure 2. Figure 2: RO-graphs for some of the pMCs in [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Illustrating the use of assumptions s3 ≺ s2. We below adapt Alg. 1 such that, instead of adding s1 between s4 and s5(l. 11), we create three copies of the reachability order. In the copy assuming s2 ≺ s3 we can order s1 as in [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: An example pMC consisting of a single SCC PrsM[u] (♦T ) ∈ [as, bs] for all u ∈ R. Assumption s1 ≺ s2 can be proven by checking bs1 ≤ as2 . 4.3 Treating cycles So far, we considered acyclic pMCs. We use two techniques to treat cycles. SCC elimination [31] contracts each SCC into a set of states, one for each entry state of the SCC [PITH_FULL_IMAGE:figures/full_fig_p012_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: What coverage (x-axis) in how much time (y-axis)? when using PLA (dotted) or Monotonicity/Sampling (solid) . The two colours indicate two different thresholds. partially applied state elimination, or using a notion of multi-step local mono￾tonicity (used in the proof of Thm. 2) are avenues for improvement. Does monotonicity allow for faster parameter synthesis? We consider three variants of parameter synth… view at source ↗
Figure 6
Figure 6. Figure 6: Outline of the construction for the proof of Lem. 2 A Proofs A.1 Proof of Theorem 1 and Lem. 2 Reductions are many-to-one reductions. The proofs use notions from Sect. 3. We use the following formal definition of the decision problems: – (pMC-V) Given a pMC M with a threshold λ ∈ [0, 1], and a graph-preserving region R, does Prs→T M (u) ≥ λ hold for all u ∈ R? – (pMC-RO) Given a pMC M with a graph-preservi… view at source ↗
Figure 7
Figure 7. Figure 7: Outline of the construction for the proof of Lem. 7 – T ′ = T ∪ {B} – V ′ = V – P ′ (s, s′ ) =    P(s, s′ ) if s, s′ ∈ S λ if s = A, s′ = B 1 − λ if s = A, s′ = C 1 if s = s ′ = B 1 if s = s ′ = C 0 otherwise States s1 and s2 now correspond to A and sI , respectively. This transformation clearly is in polynomial time. Now, the probability to reach the target from A is λ for any parameter… view at source ↗
read the original abstract

This paper presents a simple algorithm to check whether reachability probabilities in parametric Markov chains are monotonic in (some of) the parameters. The idea is to construct - only using the graph structure of the Markov chain and local transition probabilities - a pre-order on the states. Our algorithm cheaply checks a sufficient condition for monotonicity. Experiments show that monotonicity in several benchmarks is automatically detected, and monotonicity can speed up parameter synthesis up to orders of magnitude faster than a symbolic baseline.

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 / 2 minor

Summary. The paper presents a simple algorithm that constructs a pre-order on states of a parametric Markov chain using only the underlying graph structure and local transition probabilities. This pre-order is used to check a sufficient condition for monotonicity of reachability probabilities with respect to some parameters. The authors report that the check is cheap, detects monotonicity on several benchmarks, and can accelerate parameter synthesis by orders of magnitude compared to a symbolic baseline.

Significance. If the claimed sufficient condition is correctly established, the algorithm supplies an inexpensive syntactic check that can be used as a preprocessing step before expensive symbolic or numeric synthesis procedures. The reported experimental speedups on benchmarks constitute a practical strength, as they demonstrate concrete gains when the condition holds.

major comments (2)
  1. [§4] §4 (Theorem on sufficiency): the proof that the pre-order implies monotonicity of the reachability probability must explicitly address the case in which a single parameter appears in multiple transitions. The linear system whose solution yields the reachability probability is global; a local ordering on individual transitions does not automatically guarantee that the closed-form rational function is monotonic when parameters are shared across edges.
  2. [§3.2] §3.2 (Definition of the pre-order): the construction is stated to depend only on graph structure and local probabilities, yet the central claim is that this yields a sufficient condition for monotonicity of the global solution. A counter-example or additional invariant is needed to show why simultaneous effects of one parameter cannot reverse the expected direction.
minor comments (2)
  1. [Experiments] The experimental section would benefit from reporting the fraction of benchmarks on which the sufficient condition actually holds, rather than only the speedups on the subset where it succeeds.
  2. Notation for the pre-order relation and the set of parameters it applies to should be introduced once and used consistently; currently the same symbol appears to be overloaded between the state ordering and the parameter ordering.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading of the manuscript and for the constructive comments on the handling of shared parameters. We address the two major comments below, agreeing that explicit clarification strengthens the presentation of the sufficient condition.

read point-by-point responses

  1. Referee: [§4] §4 (Theorem on sufficiency): the proof that the pre-order implies monotonicity of the reachability probability must explicitly address the case in which a single parameter appears in multiple transitions. The linear system whose solution yields the reachability probability is global; a local ordering on individual transitions does not automatically guarantee that the closed-form rational function is monotonic when parameters are shared across edges.

    Authors: We agree that an explicit treatment of parameters appearing in multiple transitions strengthens the proof. The argument in Theorem 4 proceeds via the linear system for reachability probabilities and shows that the pre-order on states induces consistent signs on the relevant partial derivatives. When a parameter p occurs on several edges, the construction ensures that all such occurrences affect comparable states in a manner that preserves the monotonicity direction in the global solution. In the revised version we will expand the proof with a dedicated paragraph providing this case analysis. revision: yes

  2. Referee: [§3.2] §3.2 (Definition of the pre-order): the construction is stated to depend only on graph structure and local probabilities, yet the central claim is that this yields a sufficient condition for monotonicity of the global solution. A counter-example or additional invariant is needed to show why simultaneous effects of one parameter cannot reverse the expected direction.

    Authors: The pre-order is defined so that its transitive closure encodes an invariant on the influence of each parameter across the graph: if two states are related, any shared parameter on their outgoing transitions contributes to the reachability probability with the same monotonicity sign. This invariant is a direct consequence of the local comparison rules and the graph-based propagation. We will insert a brief paragraph after the definition in §3.2 that states this invariant explicitly and explains why reversal is precluded. revision: yes

Circularity Check

0 steps flagged

No circularity; sufficient-condition algorithm is self-contained graph-based check.

full rationale

The paper defines an algorithm that builds a pre-order solely from the underlying graph and local parametric transition probabilities, then proves (by standard reachability arguments) that this pre-order is sufficient to guarantee monotonicity of the reachability probabilities. No parameter fitting occurs, no result is renamed as a prediction, and no load-bearing step reduces to a self-citation or self-definition. The central claim is an independent soundness argument for a cheap syntactic check; it does not presuppose the global monotonicity property it is checking. This is the normal case of a verification algorithm whose correctness is established directly from its construction.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

No free parameters, axioms, or invented entities identifiable from the abstract alone.

pith-pipeline@v0.9.0 · 5597 in / 1029 out tokens · 25801 ms · 2026-05-24T19:01:09.100090+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

48 extracted references · 48 canonical work pages · 2 internal anchors

  1. [1]

    PARAM website (2019), https://depend.cs.uni-saarland.de/tools/param/

    work page 2019

  2. [2]

    In: SRDS

    Aflaki, S., Volk, M., Bonakdarpour, B., Katoen, J.P., Stor johann, A.: Automated fine tuning of probabilistic self-stabilizing algorithms. In: SRDS. IEEE CS (2017)

    work page 2017

  3. [3]

    In: Handbook of Model Checking

    Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Mod el checking probabilistic systems. In: Handbook of Model Checking. Springer (2018)

    work page 2018

  4. [4]

    MI T Press (2008) 3 Although monotonicity is not explicitly mentioned in [40]

    Baier, C., Katoen, J.P.: Principles of model checking. MI T Press (2008) 3 Although monotonicity is not explicitly mentioned in [40]. 15

    work page 2008

  5. [5]

    In: TACAS

    Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R ., Smolka, S.A.: Model repair for probabilistic systems. In: TACAS. LNCS, vol. 660 5. Springer (2011)

    work page 2011

  6. [6]

    In: IJCAI

    Bharadwaj, S., Roux, S.L., P´ erez, G.A., Topcu, U.: Reduction techniques for model checking and learning in MDPs. In: IJCAI. ijcai.org (2017)

    work page 2017

  7. [7]

    Bohnenkamp, H.C., van der Stok, P., Hermanns, H., Vaandra ger, F.W.: Cost- optimization of the ipv4 zeroconf protocol. In: DSN. IEEE CS (2003)

    work page 2003

  8. [8]

    In: CA V

    Brim, L., Ceska, M., Drazan, S., Safr´ anek, D.: Exploring parameter space of stochastic biochemical systems using quantitative model c hecking. In: CA V. LNCS, vol. 8044. Springer (2013)

    work page 2013

  9. [9]

    , Paoletti, N.: Efficient synthesis of robust models for stochastic systems

    Calinescu, R., Ceska, M., Gerasimou, S., Kwiatkowska, M. , Paoletti, N.: Efficient synthesis of robust models for stochastic systems. J. Syst. Softw. 143 (2018)

    work page 2018

  10. [10]

    Act a Inf

    Ceska, M., Dannenberg, F., Paoletti, N., Kwiatkowska, M ., Brim, L.: Precise pa- rameter synthesis for stochastic biochemical systems. Act a Inf. 54(6) (2017)

    work page 2017

  11. [11]

    In: FoSSaCS

    Chatterjee, K., Sen, K., Henzinger, T.A.: Model-checki ng omega-regular properties of interval Markov chains. In: FoSSaCS. LNCS, vol. 4962. Spr inger (2008)

    work page 2008

  12. [12]

    Chatzieleftheriou, G., Katsaros, P.: Abstract model re pair for probabilistic systems. Inf. Comput. 259(1) (2018)

    work page 2018

  13. [13]

    In: TASE

    Chen, T., Hahn, E.M., Han, T., Kwiatkowska, M.Z., Qu, H., Zhang, L.: Model repair for Markov decision processes. In: TASE. IEEE (2013)

    work page 2013

  14. [14]

    Reachability in Augmented Interval Markov Chains

    Chonev, V.: Reachability in augmented interval Markov c hains. CoRR abs/1701.02996 (2017)

    work page internal anchor Pith review Pith/arXiv arXiv 2017

  15. [15]

    In: ATV A

    Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.P., Top cu, U.: Synthesis in pMDPs: A tale of 1001 parameters. In: ATV A. LNCS, vol. 11138. Springer (2018)

    work page 2018

  16. [16]

    Ze itschrift fr Wahrschein- lichkeitstheorie und Verwandte Gebiete 10 (1968)

    Daley, D.J.: Stochastically monotone Markov chains. Ze itschrift fr Wahrschein- lichkeitstheorie und Verwandte Gebiete 10 (1968)

    work page 1968

  17. [17]

    In: PAP M-PROBMIV

    D’Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G .: Reachability analysis of probabilistic systems by successive refinements. In: PAP M-PROBMIV. LNCS, vol. 2165. Springer (2001)

    work page 2001

  18. [18]

    In: Proc

    Daws, C.: Symbolic and parametric model checking of disc rete-time Markov chains. In: Proc. of ICTAC. LNCS, vol. 3407. Springer (2004)

    work page 2004

  19. [19]

    In: CA V (1)

    Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk , M., Bruintjes, H., Katoen, J.P., ´Abrah´ am, E.: Prophesy: A probabilistic parameter synthes is tool. In: CA V (1). LNCS, vol. 9206. Springer (2015)

    work page 2015

  20. [20]

    In: CA V (2)

    Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A storm i s coming: A modern probabilistic model checker. In: CA V (2). LNCS, vol. 10427. Springer (2017)

    work page 2017

  21. [21]

    In: ICSE

    Filieri, A., Ghezzi, C., Tamburrelli, G.: Run-time effici ent probabilistic model check- ing. In: ICSE. ACM (2011)

    work page 2011

  22. [22]

    IEEE TSE 42(1) (2016)

    Filieri, A., Tamburrelli, G., Ghezzi, C.: Supporting se lf-adaptation via quantitative verification and sensitivity analysis at run time. IEEE TSE 42(1) (2016)

    work page 2016

  23. [23]

    In: ATV A

    Gainer, P., Hahn, E.M., Schewe, S.: Accelerated model ch ecking of parametric Markov chains. In: ATV A. LNCS, vol. 11138. Springer (2018)

    work page 2018

  24. [24]

    Gouberman, A., Siegle, M., Tati, B.: Markov chains with p erturbed rates to ab- sorption: Theory and application to model repair. Perf. Ev. 130 (2019)

    work page 2019

  25. [25]

    Haddad, S., Monmege, B.: Interval iteration algorithm f or MDPs and IMDPs. Theor. Comput. Sci. 735 (2018)

    work page 2018

  26. [26]

    In: QEST

    Haddad, S., Pekergin, N.: Using stochastic comparison f or efficient model checking of uncertain Markov chains. In: QEST. IEEE CS (2009)

    work page 2009

  27. [27]

    Software Tools for Technology Transfer 13(1) (2010)

    Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reac hability for parametric Markov models. Software Tools for Technology Transfer 13(1) (2010)

    work page 2010

  28. [28]

    In: TACAS

    Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Rui jters, E.: The quanti- tative verification benchmark set. In: TACAS. LNCS, vol. 114 27. Springer (2019) 16

    work page 2019

  29. [29]

    Herman, T.: Probabilistic self-stabilization. Inf. Pr ocess. Lett. 35(2) (1990)

    work page 1990

  30. [30]

    In: GandA LF

    Hutschenreiter, L., Baier, C., Klein, J.: Parametric Ma rkov chains: PCTL com- plexity and fraction-free Gaussian elimination. In: GandA LF. EPTCS, vol. 256 (2017)

    work page 2017

  31. [31]

    I n: QEST

    Jansen, N., Corzilius, F., Volk, M., Wimmer, R., ´Abrah´ am, E., Katoen, J.P., Becker, B.: Accelerating parametric probabilistic verification. I n: QEST. LNCS, vol. 8657. Springer (2014)

    work page 2014

  32. [32]

    In: LICS

    Jonsson, B., Larsen, K.G.: Specification and refinement o f probabilistic processes. In: LICS. IEEE CS (1991)

    work page 1991

  33. [33]

    ACM Comm

    Jovanovic, D., de Moura, L.: Solving non-linear arithme tic. ACM Comm. Computer Algebra 46(3/4) (2012)

    work page 2012

  34. [34]

    Junges, S., Jansen, N., Wimmer, R., Quatmann, T., Winter er, L., Katoen, J.P., Becker, B.: Finite-state controllers of POMDPs using param eter synthesis. In: UAI. AUAI Press (2018)

    work page 2018

  35. [35]

    In: LICS

    Katoen, J.P.: The probabilistic model checking landsca pe. In: LICS. ACM (2016)

    work page 2016

  36. [36]

    In: CA V

    Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Ve rification of probabilis- tic real-time systems. In: CA V. LNCS, vol. 6806. Springer (2 011)

    work page

  37. [37]

    In: QEST

    Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM ben chmark suite. In: QEST. IEEE CS (2012)

    work page 2012

  38. [38]

    Formal Asp

    Kwiatkowska, M.Z., Norman, G., Parker, D.: Probabilist ic verification of Herman’s self-stabilisation algorithm. Formal Asp. Comput. 24(4-6) (2012)

    work page 2012

  39. [39]

    : Evaluating the relia- bility of NAND multiplexing with PRISM

    Norman, G., Parker, D., Kwiatkowska, M.Z., Shukla, S.K. : Evaluating the relia- bility of NAND multiplexing with PRISM. IEEE Trans. on CAD of Integrated Circuits and Systems 24(10) (2005)

    work page 2005

  40. [40]

    Pathak, S., ´Abrah´ am, E., Jansen, N., Tacchella, A., Katoen, J.P.: A gre edy ap- proach for the efficient repair of stochastic models. In: NFM. LNCS, vol. 9058 (2015)

    work page 2015

  41. [41]

    In: ATV A

    Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoe n, J.P.: Parameter syn- thesis for Markov models: Faster than ever. In: ATV A. LNCS, v ol. 9938 (2016)

    work page 2016

  42. [42]

    ACM Trans

    Reiter, M.K., Rubin, A.D.: Crowds: Anonymity for web tra nsactions. ACM Trans. Inf. Syst. Secur. 1(1) (1998)

    work page 1998

  43. [43]

    In: FoSSaCS

    Roux, S.L., P´ erez, G.A.: The complexity of graph-based reductions for reachability in Markov decision processes. In: FoSSaCS. LNCS, vol. 10803 . Springer (2018)

    work page 2018

  44. [44]

    On the Complexity of Reachability in Parametric Markov Decision Processes

    Winkler, T., Junges, S., P´ erez, G.A., Katoen, J.: On the complexity of reachability in parametric markov decision processes. CoRR abs/1904.01503 (2019) 17 M′ M sI A B C λ 1− λ 1 1 Fig. 6. Outline of the construction for the proof of Lem. 2 A Proofs A.1 Proof of Theorem 1 and Lem. 2 Reductions are many-to-one reductions. The proofs use notions from Sect....

    work page internal anchor Pith review Pith/arXiv arXiv 1904

  45. [45]

    For this the induction step holds

    Therefore, Prπ k→ T = Prπ k+1→ T . For this the induction step holds. If πk has two successors, then πk+1∈{ s1, s2}. Let P(πk, s1) = f , and P(πk, s2) = 1− f . As Prπ k→ T↑ℓ,R p , we obtain s2⪯ s1 and f↑R p . 24 ∑ π ∈ Paths k+1 ( ∂ ∂p Pr(π) ) ·Prπ k+1→ T = ∑ π ′∈ Paths k ( ∂ ∂p (f·Pr(π′)) ) ·Prs1→ T + ( ∂ ∂p ((1− f )·Pr(π′)) ) ·Prs2→ T Chain Rule = ∑ π ′∈...

    work page

  46. [46]

    That is, ∀u∈ R

    s1≡ s. That is, ∀u∈ R. Prs→ T (u) = Prs1→ T (u). We obtain for each u∈ R: Prs→ T (u) = ( P(s, s1)·Prs→ T ) (u) + ( (1−P (s, s1))·Prs2→ T ) (u) From which follows:( (1−P (s, s1))·Prs→ T ) (u) = ( (1−P (s, s1))·Prs2→ T ) (u) So,∀u∈ R. Prs→ T (u) = Prs2→ T (u). Therefore, s≡ s2. 27

    work page

  47. [47]

    That is, ∀u∈ R

    s1≺ s. That is, ∀u∈ R. Prs1→ T (u) < Prs→ T (u). We obtain for each u∈ R: Prs→ T (u) < ( P(s, s1)·Prs→ T ) (u) + ( (1−P (s, s1))·Prs2→ T ) (u) From which follows: ( (1−P (s, s1))·Prs→ T ) (u) < ( (1−P (s, s1))·Prs2→ T ) (u) So,∀u∈ R. Prs→ T (u) < Prs2→ T (u). Therefore, s≺ s2

    work page

  48. [48]

    That is, ∀u∈ R

    s≺ s1. That is, ∀u∈ R. Prs→ T (u) < Prs1→ T (u). We obtain for each u∈ R: Prs→ T (u) > ( P(s, s1)·Prs→ T ) (u) + ( (1−P (s, s1))·Prs2→ T ) (u) From which follows: ( (1−P (s, s1))·Prs→ T ) (u) > ( (1−P (s, s1))·Prs2→ T ) (u) So,∀u∈ R. Prs→ T (u) < Prs2→ T (u). Therefore, s≺ s2. ⊓ ⊔ 28 B Full Algorithm We consolidate the algorithm developed in Sect. 4–4.3, ...

    work page