Pith. sign in

REVIEW 1 major objections 4 minor 1 cited by

Robust Probabilistic Bisimilarity for Labelled 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 ↗ Review JSON

Pith's one-line read A strengthening of probabilistic bisimilarity—robust bisimilarity—guarantees that the bisimilarity distance between two states is continuous under any sufficiently small perturbation of the transition probabilities.

desk verdict Robust probabilistic bisimilarity is a genuinely new and useful notion, but the appendix proof of the continuity theorem has a fixable gap that must be repaired before the paper is accepted. read the letter →

arxiv 2505.15290 v2 pith:72S33RCR submitted 2025-05-21 cs.LO cs.FL

Syyeda Zainab Fatmi , Stefan Kiefer , David Parker , Franck van Breugel This is my paper · ORCID
classification cs.LOcs.FL MSC 68Q6068Q87
keywords labelledMarkovchainsrobustprobabilisticbisimilaritydistancebehaviouralpseudometriccontinuityunderperturbationscouplingpoliciespartitionrefinement
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 introduces robust probabilistic bisimilarity for finite labelled Markov chains, a strengthening of ordinary probabilistic bisimilarity designed to fix a practical weakness: the usual equivalence can collapse states whose behaviour diverges completely under arbitrarily small perturbations of the transition probabilities. The central result, Theorem 2, proves that if two states are robustly bisimilar in the proposed sense, then the probabilistic bisimilarity distance between them converges to zero along every sequence of perturbed transition functions converging to the original one. This matters because transition probabilities in applications are usually estimates from data, so an equivalence that remains meaningful under noise is safer to use for state-space minimization. The paper also gives a polynomial-time algorithm that computes the greatest robust bisimulation, running in O(n⁶) where n is the number of states, and reports experiments on standard benchmark models showing it is feasible in practice.

What carries the argument

The load-bearing identity is the policy characterization of the bisimilarity distance, δτ(s,t) = min_{P∈P_τ} γ_P(s,t) (Proposition 2, drawn from [2, Theorem 10.15] and [8, Theorem 8]), where γ_P(s,t) is the probability that the pair (s,t) ever reaches the set S²_1 of differently labelled state pairs in the product chain driven by the coupling policy P. Robust bisimilarity repurposes the same product-chain machinery: instead of reaching S²_1, a robust policy must reach the diagonal S²_Δ with probability 1. The proof of Theorem 2 then runs a matrix-norm induction over the closed communication classes of the robust policy's product chain, showing that after a small perturbation of τ there is a policy P_n whose reaching probabilities γ_{P_n}(u,v) converge to γ_P(u,v) = 0 on every reachable class; this yields upper semi-continuity, and lower semi-continuity (Proposition 1) completes continuity.

What would settle it

Find a finite labelled Markov chain with a bisimilar pair (s,t) that admits a policy reaching the diagonal with probability 1, together with a sequence of transition functions τ_n → τ for which δ_{τ_n}(s,t) does not converge to 0; that would refute Theorem 2. Conversely, a bisimilar pair whose distance function is continuous at τ but for which no policy reaches the diagonal with probability 1 would refute the paper's necessity conjecture.

Watch

Extended reading notes

Core claim

Robust bisimilarity is defined via coupling policies on the product of the chain with itself: states s and t are robustly bisimilar (s ≃ t) if there is a policy P respecting the transition function τ such that the pair (s,t) reaches the diagonal S²_Δ = {(s,s) | s ∈ S} with probability 1 in the induced product Markov chain. Theorem 2 establishes the headline property: whenever s ≃ t, the function τ ↦ δ_τ(s,t) is continuous at τ, meaning lim_{n→∞} δ_{τ_n}(s,t) = 0 for any sequence of transition functions converging to τ. Since Proposition 1 gives lower semi-continuity of the distance for all pairs, the substance of the theorem is upper semi-continuity at robustly bisimilar pairs, proved by showing that the minimal reaching probabilities γ_{P_n} to the different-label set S²_1 along near-optimal policies converge to γ_P = 0. Robust bisimilarity is itself a bisimulation, hence implies ordinary bisimilarity, and the relation ≃ is the greatest fixed point of a refinement operator combining Filter, Prune, and Bisim; Algorithm 1 computes it in polynomial time.

Load-bearing premise

The continuity proof rests on the characterization of the bisimilarity distance as the minimum over coupling policies of the probability of reaching a differently-labelled pair; if that characterization fails for any class of chains, the argument that perturbed distances stay small collapses.

Editorial extensions

If this is right

  • If two states are robustly bisimilar, merging them during model minimization remains safe even when the transition probabilities are only known approximately.
  • Robust bisimilarity implies ordinary bisimilarity, so the new relation can only split, never merge, the equivalence classes of standard bisimilarity.
  • The O(n⁶) algorithm makes robustness checks feasible on models with hundreds of thousands of states, as demonstrated on standard benchmarks.
  • The paper's conjecture—that for bisimilar states robust bisimilarity is also necessary for continuity—would give a complete characterization of exactly when the distance function is continuous at a bisimilar pair.

Reading between the lines

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

  • The same recipe—demand that a coupling policy reach a designated target set with probability 1—can define robust analogues of other behavioural relations, such as simulation preorders or lumpability, yielding a uniform theory of perturbation-stable equivalences.
  • One can define a robustness degree of a bisimilar pair as the infimum over policies of the probability of not reaching the diagonal; the continuity theorem suggests this quantity controls the size of the discontinuity jump under perturbations.
  • Because the theorem permits perturbations that add new transitions (not just repricing existing ones), the result is stronger than earlier continuity statements that restricted the deformation of the chain; testing the necessity conjecture would pinpoint whether adding transitions is the only source of the discontinuity phenomenon.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

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 robust probabilistic bisimilarity for finite labelled Markov chains. Two states are robustly bisimilar if there exists a policy P for the transition function τ such that the induced product Markov chain reaches the diagonal S2_Δ with probability 1. The authors prove that this relation is a bisimulation (Lemma 1), hence implies ordinary probabilistic bisimilarity, and that it is the greatest robust bisimulation. Their main theoretical result is Theorem 2: for robustly bisimilar states s,t, the probabilistic bisimilarity distance δ_τ(s,t) is continuous at τ, i.e. for every sequence τ_n converging to τ, δ_{τ_n}(s,t) converges to 0. The proof combines a lower-semicontinuity result (Proposition 1) with an upper-semicontinuity argument (Lemma 3) using matrix norms. The paper also presents an algorithm for computing robust bisimilarity as the greatest fixed point of a Refine operator built from Filter, Prune, and Bisim, proves correctness and an O(n^6) time bound, and reports experiments on QVBS and jpf-probabilistic benchmarks. The authors state as a conjecture that robust bisimilarity is also necessary for continuity for bisimilar states.

Significance. If the main results hold, the paper makes a useful contribution: it identifies a bisimulation-based notion that is robust to small perturbations of transition probabilities, addressing a known deficiency of probabilistic bisimilarity. The central continuity theorem is nontrivial, and the appendix supplies a detailed matrix-norm proof rather than a hand-waved argument. The algorithm is accompanied by a loop-invariant correctness proof, a polynomial-time complexity bound, and an implementation in PRISM tested on a broad set of benchmarks, which is a concrete practical strength. The paper is also honest about the parts that are conjectured rather than proven, in particular the conjectured necessity of robust bisimilarity for continuity. The main weakness is a genuine gap in the written proof of Lemma 3 that is load-bearing for Theorem 2; it appears to be a fixable definitional error, but as written the central continuity theorem is not fully established.

major comments (1)
  1. [Appendix G, Lemma 3] In the induction step of Lemma 3, B is defined as the set of state pairs of all communication classes reachable from C by a path of length greater than 1, and A is defined as (S×S)\ (B∪C). The proof then asserts that support(P(u,v))⊆B∪C for all (u,v)∈C, and hence P^A=0. This assertion does not follow from the given definition: a direct successor class D of C is reachable by a path of length 1, so D is not included in B, and P may assign positive mass to pairs in D⊆A. Consequently the displayed decomposition of γ_{P_n}^C and the subsequent bound on ∥γ_{P_n}^C−γ_P^C∥ are not justified as written, and the inductive proof of (4) is incomplete. This is load-bearing because Lemma 3 supplies the upper-semicontinuity half of Theorem 2. The gap appears repairable by redefining B as the state pairs of all communication classes reachable from C by a path of positive length, so that the induction hypothesis applies to every successor class; I would like the proof corrected in this way and the surrounding text updated accordingly.
minor comments (4)
  1. [Appendix H, Figure 6] The caption of Figure 6 says 'Illustration of the proof of Proposition 1', but the figure illustrates the proof of Lemma 1; the reference should be fixed.
  2. [Proposition 27] The complexity proof says 'Refine begins with ∼, containing at most n^2 pairs of states' but Algorithm 1 begins with R=∼; the wording should say the algorithm rather than the function Refine.
  3. [Section 6.3] The sentence 'in all benchmarks we have checked, we have observed that the distance between pairs of states that are not robustly bisimilar is discontinuous' reports an empirical pattern; the text should make explicit that this is an experimental observation and not a proven statement, alongside the conjecture in Section 7.
  4. [Abstract] In the abstract and introduction, the phrase 'alackofrobustness' appears to be missing spaces ('a lack of robustness'); this typesetting issue should be corrected.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: robust bisimilarity is defined independently of the continuity claim, and the proof relies on external, non-fitted theorems; self-citations are benign pointers.

full rationale

The paper's central claim (Theorem 2) is not circular. Robust bisimilarity (Definition 5) is defined independently of the target continuity statement, namely as the existence of a policy P in P such that (s,t) reaches S2_Delta with probability 1 in the induced product chain; it is not defined in terms of delta_tau or of continuity. The link between this definition and the distance delta_tau is Proposition 2 (delta_tau = min_P gamma_P), which is imported from Baier and Katoen [2, Theorem 10.15] and Chen, van Breugel and Worrell [8, Theorem 8]. Although one current coauthor appears on [8], that theorem is a standard external characterization of the pre-existing bisimilarity distance, is not fitted to the examples, and does not assume the target result. The self-citation to the CAV version [20] is only a pointer to the extended-version relationship, not a load-bearing argument. No parameter is fitted and later renamed a prediction, and no uniqueness theorem is imported from the authors' own prior work to force the definition. One written gap does exist in the proof of Lemma 3: B is defined as classes reachable via paths of length greater than 1, so the assertion support(P(u,v)) subset B union C, and hence P^A = 0, is not justified as written; this is a fixable proof error (redefine B as positive-length reachability) and is a correctness risk, not a circularity. Overall, the derivation chain is self-contained with respect to external benchmarks and does not reduce to its own inputs.

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

The paper introduces no free parameters and no invented physical entities. It builds on standard mathematical foundations: finite labelled Markov chains, couplings, and the known fixed-point characterization of the bisimilarity distance. It relies on two external theorems: the policy characterization of the bisimilarity distance (Proposition 2, from [2,8]) and the quantitative mu-calculus characterization (from [7]). The perturbation model is a domain assumption: changes to transition probabilities are measured in the sup norm and may add transitions.

assumptions (5)
  • domain assumption Finite labelled Markov chain with at least two labels: S finite, τ: S → D(S), ℓ: S → L with |ℓ(S)| ≥ 2.
    The paper fixes such a chain in Section 2 and all definitions, proofs, and the algorithm operate in this finite setting.
  • standard math δ_τ(s,t) = min_{P∈P_τ} γ_P(s,t) (Proposition 2), the policy characterization of the bisimilarity distance.
    Stated as Proposition 2, proof follows from Baier and Katoen [2, Theorem 10.15] and Chen, van Breugel, Worrell [8, Theorem 8]; used heavily in the proof of Theorem 2.
  • standard math The bisimilarity distance is the least fixed point of Δ_τ (Definition 2) and is characterized by quantitative mu-calculus formulas.
    Definition 2 and the characterization from [7, Equation 2.3] are used in the examples, not in the core proof.
  • domain assumption Perturbations are modelled in the sup metric d_F on transition functions, allowing arbitrary changes including added transitions.
    Section 3 states the authors conservatively assume the transition function can be varied arbitrarily; the continuity result is with respect to this metric.
  • domain assumption The input to the algorithm includes the bisimilarity relation ∼, computable in polynomial time via partition refinement (Derisavi et al.).
    Algorithm 1 takes ∼ as input from the standard bisimulation algorithm; Proposition 24 uses Derisavi's method.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Robust Probabilistic Bisimilarity for Labelled Markov Chains." pith.science (2026). https://pith.science/paper/72S33RCR

@misc{pith2026250515290,
  author       = {Pith},
  title        = {Pith review of: Robust Probabilistic Bisimilarity for Labelled Markov Chains},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/72S33RCR}},
  note         = {Machine review of arXiv:2505.15290}
}
read the original abstract

Despite its prevalence, probabilistic bisimilarity suffers from a lack of robustness under minuscule perturbations of the transition probabilities. This can lead to discontinuities in the probabilistic bisimilarity distance function, undermining its reliability in practical applications where transition probabilities are often approximations derived from experimental data. Motivated by this limitation, we introduce the notion of robust probabilistic bisimilarity for labelled Markov chains, which ensures the continuity of the probabilistic bisimilarity distance function. We also propose an efficient algorithm for computing robust probabilistic bisimilarity and show that it performs well in practice, as evidenced by our experimental results.

Figures

Figures reproduced from arXiv: 2505.15290 by the authors.

Figure 1
Figure 1. Various examples featuring fair and biased coins. States labeled with [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. The Markov chain ⟨S × S, P⟩ induced by the policy P such that (h0, h1) reaches S 2 1 with probability 1 5 [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. The Markov chain ⟨S × S, P⟩ induced by the policy P such that (h0, h1) reaches S 2 ∆ with probability 1. perturbation. It follows that the probability of all paths of length at most k from (s, t) to S 2 ∆ remains at least (1 − x) · (1 − x) ≥ 1 − 2x after the perturbation. In the Appendix, we provide a different, formal proof using matrix norms. There we construct a graph consisting of the closed communication classe… view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Graph visualization of the relations A and B used in the proof of Propo￾sition 5. Note that Algorithm 1 is not a typical fixed point iteration, since we do not know whether Refine is monotone. Algorithm 2: Refine Input: A set R ∈ [S 2 ∆, ∼]B Output: Refine(R) 1 R ← Fil…
Figure 5
Figure 5. Figure 5: Illustration of the proof of Proposition 7. [PITH_FULL_IMAGE:figures/full_fig_p014_5.png]
Figure 6
Figure 6. Figure 6: Thus, we have (xm, zm) ∈ C and xm = zm, that is, (xm, zm) ∈ C ∩S 2 ∆, as required. ⊓⊔ ≃ ≃ s ≃ t ≃ u x1 y1 z1 xn ≃ zn xm [PITH_FULL_IMAGE:figures/full_fig_p036_6.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Clustered Attractor Manifolds and Dynamical Condensation in Self-Attention

    cond-mat.dis-nn 2026-08 conditional novelty 6.0 of 10

    For normalized self-attention in the d ~ N limit, the overlap gap controls a manifold of clustered fixed points and a finite-sharpness dynamical attention-condensation transition.

Reference graph

Works this paper leans on

45 extracted references · 45 canonical work pages · cited by 1 Pith paper

  1. [1]

    In: Vitter, J.S., Spirakis, P.G., Yannakakis, M

    de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. In: Vitter, J.S., Spirakis, P.G., Yannakakis, M. (eds.) Proceedings of the 33rd Annual Symposium on Theory of Computing. pp. 675–683. ACM, Heraklion, Crete, Greece (Jul 2001)

    work page 2001

  2. [2]

    The MIT Press, Cambridge, MA, USA (2008)

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

    work page 2008

  3. [3]

    Barringer, H.: Randomized algorithms - a brief introduction (2010), lecture at the University of Manchester

    work page 2010

  4. [4]

    SIAM (1994)

    Berman, A., Plemmons, R.: Nonnegative matrices in the mathematical sciences. SIAM (1994)

    work page 1994

  5. [5]

    In: Orejas, F., Spirakis, P.G., van Leeuwen, J

    van Breugel, F., Worrell, J.: Towards quantitative verification of probabilistic tran- sition systems. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) Proceedings of the 28th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 2076, pp. 421–432. Springer, Crete, Greece (Jul 2001)

    work page 2001

  6. [6]

    In: Bao, F., Li, H., Wang, G

    Cai, X., Gu, Y.: Measuring anonymity. In: Bao, F., Li, H., Wang, G. (eds.) Pro- ceedings of the 5th International Conference on Information Security Practice and Experience. Lecture Notes in Computer Science, vol. 5451, pp. 183–194. Springer, Xi’an, China (Apr 2009)

    work page 2009

  7. [7]

    Logical Methods in Computer Science6(3) (2010)

    Chatterjee, K., de Alfaro, L., Majumdar, R., Raman, V.: Algorithms for game metrics (full version). Logical Methods in Computer Science6(3) (2010)

    work page 2010

  8. [8]

    In: Birkedal, L

    Chen, D., van Breugel, F., Worrell, J.: On the complexity of computing probabilis- tic bisimilarity. In: Birkedal, L. (ed.) Proceedings of the 15th International Confer- ence on Foundations of Software Science and Computational Structures. Lecture Notes in Computer Science, vol. 7213, pp. 437–451. Springer-Verlag, Tallinn, Es- tonia (Mar/Apr 2012)

    work page 2012

Show all 45 references
  1. [9]

    Çınlar, E.: Probability and stochastics, Graduate Texts in Mathematics, vol. 261. Springer-Verlag, New York, NY, US (2011)

    2011

  2. [10]

    In: Burgard, W., Roth, D

    Comanici, G., Precup, D.: Basis function discovery using spectral clustering and bisimulation metrics. In: Burgard, W., Roth, D. (eds.) Proceedings of the 25th AAAI Conference on Artificial Intelligence. pp. 325–330. AAAI Press, San Fran- cisco, California, USA (Aug 2011)

    2011

  3. [11]

    Cambridge University Press, Cambridge, United Kingdom (2002)

    Davey, B., Priestley, H.: Introduction to lattices and order. Cambridge University Press, Cambridge, United Kingdom (2002)

    2002

  4. [12]

    In: Proceedings of the 4th International Conference on the Quantitative Eval- uation of Systems

    Derisavi, S.: Signature-based symbolic algorithm for optimal Markov chain lump- ing. In: Proceedings of the 4th International Conference on the Quantitative Eval- uation of Systems. pp. 141–150. IEEE Computer Society, Edinburgh, Scotland, UK (Sep 2007)

    2007

  5. [13]

    Information Processing Letters87(6), 309–315 (2003)

    Derisavi, S., Hermanns, H., Sanders, W.H.: Optimal state-space lumping in Markov chains. Information Processing Letters87(6), 309–315 (2003)

    2003

  6. [14]

    In: Baeten, J.C.M., Mauw, S

    Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labeled Markov systems. In: Baeten, J.C.M., Mauw, S. (eds.) Proceedings of the 10th International Conference on Concurrency Theory. Lecture Notes in Computer Sci- ence, vol. 1664, pp. 258–273. Springer-Verl...

    1999

  7. [15]

    Theoretical Computer Science318(3), 323–354 (Jun 2004) 44 S

    Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theoretical Computer Science318(3), 323–354 (Jun 2004) 44 S. Z. Fatmi et al

    2004

  8. [16]

    In: Proceedings of the 5th International Conference on the Quantitative Evaluation of Systems

    Desharnais, J., Laviolette, F., Tracol, M.: Approximate analysis of probabilistic processes: Logic, simulation and games. In: Proceedings of the 5th International Conference on the Quantitative Evaluation of Systems. pp. 264–273. IEEE Com- puter Society, Saint-Malo, France (Sep 2008)

    2008

  9. [17]

    Land9(11) (Oct 2020)

    Eastman, J.R., He, J.: A regression-based procedure for Markov transition proba- bility estimation in land change modeling. Land9(11) (Oct 2020)

    2020

  10. [18]

    Publicationes Mathematicae6, 290–297 (1959)

    Erdös, P., Rényi, A.: On random graphs I. Publicationes Mathematicae6, 290–297 (1959)

    1959

  11. [19]

    In: Laarman, A., Sokolova, A

    Fatmi, S.Z., Chen, X., Dhamija, Y., Wildes, M., Tang, Q., van Breugel, F.: Prob- abilistic model checking of randomized Java code. In: Laarman, A., Sokolova, A. (eds.) Proceedings of the 27th International Symposium on Model Checking Soft- ware, SPIN. Lecture Notes in Computer...

    2021

  12. [20]

    In: Proceedings of the 37th International Conference on Computer Aided Verification

    Fatmi,S.Z.,Kiefer,S.,Parker,D.,vanBreugel,F.:Robustprobabilisticbisimilarity for labelled Markov chains. In: Proceedings of the 37th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, Springer-Verlag, Zagreb, Croatia (Jul 2025)

    2025

  13. [21]

    Rand Corporation (1956)

    Fulkerson, D.R.: Hitchcock transportation problem. Rand Corporation (1956)

    1956

  14. [22]

    In: Broy, M., Jones, C.B

    Giacalone, A., Jou, C., Smolka, S.A.: Algebraic reasoning for probabilistic concur- rent systems. In: Broy, M., Jones, C.B. (eds.) Proceedings of the Working Confer- ence on Programming Concepts and Methods. pp. 443–458. North-Holland, Sea of Galilee, Israel (Apr 1990)

    1990

  15. [23]

    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.) Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Not...

    2019

  16. [24]

    International Journal on Software Tools for Technology Transfer 24(4), 589–610 (2022)

    Hensel,C.,Junges,S.,Katoen,J.,Quatmann,T.,Volk,M.:Theprobabilisticmodel checker storm. International Journal on Software Tools for Technology Transfer 24(4), 589–610 (2022)

    2022

  17. [25]

    Studies in Applied Mathematics20(1/4), 224–230 (Apr 1941)

    Hitchcock, F.: The distribution of a product from several sources to numerous localities. Studies in Applied Mathematics20(1/4), 224–230 (Apr 1941)

    1941

  18. [26]

    Lecture Notes in Computer Science, vol

    Jaeger, M., Mao, H., Larsen, K.G., Mardare, R.: Continuity properties of distances forMarkovprocesses.In:Norman,G.,Sanders,W.H.(eds.)Proceedingsofthe11th International Conference on Quantitative Evaluation of Systems. Lecture Notes in Computer Science, vol. 8657, pp. 297–312. ...

    2014

  19. [27]

    In: Proceedings of the 6th Annual Symposium on Logic in Computer Science

    Jonsson, B., Larsen, K.: Specification and refinement of probabilistic processes. In: Proceedings of the 6th Annual Symposium on Logic in Computer Science. pp. 266–277. IEEE, Amsterdam, The Netherlands (Jul 1991)

    1991

  20. [28]

    In: Proceedings of the 26th Annual ACM Symposium on Theory of Computing

    Karger, D.R., Motwani, R.: Derandomization through approximation: An NC al- gorithm for minimum cuts. In: Proceedings of the 26th Annual ACM Symposium on Theory of Computing. pp. 497–506. ACM, New York, NY, USA (May 1994)

    1994

  21. [29]

    In: Proceedings of the 13th Inter- national Conference on Tools and Algorithms for the Construction and Analysis of Systems

    Katoen, J., Kemna, T., Zapreev, I.S., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Proceedings of the 13th Inter- national Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer S...

    2007

  22. [30]

    Springer-Verlag, Heidelberg, Ger- many (1960) Robust Probabilistic Bisimilarity 45

    Kemeny, J.G., Snell, J.L.: Finite Markov chains. Springer-Verlag, Heidelberg, Ger- many (1960) Robust Probabilistic Bisimilarity 45

    1960

  23. [31]

    In: Johnson, D.S., Fagin, R., Fredman, M.L., Harel, D., Karp, R.M., Lynch, N.A., Papadimitriou, C.H., Rivest, R.L., Ruzzo, W.L., Seiferas, J.I

    Kozen, D.: A probabilistic PDL. In: Johnson, D.S., Fagin, R., Fredman, M.L., Harel, D., Karp, R.M., Lynch, N.A., Papadimitriou, C.H., Rivest, R.L., Ruzzo, W.L., Seiferas, J.I. (eds.) Proceedings of the 15th Annual Symposium on Theory of Computing. pp. 291–297. ACM, Boston, Mas...

    1983

  24. [32]

    In: Gopalakrishnan, G., Qadeer, S

    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Proceedings of the 23rd International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 6806, pp. 585...

    2011

  25. [33]

    In: Proceedings of the 16th Annual ACM Symposium on Principles of Programming Languages

    Larsen, K., Skou, A.: Bisimulation through probabilistic testing. In: Proceedings of the 16th Annual ACM Symposium on Principles of Programming Languages. pp. 344–352. ACM, Austin, TX, USA (Jan 1989)

    1989

  26. [34]

    Monographs in Computer Science, Springer (2004)

    McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Sys- tems. Monographs in Computer Science, Springer (2004)

    2004

  27. [35]

    Frontiers in Built Environment 3, 58 (Oct 2017)

    Mizutani, D., Lethanh, N., Adey, B.T., Kaito, K.: Improving the estimation of Markov transition probabilities using mechanistic-empirical models. Frontiers in Built Environment 3, 58 (Oct 2017)

    2017

  28. [36]

    Cambridge University Press, New York, NY, USA (1995)

    Motwani, R., Raghavan, P.: Randomized algorithms. Cambridge University Press, New York, NY, USA (1995)

    1995

  29. [37]

    In: Householder, A.S., Forsythe, G.E., Germond, H.H

    von Neumann, J.: Various techniques used in connection with random digits. In: Householder, A.S., Forsythe, G.E., Germond, H.H. (eds.) Monte Carlo Method. National Bureau of Standards Applied Mathematics Series, vol. 12, pp. 36–38. US Government Printing Office, Washington, DC (1951)

    1951

  30. [38]

    ClinicoEconomics and Outcomes Research9, 537–546 (Sep 2017)

    Olariu, E., Cadwell, K.K., Hancock, E., Trueman, D., Chevrou-Severac, H.: Cur- rent recommendations on the estimation of transition probabilities in Markov co- hort models for use in health care decision-making: a targeted literature review. ClinicoEconomics and Outcomes Resea...

    2017

  31. [39]

    BIT Numerical Mathemat- ics 15(3), 331–334 (Sep 1975)

    Pollard, J.M.: A Monte Carlo method for factorization. BIT Numerical Mathemat- ics 15(3), 331–334 (Sep 1975)

    1975

  32. [40]

    Graduate Texts in Mathematics, Springer- Verlag, New York, NY, USA (1964)

    Spitzer, F.: Principles of random walk. Graduate Texts in Mathematics, Springer- Verlag, New York, NY, USA (1964)

    1964

  33. [41]

    PharmacoEconomics 39(8), 869–878 (Aug 2021)

    Srivastava, T., Latimer, N.R., Tappenden, P.: Estimation of transition probabilities for state-transition models: A review of NICE appraisals. PharmacoEconomics 39(8), 869–878 (Aug 2021)

    2021

  34. [42]

    Tang, Q.: Computing probabilistic bisimilarity distances. Ph.D. thesis, York Uni- versity, Toronto, Canada (Aug 2018)

    2018

  35. [43]

    In: Meyer, R., Nestmann, U

    Tang, Q., van Breugel, F.: Algorithms to compute probabilistic bisimilarity dis- tances for labelled Markov chains. In: Meyer, R., Nestmann, U. (eds.) Proceedings of the 28th International Conference on Concurrency Theory. LIPIcs, vol. 85, pp. 27:1–27:16. Schloss Dagstuhl - Le...

    2017

  36. [44]

    IET Systems Biology4, 193–211 (2010)

    Thorsley, D., Klavins, E.: Approximating stochastic biochemical processes with Wasserstein pseudometrics. IET Systems Biology4, 193–211 (2010)

    2010

  37. [45]

    Automated Software Engineering10(2), 203–232 (Apr 2003)

    Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Automated Software Engineering10(2), 203–232 (Apr 2003)

    2003

Pith tools

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