{"id":"22f803a6-a88f-44d0-b19d-c7be831d2bb6","arxiv_id":"2505.15290","paper_version":2,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"A new, more stable notion of bisimilarity for labelled Markov chains is defined, proven to ensure continuity of the probabilistic bisimilarity distance, and computable in polynomial time.","lead":"This paper introduces robust probabilistic bisimilarity, a new equivalence relation for labelled Markov chains that stays stable under small perturbations of transition probabilities. It provides a polynomial-time algorithm to compute the relation and shows experimentally that the algorithm is practical on standard benchmarks.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Continuity proof for Theorem 2 has a written gap in Lemma 3: B excludes length-1 successor classes, yet P^A=0 is asserted; the matrix argument is incomplete as written. The gap is likely a fixable typo, but it is load-bearing.","rationale":"The reader's formal weakest_assumption was Proposition 2, but their rationale also flagged a typo in the appendix proof of Lemma 3. My analysis converges on the Lemma 3 gap as the load-bearing issue because Theorem 2 is Proposition 1 plus Lemma 3, and Lemma 3 is the nontrivial direction. The specific problem is the boundary between B and A: with B defined as length greater than 1, direct successors are in A and the proof's reliance on P^A=0 is not justified. The intended fix is local and plausible, so I do not find a deeper flaw. Proposition 2 is a cited standard result and is not the weakest point. The algorithm's correctness relies on Proposition 7, which appears coherent but would benefit from independent checking. Lack of a released artifact is a reproducibility limitation, not a mathematical objection. Since the reader already issued CONDITIONAL based on the same proof gap and missing artifact, my assessment does not change the verdict, hence UNCHANGED. I mark agreement as partial because the reader identified the gap in their rationale but stated a different formal weakest_assumption.","tokens_in":1093,"tokens_out":1798,"duration_ms":135742,"concrete_test":"Rederive Lemma 3 with B redefined as all communication classes reachable from C by a path of length at least 1. Verify: (i) for every (u,v)∈C, support(P(u,v))⊆C∪B; (ii) the induction hypothesis applies to all classes in B; (iii) the resulting bound on ∥γ^C_Pn−γ^C_P∥ still converges to 0. If all three hold, the gap is a harmless typo; if (iii) fails, the upper-semicontinuity proof is not salvageable by this argument.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Lemma 3 in Appendix G supplies the upper-semicontinuity half of Theorem 2. In its induction step, fixing a communication class C, the proof defines B as the set of state pairs of all communication classes reachable from C via a path of length greater than 1, and sets A=(S×S)\\(B∪C). It then asserts support(P(u,v))⊆B∪C for all (u,v)∈C, hence P^A=0. With this definition, a direct successor class D of C is not in B, so D⊆A, and P may place positive mass on D, making P^A=0 unjustified. Therefore the displayed matrix equation for γ^C_Pn and the bound on ∥γ^C_Pn−γ^C_P∥ do not follow as written, and the claim lim_n γ_Pn(u,v)=γ_P(u,v)=0 for every reachable class is not established. The most plausible repair is to redefine B as all classes reachable by a path of positive length, so the induction hypothesis applies to every successor class and the support condition holds. The gap appears fixable, but as written it is a real hole in the proof of the central continuity theorem.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":34970,"tokens_out":4757,"duration_ms":43355,"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":[{"comment":"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.","section":"Appendix G, Lemma 3"}],"minor_comments":[{"comment":"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.","section":"Appendix H, Figure 6"},{"comment":"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.","section":"Proposition 27"},{"comment":"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.","section":"Section 6.3"},{"comment":"In the abstract and introduction, the phrase 'alackofrobustness' appears to be missing spaces ('a lack of robustness'); this typesetting issue should be corrected.","section":"Abstract"}],"recommendation":"major_revision","confidential_remarks":"The main issue is the gap in Lemma 3's proof. If the authors correct the definition of B and check that the induction then goes through, I expect the paper to be acceptable. The experimental evaluation is broad and the algorithmic contribution is clearly presented; the theoretical gap is the only blocker I see."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper defines robust probabilistic bisimilarity: states are robustly bisimilar if some policy drives the product chain to the diagonal with probability 1. This is a new equivalence, strictly finer than ordinary probabilistic bisimilarity, and the main theorem says that for robustly bisimilar states the bisimilarity distance is continuous under perturbations of the transition function. That is the right kind of result for a problem that matters in practice, since measured probabilities are rarely exact. The polynomial-time algorithm via filter/prune/bisim refinement is plausible, and the experiments on QVBS and jpf-probabilistic models show it runs on reasonably large chains. The paper is also honest about what is conjectured, notably the necessity direction of continuity, and about the models that exhaust memory.\n\nThe core construction holds up on reading. The definition of robustness is natural, the proof that it is a bisimulation and the greatest robust bisimulation is fine, and the characterization of distances via policies is standard external work, not fitted to the examples.\n\nThe soft spot is in Appendix G, Lemma 3. The proof defines B as the state pairs of communication classes reachable from C by a path of length greater than 1, and A as everything outside B and C. It then asserts that support(P(u,v)) is contained in B ∪ C for (u,v) in C, hence P^A = 0. That does not follow: a direct successor class D of C is reachable by a path of length 1, so D is in A, and P may put positive mass there. The matrix equation and the bound on ||γ^C_Pn − γ^C_P|| depend on P^A = 0, so the written proof of upper semicontinuity has a real hole. The repair is straightforward: redefine B as all classes reachable by a path of positive length, bringing direct successors under the induction hypothesis. I think this is a typo, not a conceptual flaw, but the fix is load-bearing and a referee should verify the corrected argument.\n\nMinor limitations: no released implementation, so the reported times are not independently reproducible, and the O(n^6) bound is steep though the experiments suggest it is acceptable in practice.\n\nMy take: the paper deserves a serious referee and should be sent out. I would ask for a corrected Lemma 3 before acceptance, but the idea and the main theorem are sound.","headline":"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.","tokens_in":35516,"tokens_out":2650,"would_cite":true,"duration_ms":23012,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q60","68Q87"],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["labelled Markov chains","robust probabilistic bisimilarity","probabilistic bisimilarity distance","behavioural pseudometric","continuity under perturbations","coupling policies","partition refinement"],"falsifier":"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.","tokens_in":34540,"feed_emoji":"🎲","tokens_out":5103,"duration_ms":40615,"temperature":0.7,"pith_summary":"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.","feed_headline":"Robust bisimilarity survives noisy probabilities","feed_subtitle":"States that are robustly bisimilar keep distance near zero under any small perturbation.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies Theorem 10.15, which identifies γ_P(s,t) as the reaching probability to S²_1 in the product chain induced by policy P.","marker":"[2]"},{"why":"Supplies Theorem 8, the characterization δ_τ = min_{P∈P_τ} γ_P, which is the quantitative foundation for the continuity proof.","marker":"[8]"},{"why":"Provides Theorem 4.10, the equivalence between zero bisimilarity distance and probabilistic bisimilarity, used throughout the paper.","marker":"[15]"},{"why":"Presents the discontinuity examples and earlier continuity results that motivate the notion of robustness.","marker":"[26]"},{"why":"Provides the partition-refinement algorithm used by the Bisim component in the robust-bisimilarity computation.","marker":"[13]"},{"why":"Gives the fixed-point characterization of the bisimilarity distance that underlies the policy-based reformulation.","marker":"[5]"}],"fun_headline_variants":["Robust bisimilarity stays stable under perturbations","New bisimilarity notion tolerates noisy probabilities","Continuity of bisimilarity under small perturbations","A bisimulation that survives noisy data"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Robust bisimilarity stays stable under perturbations","New bisimilarity notion tolerates noisy probabilities","Continuity of bisimilarity under small perturbations","A bisimulation that survives noisy data"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000421,"raw_usage":{"total_tokens":2132,"prompt_tokens":877,"completion_tokens":1255,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":493,"completion_tokens_details":{"reasoning_tokens":1197}},"tokens_in":493,"tokens_out":1255,"duration_ms":7731,"temperature":1.0,"reasoning_tokens":1197,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T15:21:13.054047+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"The MIT Press, Cambridge, MA, USA (2008)","cited_arxiv_id":null,"evidence_quote":"Supplies Theorem 10.15, which identifies γ_P(s,t) as the reaching probability to S²_1 in the product chain induced by policy P."},{"cited_title":"In: Birkedal, L","cited_arxiv_id":null,"evidence_quote":"Supplies Theorem 8, the characterization δ_τ = min_{P∈P_τ} γ_P, which is the quantitative foundation for the continuity proof."},{"cited_title":"Theoretical Computer Science318(3), 323–354 (Jun 2004) 44 S","cited_arxiv_id":null,"evidence_quote":"Provides Theorem 4.10, the equivalence between zero bisimilarity distance and probabilistic bisimilarity, used throughout the paper."},{"cited_title":"Lecture Notes in Computer Science, vol","cited_arxiv_id":null,"evidence_quote":"Presents the discontinuity examples and earlier continuity results that motivate the notion of robustness."},{"cited_title":"Information Processing Letters87(6), 309–315 (2003)","cited_arxiv_id":null,"evidence_quote":"Provides the partition-refinement algorithm used by the Bisim component in the robust-bisimilarity computation."},{"cited_title":"In: Orejas, F., Spirakis, P.G., van Leeuwen, J","cited_arxiv_id":null,"evidence_quote":"Gives the fixed-point characterization of the bisimilarity distance that underlies the policy-based reformulation."}],"review_version":1}