Pith. sign in

REVIEW 1 major objections 4 minor 73 references

Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains

T0 review · 1 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper introduces an approximate bisimulation for continuous-time Markov chains and proves a worst-case bound on how much perturbing transition probabilities and exit rates can change time-bounded reachability probabilities.

desk verdict A genuinely useful generalization of approximate bisimulation for CTMCs, with a correct central reachability bound whose proof currently overextends a cited DTMC theorem; fix that case split and it is ready for serious review. read the letter →

arxiv 2505.15587 v2 pith:XVMHIIMV submitted 2025-05-21 cs.LO

Timm Spork , Christel Baier , Joost-Pieter Katoen , Sascha Klüppelholz , Jakob Piribauer This is my paper · ORCID
classification cs.LO MSC 68Q8568Q8760J27
keywords continuous-timeMarkovchainsapproximateprobabilisticbisimulationtime-boundedreachabilityuniformizationquasi-lumpabilityErlangCTMCreward-boundedperturbationbounds
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper proposes a new equivalence, $(\varepsilon,\delta)$-bisimulation, for comparing states of continuous-time Markov chains when the chain's data are not known exactly. Two states are related when they carry the same labels, their transition probabilities differ by at most an additive $\varepsilon$, and their total exit rates differ by a factor at most $e^\delta$. The central quantitative result is that approximately bisimilar states have time-bounded reachability probabilities that differ by at most $1-e^{-qt(e^\delta(1+\varepsilon)-1)}$, where $q$ is the maximum exit rate and $t$ is the deadline; for $\delta=0$ this bound is tight. This matters because it turns the modelling intuition that small errors in rates or probabilities should not change the answer to a "reach the goal within time $t$" query into a concrete error budget, and the guarantee extends to reward-bounded reachability for nonnegative rewards.

What carries the argument

Uniformization is the bridge from continuous time to discrete time: the CTMC is rewritten as a DTMC in which, at rate $q$, a transition is taken, so time-bounded reachability becomes a Poisson-weighted sum of step-bounded reachabilities. The paper proves that an $(\varepsilon,\delta)$-bisimulation survives uniformization as an $\varepsilon'$-bisimulation with $\varepsilon'=e^\delta(1+\varepsilon)-1$, which lets it import a known step-bounded bound for $\varepsilon$-bisimilar DTMCs. For the rate-only case the workhorse is the Erlang CTMC $E_n$, a chain of $n$ unit-rate states leading to the goal, because conditioning on a fixed path through any CTMC reduces the error computation to a sum of Erlang-chain errors; the probability of each path length is then extracted from a spectral decomposition of the transition probability matrix, using the Jordan canonical form when the matrix is not diagonalizable.

What would settle it

Take a concrete CTMC with an absorbing goal state, choose $q$ as the maximum exit rate, and pick $\varepsilon,\delta$ with $e^\delta(1+\varepsilon)-1>1$; for $(\varepsilon,\delta)$-bisimilar states $s,s'$ compute exactly $|\Pr_s(\diamondsuit_{\le t}g)-\Pr_{s'}(\diamondsuit_{\le t}g)|$ for a range of $t$ and compare with $1-e^{-qt(e^\delta(1+\varepsilon)-1)}$. A single violation would disprove Proposition 14; if no violation is found, the remaining question is whether the proof's use of the discrete-time bound is valid in that parameter range.

Watch

Extended reading notes

Core claim

The central claim is that $\sim_{\varepsilon,\delta}$, the union of all $(\varepsilon,\delta)$-bisimulations, is itself the largest such relation and behaves like a quantitative version of strong probabilistic bisimulation: it is additive in $\varepsilon$ and $\delta$, coincides with strong bisimilarity exactly when $\varepsilon=\delta=0$, and can be computed in polynomial time. Its main quantitative consequence is Proposition 14: if $s\sim_{\varepsilon,\delta}s'$, then the absolute difference between the probabilities of reaching a goal state within time $t$ from $s$ and from $s'$ is at most $1-e^{-qt(e^\delta(1+\varepsilon)-1)}$. For the case where only exit rates differ ($\varepsilon=0$), the paper obtains an exact formula for this difference as a sum over Erlang CTMCs, as well as spectral upper bounds that converge to zero as $t\to\infty$, and it shows how the two-parameter case can be pieced together from the rate-only and probability-only cases by an intermediate chain construction.

Load-bearing premise

The proof of the central bound imports a discrete-time estimate that is only stated for tolerances at most 1, while the paper applies it without restricting the combined tolerance $e^\delta(1+\varepsilon)-1$ or supplying the missing argument for larger values.

Editorial extensions

If this is right

  • If $s\sim_{\varepsilon,\delta}s'$, every time-bounded reachability query answered from $s$ is within the stated exponential bound of the same query answered from $s'$, so model-checking results transfer across perturbed chains.
  • Setting $\varepsilon=0$ gives a way to compute the reachability error between two chains that differ only by a global rate scaling, exactly via Erlang CTMCs and approximately via simple spectral formulas.
  • Because of the decomposition theorem, bounds proved separately for probability-only and rate-only perturbations combine into bounds for simultaneous perturbations.
  • Reward-bounded reachability probabilities in CTMCs with nonnegative rewards inherit the same error bounds after a time-scaling transformation.
  • For a desired accuracy $\theta$ and deadline $t$, Theorem 17 gives explicit ranges of admissible $\varepsilon$ and $\delta$, turning the bound into a design parameter for parameter estimation.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The mixed additive/multiplicative tolerance suggests an error budget in which transition probabilities and exit rates are estimated with different instruments, and the final model-checking error is a function of the two budgets.
  • The spectral bounds indicate that long-horizon robustness is governed by the second-largest eigenvalue modulus of the embedded chain; sharpening the constant $C$ could make these bounds usable as practical anytime bounds.
  • A natural testable extension is an $(\varepsilon,\delta,\mu)$-bisimulation with a reward tolerance, which the paper itself flags as future work; if the same additive/multiplicative pattern carries over, reward-bounded queries would get a three-parameter error budget.
  • The decomposition construction could be used as a quotienting recipe: reduce a model first by rate similarity and then by probability similarity, obtaining intermediate chains whose reachability errors are individually bounded.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

1 major / 4 minor

Summary. The paper introduces (ε,δ)-bisimulation for continuous-time Markov chains, an approximate bisimulation that couples an additive tolerance ε on transition probabilities with a multiplicative tolerance δ on exit rates, expressed via |ln E(s) − ln E(s′)| ≤ δ. It establishes fundamental properties: the largest (ε,δ)-bisimulation exists and is the induced bisimilarity, the relation is additive in ε and δ, it reduces to strong bisimilarity at (0,0), it can be computed in polynomial time, and any (ε,δ)-bisimilarity can be split into (ε,0)- and (0,δ)-bisimilarity. The central quantitative result is Proposition 14, a bound on the difference of time-bounded reachability probabilities of (ε,δ)-bisimilar states, obtained by uniformization and a known DTMC bound. For (0,δ)-bisimilar states the paper gives an exact Erlang-CTMC decomposition, an Erlang-based bound, and spectral bounds based on diagonalization and the Jordan canonical form; these are extended to reward-bounded reachability for nonnegative rewards.

Significance. The notion is natural and addresses a real modeling gap: quasi-lumpability mixes rate and probability perturbations, whereas (ε,δ)-bisimulation separates them, as illustrated in Example 1. The paper provides a solid structural theory (Theorem 7, Theorem 12), explicit and checkable formulas, a tightness example for δ = 0 (Example 16), and numerical illustrations of the bounds. The spectral and Erlang bounds are original. The central reachability bound (Proposition 14) is the main selling point; once its proof is repaired, the results constitute a useful contribution to approximate verification of CTMCs.

major comments (1)
  1. [Section 4, proof of Proposition 14] The proof applies Theorem 4 of [18] to the uniformized DTMC with tolerance τ = e^δ(1+ε)−1 and concludes |Pr_s(♢≤k g) − Pr_s′(♢≤k g)| ≤ 1−(1−τ)^k, then sums with Poisson weights to obtain 1 − e^{−qtτ}. Theorem 4 is stated for ε-bisimilar DTMCs and its bound 1−(1−ε)^k is a valid probability bound only for ε ≤ 1; for τ > 1 the expression exceeds 1 for odd k and is negative for even k, so the inequality is false. Lemma 9 only guarantees s ∼_τ s′ in unif(M,q) without restricting τ, and the paper imposes no restriction on ε, δ, or τ. The claimed bound is nevertheless true for τ ≥ 1 by a short missing case split: if s = g, the unique-label condition forces s′ = g and the difference is 0; otherwise both Pr_s(♢≤t g) and Pr_s′(♢≤t g) are bounded above by 1 − e^{−qt} (reaching g requires at least one transition, and E(s), E(s′) ≤ q), so their difference is at most 1 − e^{−qt} ≤ 1 − e^{−qtτ}. This case split is absent from the proof, leaving a load-bearing gap in the derivation of Proposition 14, which underlies Corollary 15 and Theorem 17.
minor comments (4)
  1. [Section 3.2, Definition 5] The δ-condition would be clearer if it also stated the equivalent multiplicative form e^{−δ} ≤ E(s)/E(s′) ≤ e^δ.
  2. [Section 4, first paragraph] The claim that the reduction to a unique absorbing goal state and a single absorbing fail state is 'w.l.o.g.' is terse: making goal states absorbing or collapsing zero-reachability states changes exit rates and labels, which can affect (ε,δ)-bisimilarity. A short argument that uniquely labeled absorbing states are isolated in any (ε,δ)-bisimulation would make the reduction precise.
  3. [Section 5, Proposition 20] The proof states that a second-derivative computation shows the local maximum is global, but the expression for the second derivative is not given; including it would make the verification easier.
  4. [Appendix A, Proposition 30] In the definition of S^*_{1,hl+j}, the text contains the typographical artifact 'S_{1,hl,+j}' (an extra comma); this should read 'S_{1,hl+j}'.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation; central bounds rest on an external DTMC theorem and explicit Erlang/spectral arguments, with only a non-circular proof gap in Proposition 14.

full rationale

The paper's central quantitative claim, Proposition 14, is obtained by combining Lemma 9 -- which explicitly proves that (ε,δ)-bisimilar states become τ-bisimilar in the uniformized DTMC with τ = e^δ(1+ε)-1 -- with Theorem 4 of [18], an external bound for ε-bisimilar DTMCs. Neither step is equivalent to the target reachability inequality by construction: Lemma 9 is proved in Appendix A from the definitions of the (ε,δ)- and ε-conditions, and Theorem 4 is an independent discrete-time result. No parameter is fitted to make the bound hold. The auxiliary splitting theorem (Theorem 12) uses the weight-function characterization from the authors' prior paper [59], but that lemma is stated in the paper, is parameter-free, and is not used to prove the main reachability bound; at most it supports a secondary refinement at the end of Section 5. The Section 5 bounds for (0,δ)-bisimilar chains are derived from explicit Erlang CTMC computations and spectral decompositions, again with no circular reduction. The only substantive issue is a non-circular correctness gap: the proof of Proposition 14 applies Theorem 4 of [18] at tolerance τ = e^δ(1+ε)-1 without restricting τ ≤ 1, although the intermediate inequality |Pr_s(♢≤k g)-Pr_{s'}(♢≤k g)| ≤ 1-(1-τ)^k is false for τ > 1. The final bound remains true for τ ≥ 1 by a short missing argument (the right-hand side is at least 1-e^{-qt}, and reaching the uniquely labeled absorbing goal requires at least one transition from a non-goal state), but that case split is absent. This is a proof repair, not a circularity, so the circularity score is 0.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

No parameters are fitted to data. The tolerances ε and δ are user inputs, and q, N, C are derived from the model. The central claims rest on standard Markov chain and linear algebra results plus the cited approximate-bisimulation theorems. The main unstated input is the parameter range restriction for the cited DTMC bound.

assumptions (6)
  • standard math Uniformization preserves (ε,δ)-bisimilarity as a τ-bisimulation on the embedded DTMC with τ = e^δ(1+ε)-1 (Lemma 9).
    Proved in the paper using standard uniformization; it is the bridge from CTMC bounds to DTMC bounds.
  • domain assumption The bound of Theorem 4 in [18] applies to ε-bisimulation with tolerance at most 1.
    The paper applies this to τ which may exceed 1; this range restriction is not stated or proven.
  • domain assumption Time-bounded reachability probabilities can be analyzed with a unique absorbing goal state and a unique absorbing fail state without loss of generality.
    Section 4 standard preprocessing for CTMC model checking; it relies on labels and absorption.
  • standard math Weight function characterization of ε-bisimulation (Lemma 3).
    Taken from [59], a prior CONCUR paper by overlapping authors; used in the splitting theorem; independently checkable.
  • standard math Spectral decomposition of the transition probability matrix (diagonalization or Jordan form) is available and the bounds from Watterson [62] hold.
    Section 5 uses standard linear algebra for absorbing Markov chains.
  • domain assumption For transitive (0,δ)-bisimulations, rates can be normalized to a uniform CTMC with the error non-increasing.
    Appendix C.1 gives a construction; if flawed, the refined Section 5 bounds for non-uniform chains would not hold.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains." pith.science (2026). https://pith.science/paper/XVMHIIMV

@misc{pith2026250515587,
  author       = {Pith},
  title        = {Pith review of: Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/XVMHIIMV}},
  note         = {Machine review of arXiv:2505.15587}
}
abstract

We introduce $(\varepsilon, \delta)$-bisimulation, a novel type of approximate probabilistic bisimulation for continuous-time Markov chains. In contrast to related notions, $(\varepsilon, \delta)$-bisimulation allows the use of different tolerances for the transition probabilities ($\varepsilon$, additive) and total exit rates ($\delta$, multiplicative) of states. Fundamental properties of the notion, as well as bounds on the absolute difference of time- and reward-bounded reachability probabilities for $(\varepsilon,\delta)$-bisimilar states, are established.

Figures

Figures reproduced from arXiv: 2505.15587 by the authors.

Figure 1
Figure 1. Three CTMCs where the copies of the states can be related by a [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. The CTMC used in Example 6. Any (ε, δ)-bisimulation on M induces an ε-bisimulation on the embedded DTMC DM, i.e., s ∼M ε,δ t implies s ∼DMε t. Hence, there are weight functions ∆s,t as in Lemma 3 (w.r.t. the probabilities of M) for (ε, δ)-bisimilar states s, t. Example 6. Let ε < 1 2 and δ > 0. In [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. The CTMCs used in Example 13. Example 13. We illustrate the construction of Theorem 12 in [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figures from the paper (5 more)
Figure 4
Figure 4. Figure 4: A CTMC with s ∼ε,0 s ′ and |Prs(♢ ≤t g) − Prs ′ (♢ ≤t g)| = 1 − e −qtε . Proposition 14. For s ∼ε,δ s ′ : |Prs(♢ ≤t g) − Prs ′ (♢ ≤t g)| ≤ 1 − e −qt(e δ (1+ε)−1) . Considering ε = 0 or δ = 0 in Proposition 14 yields the following corollary. Corollary 15. Let s ∼ε,δ s ′…
Figure 5
Figure 5. Figure 5: The Erlang CTMC E4. E4 is illustrated in [PITH_FULL_IMAGE:figures/full_fig_p013_5.png]
Figure 6
Figure 6. Figure 6: A CTMC M with diagonalizable probability matrix (left) and a compar￾ison of the different error bounds for Difft(M). Combining Theorem 22 and Proposition 25 yields a new bound for Difft(M). Proposition 26. Under the conditions of Theorem 22 we have Difft(M) ≤ (n − aP) …
Figure 7
Figure 7. Figure 7: The queue from Example 28 (left) and the bounds and errors for specific [PITH_FULL_IMAGE:figures/full_fig_p016_7.png]
Figure 8
Figure 8. Figure 8: The CTMC M used in the proof of Proposition 11. ≤ P(s ′ , ∼ε,δ(A)) − e −δ + ε · e −δ + 1 = P(s ′ , ∼ε,δ(A)) + e −δ · (ε − 1) + 1 Hence, ∼ε,δ induces a max{1 + e −δ ·(ε − 1), eδ ·(1 + ε) − 1}-bisimulation on the uniformized DTMC unif(M, q). As this maximum is, for any ε…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

73 extracted references · 58 canonical work pages

  1. [18]

    In: Esparza, J., Murawski, A.S

    Bian, G., Abate, A.: On the relationship between bisimulation and trace equiv- alence in an approximate probabilistic context. In: Esparza, J., Murawski, A.S. (eds.) Foundations of Software Science and Computation Structures (FoSSaCS). Lecture Notes in Computer Science (LNCS), vol. 10203, pp. 321–337. Springer, Berlin, Heidelberg (2017).https://doi.org/10...

    work page doi:10.1007/978-3-662-54458-7_19 2017

  2. [1]

    Electronic Notes in Theoretical Computer Science297, 3–25 (2013).https://doi.org/10.1016/j.entcs.2013.12.002, pro- ceedings of the first workshop on Hybrid Autonomous Systems

    Abate, A.: Approximation metrics based on probabilistic bisimulations for general state-space Markov processes: A survey. Electronic Notes in Theoretical Computer Science297, 3–25 (2013).https://doi.org/10.1016/j.entcs.2013.12.002, pro- ceedings of the first workshop on Hybrid Autonomous Systems

    doi:10.1016/j.entcs.2013.12.002 2013

  3. [2]

    In: Kroening, D., Păsăreanu, C.S

    Abate, A., Brim, L., Češka, M., Kwiatkowska, M.: Adaptive aggregation of Markov chains: Quantitative analysis of chemical reaction networks. In: Kroening, D., Păsăreanu, C.S. (eds.) Computer Aided Verification. Lecture Notes in Computer Science (LNCS), vol. 9206, pp. 195–213. Springer International Publishing, Cham (2015).https://doi.org/10.1007/978-3-319...

    work page doi:10.1007/978-3-319-21690-4_12 2015

  4. [3]

    In: van Breugel, F., Kashefi, E., Palamidessi, C., Rutten, J

    Abate, A., Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model check- ing of labelled Markov processes via finite approximate bisimulations. In: van Breugel, F., Kashefi, E., Palamidessi, C., Rutten, J. (eds.) Horizons of the Mind. A Tribute to Prakash Panangaden: Essays Dedicated to Prakash Panangaden on the Occasion of His 60th Birthday, Lectur...

    work page doi:10.1007/978-3-319-068 2014

  5. [4]

    PLoS ONE9(4), e94553 (Apr 2014).https://doi.org/10

    Češka, M., Šafránek, D., Dražan, S., Brim, L.: Robustness Analysis of Stochastic Biochemical Systems. PLoS ONE9(4), e94553 (Apr 2014).https://doi.org/10. 1371/journal.pone.0094553

    work page 2014

  6. [5]

    Aldini, A.: A note on the approximation of weak probabilistic bisimulation (2009)

    work page 2009

  7. [6]

    In: Petri Nets

    Amparore, E.G., Beccuti, M., Donatelli, S.: (Stochastic) model checking in Great- SPN. In: Petri Nets. Lecture Notes in Computer Science (LNCS), vol. 8489, pp. 354–363. Springer (2014).https://doi.org/10.1007/978-3-319-07734-5_19

    work page doi:10.1007/978-3-319-07734-5_19 2014

  8. [7]

    Amparore, E.G., Donatelli, S.: Efficient model checking of the stochastic logic CSLTA. Perform. Evaluation123-124, 1–34 (2018).https://doi.org/10.1016/ j.peva.2018.03.002

    work page 2018

Show all 73 references
  1. [8]

    In: SAFECOMP

    Arnold, F., Belinfante, A., van der Berg, F.I., Guck, D., Stoelinga, M.: DFTCalc: A tool for efficient fault tree analysis. In: SAFECOMP. Lecture Notes in Computer Science (LNCS), vol. 8153, pp. 293–301. Springer (2013).https://doi.org/10. 1007/978-3-642-40793-2_27

    2013

  2. [9]

    ACM Trans

    Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time Markov chains. ACM Trans. Comput. Logic1(1), 162–170 (Jul 2000).https:// doi.org/10.1145/343369.343402

  3. [10]

    In: Alur, R., Henzinger, T.A

    Baier, C.: Polynomial time algorithms for testing probabilistic bisimulation and simulation. In: Alur, R., Henzinger, T.A. (eds.) Computer Aided Verification. Lec- ture Notes in Computer Science (LNCS), vol. 1102, pp. 50–61. Springer, Berlin, Heidelberg (1996).https://doi.org/...

    1996 doi

  4. [11]

    IEEE Trans

    Baier, C., Cloth, L., Haverkort, B.R., Kuntz, M., Siegle, M.: Model checking Markov chains with actions and state labels. IEEE Trans. Software Eng.33(4), 209–224 (2007).https://doi.org/10.1109/TSE.2007.36

    2007 doi

  5. [12]

    In: Montanari, U., Rolim, J.D.P., Welzl, E

    Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: On the logical characterisa- tion of performability properties. In: Montanari, U., Rolim, J.D.P., Welzl, E. (eds.) Automata, Languages and Programming (ICALP 2000). Lecture Notes in Com- puter Science (LNCS), vol. 1853, pp....

    2000 doi

  6. [13]

    IEEE Trans

    Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Software Eng.29(6), 524– 541 (07 2003).https://doi.org/10.1109/TSE.2003.1205180 Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains 23

    2003 arXiv

  7. [14]

    The MIT Press (2008)

    Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press (2008)

    2008

  8. [15]

    Information and Computation200(2), 149–214 (2005)

    Baier, C., Katoen, J.P., Hermanns, H., Wolf, V.: Comparative branching-time se- mantics for Markov chains. Information and Computation200(2), 149–214 (2005). https://doi.org/10.1016/j.ic.2005.03.001

    2005 doi

  9. [16]

    Logical Methods in Computer Science19(1) (2023).https://doi.org/10.46298/lmcs-19(1:22)2023

    Bartoletti, M., Murgia, M., Zunino, R.: Sound approximate and asymptotic prob- abilistic bisimulations for PCTL. Logical Methods in Computer Science19(1) (2023).https://doi.org/10.46298/lmcs-19(1:22)2023

    2023 doi

  10. [17]

    IEEE Transactions on ComputersC-27(6), 540–547 (1978).https://doi.org/ 10.1109/TC.1978.1675145

    Beaudry, M.D.: Performance-related reliability measures for computing systems. IEEE Transactions on ComputersC-27(6), 540–547 (1978).https://doi.org/ 10.1109/TC.1978.1675145

    1978

  11. [19]

    Journal of Applied Probability31(1), 59–75 (1994).https://doi.org/10.2307/3215235

    Buchholz, P.: Exact and ordinary lumpability in finite Markov chains. Journal of Applied Probability31(1), 59–75 (1994).https://doi.org/10.2307/3215235

    1994 doi

  12. [20]

    In: Abate, A., Marin, A

    Cardelli, L., Grosu, R., Larsen, K.G., Tribastone, M., Tschaikowski, M., Vandin, A.: Lumpability for Uncertain Continuous-Time Markov Chains. In: Abate, A., Marin, A. (eds.) Quantitative Evaluation of Systems (QEST 2021), Lecture Notes in Computer Science (LNCS), vol. 12846, p...

    2021 doi

  13. [21]

    IEEE Transactions on Automatic Control68(11), 6557–6572 (Nov 2023).https://doi

    Cardelli,L.,Grosu,R.,Larsen,K.G.,Tribastone,M.,Tschaikowski,M.,Vandin,A.: Algorithmic Minimization of Uncertain Continuous-Time Markov Chains. IEEE Transactions on Automatic Control68(11), 6557–6572 (Nov 2023).https://doi. org/10.1109/TAC.2023.3244093

    2023

  14. [22]

    In: 24th IEEE Symposium on Logic In Computer Science (LICS)

    Chen, T., Han, T., Katoen, J., Mereacre, A.: Quantitative model checking of continuous-time Markov chains against timed automata specifications. In: 24th IEEE Symposium on Logic In Computer Science (LICS). pp. 309–318. IEEE Com- puter Society (2009).https://doi.org/10.1109/LIC...

    2009 doi

  15. [23]

    In: Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LiCS)

    Desharnais, J., Edalat, A., Panangaden, P.: A logical characterization of bisim- ulation for labeled Markov processes. In: Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LiCS). pp. 478–487 (1998). https://doi.org/10.1109/LICS.1998.705681

    1998

  16. [24]

    Information and Computation179(2), 163–193 (2002).https://doi.org/ 10.1006/inco.2001.2962

    Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled Markov pro- cesses. Information and Computation179(2), 163–193 (2002).https://doi.org/ 10.1006/inco.2001.2962

    2002

  17. [25]

    In: Fifth International Conference on Quantitative Evaluation of Systems (QEST 2008)

    Desharnais, J., Laviolette, F., Tracol, M.: Approximate analysis of probabilistic processes: Logic, simulation and games. In: Fifth International Conference on Quantitative Evaluation of Systems (QEST 2008). pp. 264–273 (QEST 2008). https://doi.org/10.1109/QEST.2008.42

    2008 doi

  18. [26]

    In: Tauman Kalai, Y

    Dey, P., Kannan, R., Ryder, N., Srivastava, N.: Bit Complexity of Jordan Normal Form and Polynomial Spectral Factorization. In: Tauman Kalai, Y. (ed.) 14th Innovations in Theoretical Computer Science Conference (ITCS 2023). Leibniz International Proceedings in Informatics (LIP...

    2023 doi

  19. [27]

    D’Innocenzo, A., Abate, A., Katoen, J.P.: Robust PCTL model checking. In: Pro- ceedings of the 15th ACM International Conference on Hybrid Systems: Computa- tionandControl(HSCC2012).pp.275–286.AssociationforComputingMachinery, New York, NY, USA (2012).https://doi.org/10.1145/2...

    2012

  20. [28]

    The Post Office Electrical Engineer’s Jour- nal pp

    Erlang, A.K.: Solution to some problems of the theory of probabilities of signifi- cance in automatic telephone exchange. The Post Office Electrical Engineer’s Jour- nal pp. 189–197 (1917)

    1917

  21. [29]

    Performance Evaluation20(1), 223–243 (1994).https://doi.org/10.1016/ 0166-5316(94)90015-9

    Franceschinis, G., Muntz, R.R.: Bounds for quasi-lumpable Markov chains. Performance Evaluation20(1), 223–243 (1994).https://doi.org/10.1016/ 0166-5316(94)90015-9

    1994

  22. [30]

    IEEE Transactions on Software Engi- neering20(7), 516–525 (1994).https://doi.org/10.1109/32.297940

    Franceschinis, G., Muntz, R.R.: Computing bounds for the performance indices of quasi-lumpable stochastic well-formed nets. IEEE Transactions on Software Engi- neering20(7), 516–525 (1994).https://doi.org/10.1109/32.297940

    1994 doi

  23. [31]

    In: Remke, A., Stoelinga, M

    Gouberman, A., Siegle, M.: Markov reward models and Markov decision processes in discrete and continuous time: Performance evaluation and optimization. In: Remke, A., Stoelinga, M. (eds.) Stochastic Model Checking. Rigorous Depend- ability Analysis Using Model Checking Techniq...

    2014 doi

  24. [32]

    Com- puters & Operations Research4(1), 47–53 (1977).https://doi.org/10.1016/ 0305-0548(77)90007-7

    Grassmann, W.K.: Transient solutions in Markovian queueing systems. Com- puters & Operations Research4(1), 47–53 (1977).https://doi.org/10.1016/ 0305-0548(77)90007-7

    1977

  25. [33]

    In: 2021 American Control Conference (ACC)

    Haesaert, S., Nilsson, P., Soudjani, S.: Formal multi-objective synthesis of continuous-state MDPs. In: 2021 American Control Conference (ACC). pp. 3428– 3433 (2021).https://doi.org/10.23919/ACC50511.2021.9482873

    2021

  26. [34]

    International Journal on Software Tools for Technology Transfer (STTT)24, 589–610 (2022).https://doi.org/10.1007/s10009-021-00633-z

    Hensel,C.,Junges,S.,Katoen,J.,Quatmann,T.,Volk,M.:Theprobabilisticmodel checker STORM. International Journal on Software Tools for Technology Transfer (STTT)24, 589–610 (2022).https://doi.org/10.1007/s10009-021-00633-z

    2022 doi

  27. [35]

    Scandi- navian Actuarial Journal1953(sup1), 87–91 (1953).https://doi.org/10.1080/ 03461238.1953.10419459

    Jensen, A.: Markoff chains as an aid in the study of Markoff processes. Scandi- navian Actuarial Journal1953(sup1), 87–91 (1953).https://doi.org/10.1080/ 03461238.1953.10419459

    1953

  28. [36]

    Undergraduate Texts in Mathe- matics (UTM), Springer New York (1976)

    Kemeny, J.G., Snell, J.L.: Finite Markov Chains. Undergraduate Texts in Mathe- matics (UTM), Springer New York (1976)

    1976

  29. [37]

    In: Bojańczy, M., Chekuri, C

    Kiefer, S., Tang, Q.: Approximate Bisimulation Minimisation. In: Bojańczy, M., Chekuri, C. (eds.) 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz Inter- national Proceedings in Informatics (LIPIcs), vol...

    2021 doi

  30. [38]

    Mathematische Annalen104, 415–458 (1931).https://doi.org/10

    Kolmogorov, A.N.: Über die analytischen Methoden in der Wahrscheinlichkeit- srechnung. Mathematische Annalen104, 415–458 (1931).https://doi.org/10. 1007/BF01457949

    1931

  31. [39]

    Springer Texts in Statistics (STS), Springer New York (2010).https://doi.org/ 10.1007/978-1-4419-1772-0

    Kulkarni, V.G.: Introduction to Modeling and Analysis of Stochastic Systems. Springer Texts in Statistics (STS), Springer New York (2010).https://doi.org/ 10.1007/978-1-4419-1772-0

    2010 doi

  32. [40]

    In: Gopalakrishnan, G., Qadeer, S

    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilis- tic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Proc. 23rd In- ternational Conference on Computer Aided Verification (CAV’11). Lecture Notes in Computer Science (LNCS), vol. 6806, ...

    2011 doi

  33. [41]

    Kwiatkowska,M.Z.,Thachuk,C.:Probabilisticmodelcheckingforbiology.In:Soft- ware Systems Safety, NATO Science for Peace and Security Series, D: Information and Communication Security, vol. 36, pp. 165–189. IOS Press (2014) Approximate Probabilistic Bisimulation for Continuous-Ti...

    2014

  34. [42]

    Information and Computation94(1), 1–28 (1991).https://doi.org/10.1016/0890-5401(91) 90030-6

    Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Information and Computation94(1), 1–28 (1991).https://doi.org/10.1016/0890-5401(91) 90030-6

    1991 doi

  35. [43]

    Journal of Applied Probability61(4), 1278–1300 (2024).https://doi.org/ 10.1017/jpr.2024.20

    Lin, N., Liu, Y.: Perturbation analysis for continuous-time Markov chains in a weak sense. Journal of Applied Probability61(4), 1278–1300 (2024).https://doi.org/ 10.1017/jpr.2024.20

    2024 doi

  36. [44]

    Sci- ence China Mathematics58(2), 2633–2642 (2015).https://doi.org/10.1007/ s11425-015-5019-z

    Liu, Y.: Perturbation analysis for continuous-time Markov chains. Sci- ence China Mathematics58(2), 2633–2642 (2015).https://doi.org/10.1007/ s11425-015-5019-z

    2015

  37. [45]

    Advances in Applied Probability50(2), 645–669 (2018).https://doi.org/10.1017/apr.2018.28

    Liu, Y., Li, W.: Error bounds for augmented truncation approximations of Markov chains via the perturbation method. Advances in Applied Probability50(2), 645–669 (2018).https://doi.org/10.1017/apr.2018.28

    2018 doi

  38. [46]

    Madsen, C., Zhang, Z., Roehner, N., Winstead, C., Myers, C.J.: Stochastic model checking of genetic circuits. ACM J. Emerg. Technol. Comput. Syst.11(3), 23:1– 23:21 (2014).https://doi.org/10.1145/2644817

    2014 doi

  39. [47]

    Performance Evaluation7(3), 175–194 (1987).https://doi.org/10.1016/ 0166-5316(87)90039-3

    Maire, R.A., Reibman, A.L., Trivedi, K.S.: Transient analysis of acyclic Markov chains. Performance Evaluation7(3), 175–194 (1987).https://doi.org/10.1016/ 0166-5316(87)90039-3

    1987

  40. [48]

    In: André, É., Stoelinga, M.(eds.)FormalModelingandAnalysisofTimedSystems(FORMATS)2019.Lec- ture Notes in Computer Science (LNCS), vol

    Marin, A., Piazza, C., Rossi, S.: Proportional lumpability. In: André, É., Stoelinga, M.(eds.)FormalModelingandAnalysisofTimedSystems(FORMATS)2019.Lec- ture Notes in Computer Science (LNCS), vol. 11750, pp. 265–281. Springer Interna- tional Publishing, Cham (2019).https://doi....

    2019 doi

  41. [49]

    Acta Inf.59(2–3), 211–244 (Jun 2022).https://doi.org/10.1007/ s00236-021-00404-y

    Marin, A., Piazza, C., Rossi, S.: Proportional lumpability and proportional bisimilarity. Acta Inf.59(2–3), 211–244 (Jun 2022).https://doi.org/10.1007/ s00236-021-00404-y

    2022

  42. [50]

    Society for Industrial and Applied Mathematics, Philadelphia, PA (2000)

    Meyer, C.D.: Matrix Analysis and Applied Linear Algebra. Society for Industrial and Applied Mathematics, Philadelphia, PA (2000)

    2000

  43. [51]

    Journal of Applied Probability42(4), 1003–1014 (2005)

    Mitrophanov, A.Y.: Sensitivity and convergence of uniformly ergodic Markov chains. Journal of Applied Probability42(4), 1003–1014 (2005)

    2005

  44. [52]

    Mathematics12(11) (2024).https://doi.org/10

    Mitrophanov, A.Y.: The arsenal of perturbation bounds for finite continuous-time Markov chains: A perspective. Mathematics12(11) (2024).https://doi.org/10. 3390/math12111608

    2024

  45. [53]

    SIAM Review45(1), 3–49 (Jan 2003).https: //doi.org/10.1137/S00361445024180

    Moler, C., Van Loan, C.: Nineteen Dubious Ways to Compute the Exponential of a Matrix, Twenty-Five Years Later. SIAM Review45(1), 3–49 (Jan 2003).https: //doi.org/10.1137/S00361445024180

    2003 doi

  46. [54]

    Pan,V.Y.,Chen,Z.Q.:Thecomplexityofthematrixeigenproblem.In:Proceedings of the thirty-first annual ACM symposium on Theory of Computing. pp. 507–

  47. [55]

    In: Abate, A., Marin, A

    Piazza, C., Rossi, S.: Reasoning about proportional lumpability. In: Abate, A., Marin, A. (eds.) Quantitative Evaluation of Systems (QEST 2021). Lecture Notes in Computer Science (LNCS), vol. 12846, pp. 372–390. Springer International Pub- lishing, Cham (2021).https://doi.org/...

    2021 doi

  48. [56]

    https://doi.org/10.3390/a17040159

    Piazza, C., Rossi, S., Smuseva, D.: Efficient algorithm for proportional lumpability anditsapplicationtoselfishmininginpublicblockchains.Algorithms17(4)(2024). https://doi.org/10.3390/a17040159

    2024 doi

  49. [57]

    In: Jon- sson, B., Parrow, J

    Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jon- sson, B., Parrow, J. (eds.) CONCUR ’94: Concurrency Theory. Lecture Notes in Computer Science (LNCS), vol. 836, pp. 481–496. Springer, Berlin, Heidelberg (1994).https://doi.org/10.1007/978-3...

    1994 doi

  50. [58]

    SIAM Journal on Numerical Analysis 37(4), 1120–1137 (2000).https://doi.org/10.1137/S0036142998337235

    Shardlow, T., Stuart, A.M.: A perturbation theory for ergodic Markov chains and application to numerical approximations. SIAM Journal on Numerical Analysis 37(4), 1120–1137 (2000).https://doi.org/10.1137/S0036142998337235

    2000 doi

  51. [59]

    In: Majumdar, R., Silva, A

    Spork, T., Baier, C., Katoen, J.P., Piribauer, J., Quatmann, T.: A Spectrum of Approximate Probabilistic Bisimulations. In: Majumdar, R., Silva, A. (eds.) 35th International Conference on Concurrency Theory (CONCUR 2024). Leib- niz International Proceedings in Informatics (LIP...

    2024 doi

  52. [60]

    In: Massink, M., Norman, G

    Tracol, M., Desharnais, J., Zhioua, A.: Computing distances between probabilis- tic automata. In: Massink, M., Norman, G. (eds.) Proceedings Ninth Work- shop on Quantitative Aspects of Programming Languages (QAPL 2011), Saar- brücken, Germany, April 1-3, 2011. EPTCS, vol. 57, ...

    2011 doi

  53. [61]

    IEEE Trans

    Volk,M.,Junges,S.,Katoen,J.:Fastdynamicfaulttreeanalysisbymodelchecking techniques. IEEE Trans. Ind. Informatics14(1), 370–379 (2018).https://doi. org/10.1109/TII.2017.2710316

    2018

  54. [62]

    The Annals of Mathematical Statistics32(3), 716–729 (Sep 1961).https://doi.org/ 10.1214/aoms/1177704967

    Watterson, G.A.: Markov Chains with Absorbing States: A Genetic Example. The Annals of Mathematical Statistics32(3), 716–729 (Sep 1961).https://doi.org/ 10.1214/aoms/1177704967

    1961

  55. [63]

    Zhang, L., Jansen, D.N., Nielson, F., Hermanns, H.: Automata-based CSL model checking. Log. Methods Comput. Sci.8(2) (2011).https://doi.org/10.1007/ 978-3-642-22012-8_21 Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains 27 A Proofs of Section 3 Lemma 38....

    2011

  56. [65]

    3.s∼s ′ iffs∼ 0,0 s′

    Ifs∼ ε1,δ1 s′ ands ′ ∼ε2,δ2 s′′ thens∼ ε1+ε2,δ1+δ2 s′′. 3.s∼s ′ iffs∼ 0,0 s′. Proof.1. We start by showing that∼ ε,δ is itself an(ε, δ)-bisimulation. To this end we first observe that, as a countable union of symmetric and reflexive relations,∼ ε,δ is itself both reflexive and...

  57. [66]

    Define R={(x, z)∈S×S| ∃y∈S:x∼ ε1,δ1 yandy∼ ε2,δ2 z}

    It is clear thatL(s) =L(s ′) =L(s ′′). Define R={(x, z)∈S×S| ∃y∈S:x∼ ε1,δ1 yandy∼ ε2,δ2 z}. Then it follows from the respective properties of∼ε1,δ1 and∼ ε2,δ2 thatRis a symmetric and reflexive relation, and it holds that(s, s′′)∈R. Moreover, 28 T. Spork et al. for every pair o...

  58. [67]

    To see this, lets∼0,0 s′ and s′ ∼0,0 s′′

    We first observe that∼0,0 is an equivalence. To see this, lets∼0,0 s′ and s′ ∼0,0 s′′. By the additivity of(ε, δ)-bisimulations proved in item 2 it fol- lows thats∼ 0+0,0+0 s′′, i.e.,s∼ 0,0 s′′, so∼ 0,0 is transitive. As any(ε, δ)- bisimulation is reflexive and symmetric by de...

  59. [68]

    Theorem 17.Letθ∈[0,1),t >0, andq= max p∈S E(p)

    yields the desired bound via |Prs(♢≤tg)−Pr s′(♢≤tg)|=e −q·t · ∞X k=0 (q·t) k k! ·( P k s,g − P k s′,g) =e −q·t · ∞X k=0 (q·t) k k! ·(Pr s(♢≤kg)−Pr s′(♢≤kg)) ≤e −q·t · ∞X k=0 (q·t) k k! · |Prs(♢≤kg)−Pr s′(♢≤kg)| ≤e −q·t · ∞X k=0 (q·t) k k! ·(1−(1−(e δ ·(1 +ε)−1)) k) =e −q·t · ∞...

  60. [69]

    EachJi with corresponding eigenvalueλ i is anr i ×r i matrix of the form Ji =   λi 1 0 0

    J qJ   .(7) whereq J is the total number of Jordan blocks ofJ. EachJi with corresponding eigenvalueλ i is anr i ×r i matrix of the form Ji =   λi 1 0 0. . . 0λ i 1 0

  61. [70]

    0λ i   . The probability to reachgafter exactlyN+ 1discrete time steps is pN+1 =1 sinit ·(P N+1 −P N )·1 ⊤ g =1 sinit · ·((SJS−1)N+1 −(SJS −1)N )·1 ⊤ g =1 sinit ·S·(J N+1 −J N )·S −1 ·1 ⊤ g = S1,1 S1,2 . . .S1,n ·(J N+1 −J N )·   S−1 1,n S−1 2,n ... S−1 n,n   ...

  62. [71]

    Spork et al

    0 0λ N i   ,(9) yielding JN+1 i −J N i =J N i ·(J i −I ri ) 54 T. Spork et al. =   λN i (λi −1)λ N−1 i (λi N+1 1 − N 1 )λ N−2 i (λi N+1 2 − N 2 ). . . λ N−r i+1 i (λi N+1 ri−1 − N ri−1 ) 0λ N i (λi −1)λ N−1 i (λi N+1 1 − N 1 ). . . λ N−r i+2 i (λi N+1 ri−...

  63. [72]

    0λ N i (λi −1)λ N−1 i (λi N+1 1 − N 1 )

  64. [73]

    0 0λ N i (λi −1)   whereI ri is ther i ×r i identity matrix. When combining the derived form of JN+1 i −J N i with Equation (8) and carrying out the multiplication, we obtain pN+1 = qJX l=2 rlX j=1 jX k=1 S1,k+hl ·S −1 j+hl,n ·λ N+k−j l · λl · N+ 1 j−k − N j−k = qJX...

  65. [516]

    ACM, Atlanta Georgia USA (May 1999).https://doi.org/10.1145/301250. 301389

    1999 doi

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.