pith. sign in

arxiv: 2507.19886 · v2 · submitted 2025-07-26 · 💻 cs.LO

A Unifying Approach to Probabilistic Testing Equivalences

Weijun Chen , Yuxi Fu , Huan Long , Hao Wu This is my paper

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

classification 💻 cs.LO
keywords probabilistic testing equivalencesdistribution-based semanticsprocess predicatescongruencesfair/should equivalencemay equivalenceprobabilistic bisimilaritiespCSP
0
0 comments X

The pith

Distribution-based semantics unify internal and external characterizations of probabilistic testing equivalences.

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

The paper proposes a unifying approach to probabilistic testing equivalences for concurrent systems. It defines a new distribution-based semantics for probabilistic models and builds a testing framework around process predicates. This framework yields both an internal characterization and an external one. The external version generalizes the classical fair/should and may equivalences from the non-probabilistic setting. The resulting equivalences are shown to be congruences, and they are compared directly to probabilistic bisimilarities. The same techniques apply to other probabilistic models, illustrated by a case study on pCSP.

Core claim

With a distribution-based semantics for probabilistic models and a testing framework defined with respect to process predicates, the paper derives internal and external characterizations of testing equivalences. The external characterization generalizes classical fair/should equivalence and may equivalence. These equivalences are congruences, and a comparison with probabilistic bisimilarities is provided. The method extends to other probabilistic concurrent models such as pCSP.

What carries the argument

The distribution-based semantics for probabilistic models together with the probabilistic testing framework defined relative to process predicates, which support both internal and external characterizations of the equivalences.

If this is right

  • The testing equivalences are congruences for the operators of the process language.
  • The external characterization directly extends the classical fair/should and may equivalences to probabilistic models.
  • A detailed comparison locates the new equivalences relative to probabilistic bisimilarities.
  • The same characterizations and proofs carry over to other probabilistic models, as shown by the pCSP case study.

Where Pith is reading between the lines

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

  • The congruences could simplify compositional verification of probabilistic properties in mobile systems.
  • The predicate-based testing view might be adapted to define equivalences for models that mix probability with other quantitative features.
  • Concrete algorithms for checking the equivalences could be derived from the external characterization for practical model checking.

Load-bearing premise

The new distribution-based semantics and the predicate-based testing framework together supply a sound foundation for defining and characterizing the testing equivalences.

What would settle it

Two probabilistic processes that are equivalent according to the internal characterization but fail to be equivalent under the external characterization, or whose parallel composition violates congruence, would disprove the unification.

Figures

Figures reproduced from arXiv: 2507.19886 by Hao Wu, Huan Long, Weijun Chen, Yuxi Fu.

Figure 1
Figure 1. Figure 1: The inclusion relations among probabilistic equivalences presented in this paper, where the arrow from one equivalence [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: LTS for CCS. and transitive closure of τ −−→. Given a process P, an internal action sequence of P is a possibly infinite sequence of the form P τ −−→ P1 τ −−→ · · · . A process P is divergent if there exists an infinite internal action sequence starting from P. 2.2. Classical testing equivalence Given a set S, we use R and E to denote a relation and an equivalence relation over S, respectively. We write S/… view at source ↗
Figure 3
Figure 3. Figure 3: The counterexamples of classical testing equivalences. [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: pLTS for RCCS - Part I. µ (α,p) −−−→ ν  where µ, ν ∈ D(PRCCS ), α ∈ A, p ∈ (0, 1], and there exists a process P ∈ supp(µ) such that P α−−→ ρ for some ρ and ν = µ + µ(P)p(ρ − δP ).  [PITH_FULL_IMAGE:figures/full_fig_p007_4.png] view at source ↗
Figure 6
Figure 6. Figure 6: Examples of the distribution-based semantics. [PITH_FULL_IMAGE:figures/full_fig_p007_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: The infinite transition sequence of Q2 to obtain the satisfactory probability 1 2 . 4.2. Approximation by degenerate sequences Since both the external and internal characterization of probabilistic testing will be defined within this framework, we provide several general technical lemmas in this part. Recall that a witness π of an internal transition sequence is degenerate if π ∈ τ ∗ , i.e., without uncert… view at source ↗
Figure 8
Figure 8. Figure 8: Two processes can be probabilistically may equivalent without being probabilistically weak bisimilar. [PITH_FULL_IMAGE:figures/full_fig_p021_8.png] view at source ↗
read the original abstract

Probabilistic concurrent systems are foundational models for modern mobile computing. In this paper, a unifying approach to probabilistic testing equivalences is proposed. With the help of a new distribution-based semantics for probabilistic models and a probabilistic testing framework with respect to process predicates, the internal characterization and the external characterization for testing equivalences are studied. The latter characterization can be viewed as the generalization of the classical fair/should equivalence and may equivalence. These equivalences are shown to be congruences. A thorough comparison between these equivalences and probabilistic bisimilarities is carried out. The techniques introduced in this paper can be easily extended to other probabilistic concurrent models. To showcase this flexibility, a case study is carried out on the pCSP model.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper proposes a unifying approach to probabilistic testing equivalences in concurrent systems. It introduces a distribution-based semantics for probabilistic models together with a probabilistic testing framework defined with respect to process predicates. Using these, the authors develop internal and external characterizations of testing equivalences; the external characterization is presented as a generalization of classical fair/should and may equivalences. The equivalences are shown to be congruences, compared in detail with probabilistic bisimilarities, and illustrated through a case study on the pCSP model. The framework is claimed to extend readily to other probabilistic concurrent models.

Significance. If the characterizations, congruence proofs, and comparisons hold, the work supplies a coherent, extensible foundation that unifies several lines of research on testing equivalences for probabilistic processes. The generalization of may/fair equivalences and the explicit congruence results are useful for compositional reasoning, while the pCSP case study and the stated extensibility indicate practical reach beyond the core model.

minor comments (2)
  1. [Introduction] The abstract and introduction would benefit from a brief forward pointer to the specific theorems that establish the internal and external characterizations (e.g., the theorem numbers that prove congruence).
  2. [Semantics] Notation for distributions and predicate satisfaction is introduced in the semantics section; a small table summarizing the key operators and their probabilistic interpretations would improve readability for readers unfamiliar with the distribution-based approach.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the careful review of our manuscript and for the positive evaluation of its significance. We are pleased with the recommendation for minor revision and will incorporate any necessary clarifications or corrections in the revised version.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper introduces a new distribution-based semantics for probabilistic models together with a predicate-based probabilistic testing framework as independent foundational definitions. These are then used to derive internal and external characterizations of testing equivalences, prove congruence properties, and compare them to bisimilarities. The characterizations and congruences are obtained by applying the new semantics and framework rather than by fitting parameters to the target equivalences or by reducing to prior self-citations; the derivation chain therefore remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Review based on abstract only; no specific free parameters, axioms, or invented entities can be extracted in detail. The approach relies on standard assumptions from process algebra and probabilistic semantics.

axioms (1)
  • domain assumption Probabilistic concurrent systems admit a distribution-based semantics that supports testing equivalences.
    Invoked as the foundation for the new approach in the abstract.

pith-pipeline@v0.9.0 · 5647 in / 1183 out tokens · 34758 ms · 2026-05-19T03:24:21.777031+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

78 extracted references · 78 canonical work pages · 1 internal anchor

  1. [1]

    Boreale, R

    M. Boreale, R. Pugliese, Basic Observables for Processes, Information and Computation 149 (1) (1999) 77–98. doi: 10.1006/inco.1998.2755

    work page doi:10.1006/inco.1998.2755 1999

  2. [2]

    De Nicola, M

    R. De Nicola, M. C. B. Hennessy, Testing equivalences for processes, Theoretical Computer Science 34 (1) (1984) 83–133. doi:10.1016/0304-3975(84)90113-0. 22

    work page doi:10.1016/0304-3975(84)90113-0 1984

  3. [3]

    Brinksma, A

    E. Brinksma, A. Rensink, W. Vogler, Fair testing, in: I. Lee, S. A. Smolka (Eds.), CONCUR ’95: Concurrency Theory, Springer, Berlin, Heidelberg, 1995, pp. 313–327. doi:10.1007/3-540-60218-6_23

    work page doi:10.1007/3-540-60218-6_23 1995

  4. [4]

    Natarajan, R

    V. Natarajan, R. Cleaveland, Divergence and fair testing, in: Z. F¨ ul¨ op, F. G´ ecseg (Eds.), Automata, Languages and Programming, Springer, Berlin, Heidelberg, 1995, pp. 648–659. doi:10.1007/3-540-60084-1_112

    work page doi:10.1007/3-540-60084-1_112 1995

  5. [5]

    Baier, J.-P

    C. Baier, J.-P. Katoen, Principles of Model Checking, The MIT Press, Cambridge, Mass, 2008

    work page 2008

  6. [6]

    Araujo, M

    H. Araujo, M. R. Mousavi, M. Varshosaz, Testing, validation, and verification of robotic and autonomous systems: a systematic review, ACM Transactions on Software Engineering and Methodology 32 (2) (2023) 1–61

    work page 2023

  7. [7]

    Cheung, M

    L. Cheung, M. Stoelinga, F. Vaandrager, A testing scenario for probabilistic processes, J. ACM 54 (6) (2007) 29–es. doi:10.1145/1314690.1314693. URL https://doi.org/10.1145/1314690.1314693

    work page doi:10.1145/1314690.1314693 2007

  8. [8]

    R. M. Hierons, M. N´ u˜ nez, Testing probabilistic distributed systems, in: J. Hatcliff, E. Zucca (Eds.), Formal Techniques for Distributed Systems, Springer Berlin Heidelberg, Berlin, Heidelberg, 2010, pp. 63–77

    work page 2010

  9. [9]

    Gerhold, M

    M. Gerhold, M. Stoelinga, Model-based testing of probabilistic systems, Form. Asp. Comput. 30 (1) (2018) 77–106. doi:10.1007/s00165-017-0440-4 . URL https://doi.org/10.1007/s00165-017-0440-4

    work page doi:10.1007/s00165-017-0440-4 2018

  10. [10]

    Crafa, F

    S. Crafa, F. Ranzato, A spectrum of behavioral relations over ltss on probability distributions, in: Proceedings of the 22nd International Conference on Concurrency Theory, CONCUR’11, Springer-Verlag, Berlin, Heidelberg, 2011, p. 124–139

    work page 2011

  11. [11]

    Etessami, M

    K. Etessami, M. Yannakakis, Recursive Markov Decision Processes and Recursive Stochastic Games, Journal of the ACM 62 (2) (2015) 11:1–11:69. doi:10.1145/2699431

    work page doi:10.1145/2699431 2015

  12. [12]

    Fu, Model independent approach to probabilistic models, Theoretical Computer Science 869 (2021) 181–194

    Y. Fu, Model independent approach to probabilistic models, Theoretical Computer Science 869 (2021) 181–194. doi: 10.1016/j.tcs.2021.04.001

    work page doi:10.1016/j.tcs.2021.04.001 2021

  13. [13]

    H. Wu, H. Long, Probabilistic weak bisimulation and axiomatization for probabilistic models, Information Processing Letters 182 (2023) 106399. doi:10.1016/j.ipl.2023.106399

    work page doi:10.1016/j.ipl.2023.106399 2023

  14. [14]

    Zhang, H

    W. Zhang, H. Long, X. Xu, Uniform Random Process Model Revisited, in: A. W. Lin (Ed.), Programming Languages and Systems, Lecture Notes in Computer Science, Springer International Publishing, Cham, 2019, pp. 388–404. doi: 10.1007/978-3-030-34175-6_20

    work page doi:10.1007/978-3-030-34175-6_20 2019

  15. [15]

    Cattani, R

    S. Cattani, R. Segala, Decision Algorithms for Probabilistic Bisimulation, in: L. Brim, M. Kˇ ret´ ınsk´ y, A. Kuˇ cera, P. Janˇ car (Eds.), CONCUR 2002 — Concurrency Theory, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 2002, pp. 371–386. doi:10.1007/3-540-45694-5_25

    work page doi:10.1007/3-540-45694-5_25 2002

  16. [16]

    Segala, Modeling and Verification of Randomized Distributed Real-Time Systems, Thesis, Massachusetts Institute of Technology (1995)

    R. Segala, Modeling and Verification of Randomized Distributed Real-Time Systems, Thesis, Massachusetts Institute of Technology (1995)

    work page 1995

  17. [17]

    Turrini, H

    A. Turrini, H. Hermanns, Polynomial time decision algorithms for probabilistic automata, Information and Computation 244 (2015) 134–171. doi:10.1016/j.ic.2015.07.004

    work page doi:10.1016/j.ic.2015.07.004 2015

  18. [18]

    Deng, Semantics of Probabilistic Processes, Springer Berlin Heidelberg, Berlin, Heidelberg, 2014

    Y. Deng, Semantics of Probabilistic Processes, Springer Berlin Heidelberg, Berlin, Heidelberg, 2014. doi:10.1007/ 978-3-662-45198-4

    work page 2014

  19. [19]

    Fu, Theory of interaction, Theoretical Computer Science 611 (2016) 1–49

    Y. Fu, Theory of interaction, Theoretical Computer Science 611 (2016) 1–49. doi:10.1016/j.tcs.2015.07.043

    work page doi:10.1016/j.tcs.2015.07.043 2016

  20. [20]

    Y. Fu, H. Zhu, The Name-Passing Calculus (2015). arXiv:1508.00093, doi:10.48550/arXiv.1508.00093

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.1508.00093 2015

  21. [21]

    Milner, Communication and Concurrency, Prentice-Hall, Inc., 1989

    R. Milner, Communication and Concurrency, Prentice-Hall, Inc., 1989

    work page 1989

  22. [22]

    R. J. van Glabbeek, W. P. Weijland, Branching time and abstraction in bisimulation semantics, Journal of the ACM 43 (3) (1996) 555–600. doi:10.1145/233551.233556

    work page doi:10.1145/233551.233556 1996

  23. [23]

    R. J. van Glabbeek, The linear time — Branching time spectrum II, in: E. Best (Ed.), CONCUR’93, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 1993, pp. 66–81. doi:10.1007/3-540-57208-2_6

    work page doi:10.1007/3-540-57208-2_6 1993

  24. [24]

    Cleaveland, Z

    R. Cleaveland, Z. Dayar, S. A. Smolka, S. Yuen, Testing preorders for probabilistic processes, Information and Computation 154 (2) (1999) 93–148. doi:https://doi.org/10.1006/inco.1999.2808

    work page doi:10.1006/inco.1999.2808 1999

  25. [25]

    H. Wu, Y. Fu, H. Long, X. Xu, W. Zhang, Analyzing Divergence for Nondeterministic Probabilistic Models (2024). arXiv:2403.00491, doi:10.48550/arXiv.2403.00491

    work page doi:10.48550/arxiv.2403.00491 2024

  26. [26]

    W. Yi, K. G. Larsen, Testing Probabilistic and Nondeterministic Processes, in: R. J. Linn, M. ¨U. Uyar (Eds.), Protocol Specification, Testing and Verification, XII, IFIP Transactions C: Communication Systems, Elsevier, Amsterdam, 1992, pp. 47–61. doi:10.1016/B978-0-444-89874-6.50010-6

    work page doi:10.1016/b978-0-444-89874-6.50010-6 1992

  27. [27]

    Y. Deng, Y. Feng, Probabilistic bisimilarity as testing equivalence, Information and Computation 257 (2017) 58–64. doi:https://doi.org/10.1016/j.ic.2017.09.014

    work page doi:10.1016/j.ic.2017.09.014 2017

  28. [28]

    Arora, B

    S. Arora, B. Barak, Computational Complexity: A Modern Approach, Cambridge University Press, 2006

    work page 2006

  29. [29]

    W. Du, Y. Deng, D. Gebler, Behavioural pseudometrics for nondeterministic probabilistic systems., Sci. Ann. Comput. Sci. 32 (2) (2022) 211–254

    work page 2022

  30. [30]

    Dal Lago, M

    U. Dal Lago, M. Murgia, et al., Contextual behavioural metrics, in: Proceedings of the 34th International Conference on Concurrency Theory, CONCUR 2023, 2023, pp. 1–17

    work page 2023

  31. [31]

    Spork, C

    T. Spork, C. Baier, J.-P. Katoen, J. Piribauer, T. Quatmann, A Spectrum of Approximate Probabilistic Bisimulations, in: R. Majumdar, A. Silva (Eds.), 35th International Conference on Concurrency Theory (CONCUR 2024), Vol. 311 of Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl – Leibniz-Zentrum f¨ ur Informatik, Dagstuhl, German...

    work page doi:10.4230/lipics.concur.2024.37 2024

  32. [32]

    Bernardo, R

    M. Bernardo, R. De Nicola, M. Loreti, Revisiting trace and testing equivalences for nondeterministic and probabilistic processes, Logical Methods in Computer Science 10 (2014)

    work page 2014

  33. [33]

    Bernardo, et al., Probabilistic trace and testing semantics: The importance of being coherent, Foundations and Trends® in Programming Languages 7 (4) (2022) 244–332

    M. Bernardo, et al., Probabilistic trace and testing semantics: The importance of being coherent, Foundations and Trends® in Programming Languages 7 (4) (2022) 244–332. 23 A. Omitted Proofs A.1. Proofs for Section 3 A.1.1. Proof of Lemma 2 Proof. The cases are trivial for p = 0 or p = 1. Now we assume p ∈ (0, 1)

    work page 2022

  34. [34]

    The base case is trivial

    Prove by induction on |π1| + |π2|. The base case is trivial. Assume that |π1| + |π2| = k + 1 > 0. Then at least one of |π1|, |π2| are non-zero. W.l.o.g., we assume that |π1| > 0. Then the original transition sequence µ1 π − − →ν1 can be divided into µ1 π′ 1 − − →ν′ 1 (α,q) − − − →ν1, where π1 = π′ 1 ◦ (α, q) and q ∈ (0, 1]. Since |π′ 1| + |π2| = k, by app...

    work page

  35. [35]

    Note that pν′ 1(P ) + (1 − p)ν2(P ) ̸= 0 for p ∈ (0, 1)

    such that P α − − →ρ and ν1 = ν′ 1 + ν′ 1(P )q(ρ − δP ). Note that pν′ 1(P ) + (1 − p)ν2(P ) ̸= 0 for p ∈ (0, 1). We can define r := ν′ 1(P)pq pν′ 1(P)+(1−p)ν2(P). Still considering the aforementioned transition P α − − →ρ, we have pν′ 1 + (1 − p)ν2 (α,r) − − − →ν := pν′ 1 + (1 − p)ν2 + [pν′ 1 + (1 − p)ν2](P )r(ρ − δP ) = pν1 + (1 − p)ν2. (A.1) Let π := π...

    work page

  36. [36]

    In the base case where |π| = 0, set ν1 = µ, ν2 = µ, and the result follows

    Prove by induction on |π|. In the base case where |π| = 0, set ν1 = µ, ν2 = µ, and the result follows. When |π| = k + 1, we can divide the transition sequence corresponding to pµ1 + (1 − p)µ2 π − − →ν into pµ1 + (1 − p)µ2 π′ − − →ν′ (α,q) − − →ν, where π = π′ ◦ (α, q) and q ∈ (0, 1]. Since |π′| = k, by the induction hypothesis, there exists ν′ 1, ν′ 2 ∈ D...

    work page

  37. [37]

    Assume, without loss of generality, that ν′ 1(φ) ≤ ν(φ) ≤ ν′ 2(φ)

    By Lemma 2, there exist ν′ 1, ν′ 2 such that µ′ 1 π′′ 1 − − →ν′ 1, µ′ 2 π′′ 2 − − →ν′ 2 and ν = (1 − p)ν′ 1 + pν′ 2, where |π′′ 1 |, |π′′ 2 | ≤ k. Assume, without loss of generality, that ν′ 1(φ) ≤ ν(φ) ≤ ν′ 2(φ). Since |π′′ 1 |, |π′′ 2 | ≤ k, by the induction hypothesis, there exist two distribution ν1, ν2 such that (i) µ′ 1 π′ 1 − − →ν1, µ′ 2 π′ 2 − − →...

    work page

  38. [38]

    For 1 ≤ i ≤ m, since b /∈ L, we have BL i b − − →, which implies BL i ∈ ψL and χmay L (BL i ) = 1

    work page

  39. [39]

    There exists an external action li ∈ L ∪ L and a distribution ρi such that Ai li − − →ρi

    For 1 ≤ i ≤ n, Ai ∈ ψL. There exists an external action li ∈ L ∪ L and a distribution ρi such that Ai li − − →ρi. Since Q li − − →δ0, we have δAL i τ − − →(L)(ρi | δ0) and χmay L ((L)(ρi | δ0)) = 0. 25 Note that νL =Pn i=1 ν(Ai)δAL i +Pm i=1 ν(Bi)δBL i . By Corollary 3 (1), we have µL ⇝ νL ⇝ ν′ := nX i=1 ν(Ai)(L)(ρi | δ0) + mX i=1 ν(Bi)δRL i . (A.5) By Le...

    work page

  40. [40]

    If no such division exists, break from this procedure

    Divide µL πj − − →νj into µL π1 j − − →µ′ τ − − →µ′′ π2 j − − →νj such that (i) πj = π1 j ◦τ ◦π2 j , (ii) µ′′(X1) = νj(X1), and (iii) µ′(X1) > µ ′′(X1). If no such division exists, break from this procedure. Assume that µ′ τ − − →µ′′ is caused by P L τ − − →ρ for some process P L ∈ ψL and distribution ρ such that ρ(X2) = 1. This indicates that this τ acti...

    work page

  41. [41]

    By Corollary 3 (2), there exists µ1, µ2 such that µ′−µ′(P L)δP L 1−µ′(P L) ⇝ µ1, ρ ⇝ µ2, and νj = (1 − µ′(P L))µ1 + µ′(P L)µ2

    Since µ′ = (µ′ −µ′(P L)δP L)+ µ′(P L)δP L and µ′ τ − − →µ′′, we have µ′′ = (µ′ −µ′(P L)δP L)+ µ′(P L)ρ. By Corollary 3 (2), there exists µ1, µ2 such that µ′−µ′(P L)δP L 1−µ′(P L) ⇝ µ1, ρ ⇝ µ2, and νj = (1 − µ′(P L))µ1 + µ′(P L)µ2. Replacing δP L ⇝ ρ ⇝ µ2 by δP L ⇝ δP L and again by this lemma, we obtain a new transition sequence µ′ π3 j − − →νj+1 := (1 − ...

    work page

  42. [42]

    Besides, by µ′′(X1) = νj(X1) and monotonicity, we have µ1(X1) = µ′ − µ′(P L)δP L 1 − µ′(P L) (X1) = µ′(X1) − µ′(P L) 1 − µ′(P L)

    We have maintained ( νj+1 − νj)(ψL ∪ X2) = µ′(P L)(δP L − µ2)(ψL ∪ X2) = µ′(P L)(1 − 1) = 0. Besides, by µ′′(X1) = νj(X1) and monotonicity, we have µ1(X1) = µ′ − µ′(P L)δP L 1 − µ′(P L) (X1) = µ′(X1) − µ′(P L) 1 − µ′(P L) . (A.8) Therefore, we can derive that νj+1(X1) = (1 − µ′(P L))µ1(X1) + µ′(P L)δP L(X1) = µ′(X1). Although πj+1 may be longer than πj, t...

    work page

  43. [43]

    χmay ω (µ1) = χmay ω (µ2), and

    work page

  44. [44]

    χfair ω (µ1) = χfair ω (µ2). Proof. By Proposition 9, if µ1 ⇝ ν1 for some ν1, then µ2 ⇝ ν2 ∼† p ν1 for some ν2. By definition, ν1(ψω) = ν2(ψω). Therefore, Oµ1 ω ⊆ O µ2 ω . By symmetry, Oµ1 ω = Oµ2 ω and χmay ω (µ1) = χmay ω (µ2). Now we also have χmay ω (ν1) = χmay ω (ν2) Therefore, χfair ω (µ1) = χfair ω (µ2) holds. □ Claim 34. Let µ1, µ2 ∈ P ω RCCS be t...

    work page

  45. [45]

    χmay((L)µ1 | µ2) = χmay(µ1 | (L)µ2), and

    work page

  46. [46]

    χfair((L)µ1 | µ2) = χfair(µ1 | (L)µ2). Proof. Define a special set of processes X = {(L)P1 | P2} ⊆ P ω RCCS. For P := ( L)P1 | P2 ∈ X , define P ∗ := P1 | (L)P2. Moreover, if P ∈ ψω, then P ∗ ∈ ψω since ω ̸∈ N . For µ ∈ D(X ), we can also define µ∗ := {(P ∗, µ(P )) : P ∈ supp(µ)} such that µ(ψω) = µ∗(ψω). By induction, we can prove that if µ ∈ D(X ) and µ...

    work page

  47. [47]

    χmay ω ((µ1 | ν) | o) = χmay ω (µ1 | (ν | o)) = χmay ω (µ2 | (ν | o)) = χmay ω ((µ2 | ν) | o),

    work page

  48. [48]

    Therefore, ( µ1 | ν) = D may (µ2 | ν) and ( L)µ1 =D may (L)µ2, which implies that the equivalence = D may is D- extensional

    χmay ω ((L)µ1 | o) = χmay ω (µ1 | (L)o) = χmay ω (µ1 | (L)o) = χmay ω ((L)µ2 | o). Therefore, ( µ1 | ν) = D may (µ2 | ν) and ( L)µ1 =D may (L)µ2, which implies that the equivalence = D may is D- extensional. Similarly, the equivalence = D fair is also D-extensional. □ 27 A.3.5. Proof of Lemma 14 Proof. For any ν such that µ | oL π − − →ν and π ∈ τ ∗, the ...

    work page

  49. [49]

    Thus, δP |OL τ − − →ρP | δω and (ρP | δω)(ψω) = 1

    For any process P ∈ ψL ∩ supp(ν), we have P ℓ − − →ρP for some ρP ∈ D(PRCCS) and ℓ ∈ L ∪ L. Thus, δP |OL τ − − →ρP | δω and (ρP | δω)(ψω) = 1

    work page

  50. [50]

    Since ν | oL =P P ∈supp(ν) ν(P )δP |OL, by Corollary 3, we have µ | oL ⇝ ν | oL ⇝ ν′ := X P ∈ψL∩supp(ν) ν(P )(ρP | δω) + X P ∈ψL∩supp(ν) ν(P )δP |OL

    If P ∈ ψL ∩ supp(ν), then ν(ψω) = 0. Since ν | oL =P P ∈supp(ν) ν(P )δP |OL, by Corollary 3, we have µ | oL ⇝ ν | oL ⇝ ν′ := X P ∈ψL∩supp(ν) ν(P )(ρP | δω) + X P ∈ψL∩supp(ν) ν(P )δP |OL . (A.14) Clearly, ν′(ψω) =P P ∈ψL∩supp(ν) ν(P ) = ν(ψL). Therefore, χmay ω (µ | oL) = sup {ν′(ψω) : µ | oL ⇝ ν′} ≥ sup {ν(ψL) : µ ⇝ ν} = χmay L (µ), (A.15) which implies χ...

    work page

  51. [51]

    It is trivial that sup OP ω = 1 for any P ∈ X2

    work page

  52. [52]

    Therefore, sup OQ ω = 1 for any Q ∈ ψL

    If P ℓ − − →ρ, then δP |OL τ − − →ρ | δω ∈ D(X2). Therefore, sup OQ ω = 1 for any Q ∈ ψL. For anyν such that µ | oL π − − →ν and π ∈ τ ∗, we can obtain a transition sequenceµ | oL ⇝ νk for some k, such that i) all distributions are of typeX1, and ii) supOνk ω = sup Oν ω. The invariant ii) can be maintained because processes can only evolve from ψL to dist...

    work page

  53. [53]

    Since L must be finite, by Lemma 14, we have χmay L (µ1) = χmay ω (µ1 | oL) = χmay ω (µ2 | oL) = χmay L (µ2)

    For any distributions µ1, µ2 ∈ D(PRCCS) such that µ1 =D may µ2, we define L := N (µ1) ∪ N(µ2). Since L must be finite, by Lemma 14, we have χmay L (µ1) = χmay ω (µ1 | oL) = χmay ω (µ2 | oL) = χmay L (µ2). (A.17) Hence, the equivalence = D may is probabilistically equipollent

    work page

  54. [54]

    (A.18) Therefore, the equivalence = D fair is probabilistically strongly equipollent

    For any distributions µ1, µ2 ∈ D(PRCCS) such that µ1 =D fair µ2, we can prove in a similar manner that χfair L (µ1) = χfair ω (µ1 | oL) = χfair ω (µ2 | oL) = χfair L (µ2). (A.18) Therefore, the equivalence = D fair is probabilistically strongly equipollent. By Lemma 13, we have = D may ⊆ =D ♢ and = D fair ⊆ =D □. □ A.3.7. Proof of Lemma 16 Proof. For any ...

    work page

  55. [55]

    For any µ1, µ2 such that µ1 R◦ µ2, we assume that µ1 = ϑ P i∈I ai.P1,i and µ2 = ϑ P i∈I ai.P2,i , where ϑ is a 1-ary distribution containing only one occurrence of X

    Let R := n δP i∈I ai.P1,i , δP i∈I ai.P2,i : P1,i =p ♢ P2,i for all i ∈ I o . For any µ1, µ2 such that µ1 R◦ µ2, we assume that µ1 = ϑ P i∈I ai.P1,i and µ2 = ϑ P i∈I ai.P2,i , where ϑ is a 1-ary distribution containing only one occurrence of X. Observe that if µ1 α − − →ν1, then there exist two 1-ary distri- butions ς1, ς2, i ∈ I and p ∈ [0, 1] such that ...

    work page

  56. [56]

    Note that δL i∈I pi.Pi τ − − →P i∈I piδPi and we have proved that =p ♢ is preserved by convex combinations

    Let R := n δL i∈I pi.Pi , δL i∈I pi.Qi o . Note that δL i∈I pi.Pi τ − − →P i∈I piδPi and we have proved that =p ♢ is preserved by convex combinations. Similarly, we can prove that R ⊆=p ♢. Therefore, (= p ♢)↾RCCS is closed under the probabilistic choice operation. In conclusion, the equality (= p ♢)↾RCCS is preserved by the nondeterministic choice, probab...

    work page

  57. [57]

    If ϑ[µX.τ.S ] α − − →ν, then there exists two 1-ary distributions ς1, ς2 such that ς1 =p ♢ ς2, ν = ς1[µX.τ.S ] and ϑ[µX.τ.T ] α − − →ς2[µX.τ.T ]

    work page

  58. [58]

    Proof of claim

    ϑ[µX.τ.S ](ψL) = ϑ[µX.τ.T ](ψL). Proof of claim. Assume that ϑ[µX.τ.S ] α − − →ν is induced by R ∈ supp(ϑ) such that R[µX.τ.S ] α − − →ρ and ν = ϑ[µX.τ.S ] + ϑ(R)(ρ − δR[µX.τ.S ]). It suffices to prove that there exists two 1-ary distributions ϱ1, ϱ2 such that ϱ1 =p ♢ ϱ2, ρ = ϱ1[µX.τ.S ] and R[µX.τ.T ] α − − →ϱ2[µX.τ.T ], which is standard by induction on...

    work page

  59. [59]

    Then ν1 = ϑ[µX.τ.S ]

    k = 0. Then ν1 = ϑ[µX.τ.S ]. By statement (2), one has that ϑ[µX.τ.S ](ψL) = ϑ[µX.τ.T ](ψL). Hence, ν1(ψL) ≤ sup Oϑ[µX.τ.S] L = χmay L (ϑ[µX.τ.T ]). 30

    work page

  60. [60]

    By statement (1), we can w.l.o.g

    k = i + 1. By statement (1), we can w.l.o.g. assume that ϑ[µX.τ.S ] τ − − →ς1[µX.τ.S ] τ i − − →ν1 and ϑ[µX.τ.T ] τ − − →ς2[µX.τ.T ] for some 1-ary distributions ς1, ς2 such that ς1 =p ♢ ς2. Applying the induction hypothesis to ς1[µX.τ.S ] τ i − − →ν1, we can obtain that ν1(ψL) ≤ sup Oς1[µX.τ.T ] L . Since ς1 =p ♢ ς2, we have ς1[µX.τ.T ] =p ♢ ς2[µX.τ.T ]....

    work page

  61. [61]

    If ϑ[µX.T ] α − − →ν, then there exists a 1-ary distribution ς such that ν = ς[µX.T ] and ϑ[µX.τ.T ] ⇝ α − − → ς[µX.τ.T ]

    work page

  62. [62]

    If ϑ[µX.τ.T ] α − − →ν, then there exists a 1-ary distribution ς such that ν = ς[µX.τ.T ] and ϑ[µX.T ] α − − → ς[µX.T ] or ϑ[µX.T ] ∼† p ς[µX.T ]

    work page

  63. [63]

    Therefore, for any transition sequence ϑ[µX.T ] τ k − − →ν1, we can prove by induction on k that ν1(ψL) ≤ χmay L (ϑ[µX.τ.T ])

    ϑ[µX.τ.T ](ψL) ≤ ϑ[µX.T ](ψL) ≤ χmay L (ϑ[µX.τ.T ]). Therefore, for any transition sequence ϑ[µX.T ] τ k − − →ν1, we can prove by induction on k that ν1(ψL) ≤ χmay L (ϑ[µX.τ.T ]). Hence, by Corollary 7, χmay L (ϑ[µX.T ]) ≤ χmay L (ϑ[µX.τ.T ]). The analog statement in the symmetric case also holds. By Lemma 11, we have µX.T =p ♢ µX.τ.T . □ A.3.10. Proof of...

    work page

  64. [64]

    Now we see that δP ′(ψL) = 1 for some transition sequence δP ⇝ δP ′, and thus χmay L (P ) = 1

    If P ⇓, then there exists P ′ ∈ ψL with P =⇒ P ′. Now we see that δP ′(ψL) = 1 for some transition sequence δP ⇝ δP ′, and thus χmay L (P ) = 1

    work page

  65. [65]

    Consider any transition sequence δP ⇝ ν with witness π, we can prove that supp(ν) ⊆ Reachτ(P ) by induction on the length of π

    If P ̸⇓, then P ′ /∈ ψL for all P ′ with P =⇒ P ′, which implies that Reachτ(P ) ⊆ ψL. Consider any transition sequence δP ⇝ ν with witness π, we can prove that supp(ν) ⊆ Reachτ(P ) by induction on the length of π. Then ν(ψL) =P P ′∈ψL ν(P ′) = 0. Therefore, χmay L (P ) = 0. We then prove the equality for χfair L (P ). There are two possible cases accordi...

    work page

  66. [66]

    According to the above conclusion, χmay L (P ′) = 1 for all P ′ for all P ′ ∈ Reachτ(P )

    If P ⇊, then P ′ ⇓ for all P ′ with P =⇒ P ′. According to the above conclusion, χmay L (P ′) = 1 for all P ′ for all P ′ ∈ Reachτ(P ). Consider any transition sequence δP ⇝ ν. According to Lemma 4, we have χmay L (ν) = X P ′∈supp(ν) ν(P ′)χmay L (P ′) = X P ′∈supp(ν) ν(P ′) · 1 = 1. (A.24) By the arbitrariness of the transition sequences, we have χfair L...

    work page

  67. [67]

    By our first equality, we have χmay L (P ′) = 0

    If P ̸⇊, then P ′ ̸⇓ for some P ′ with P =⇒ P ′. By our first equality, we have χmay L (P ′) = 0. Now we see that χmay L (P ′) = 0 for the transition sequence δP ⇝ δP ′. Thus, χfair L (µ) = 0. □ 31 A.4.2. Proof of Proposition 24 Proof. Define the ∆-lifting of a relation R over PCCS by R∆ := {(δP , δQ) : P R Q}. Then R∆ can be viewed as a relation over D(P...

    work page

  68. [68]

    If R is a ∆-extensional relation on D(PRCCS), then ( ∼† p R ∼ † p)↾CCS is extensional on PCCS

    work page

  69. [69]

    By Lemma 23, we can deduce that (=∆ ♢ )↾CCS is an extensional, equipollent relation onPCCS, which is contained in = ♢

    If E is an extensional equivalence on PCCS then ∼† p E∆ ∼† p is ∆-extensional on D(PRCCS). By Lemma 23, we can deduce that (=∆ ♢ )↾CCS is an extensional, equipollent relation onPCCS, which is contained in = ♢. Again by this lemma, we obtain that ∼† p (=♢)∆ ∼† p is ∆-extensional and probabilistic equipollent and thus contained in = ∆ ♢ . By definition, we ...

    work page

  70. [70]

    By the definition of = may and Lemma 25, we have χmay ω (δP | o) = χmay ω (P | O) = χmay ω (Q | O) = χmay ω (δQ | o)

    Given any P, Q ∈ P CCS such that P =may Q, for any o ∈ ∆(PCCS)ω, it is clear that o = δO for some O ∈ P ω CCS. By the definition of = may and Lemma 25, we have χmay ω (δP | o) = χmay ω (P | O) = χmay ω (Q | O) = χmay ω (δQ | o). Therefore, δP =∆ may δQ holds, which implies = may⊆ (=∆ may)↾CCS

    work page

  71. [71]

    By Lemma 25, P =may Q and thus (=∆ may)↾CCS ⊆=may

    Given any P, Q ∈ P CCS such that P (=∆ may)↾CCS Q and any classical observer O ∈ P ω CCS, the equality χmay ω (P | O) = χmay ω (Q | O) holds by definition. By Lemma 25, P =may Q and thus (=∆ may)↾CCS ⊆=may. Following a similar argument, we can prove that (= ∆ fair)↾CCS = (=fair). □ A.4.4. Proof of Lemma 28 Proof. Assume that µ1 ⇝ ν1 is witnessed by π1 ∈ τ...

    work page

  72. [72]

    Since µ1 ≈p µ2 , µ1(C) = µ2(C) holds for all C ∈ P RCCS / ≈p (see Definition 3), which implies that |µ2 − µ1|≈p = 0

    In the base case |π1| = 0, we have ν1 = µ1. Since µ1 ≈p µ2 , µ1(C) = µ2(C) holds for all C ∈ P RCCS / ≈p (see Definition 3), which implies that |µ2 − µ1|≈p = 0. Now by setting ν2 = µ2, we see that µ2 ⇝ ν2 and |ν2 − ν1|≈p = |µ2 − µ1|≈p = 0, thus the results follows

    work page

  73. [73]

    When |π1| = k + 1, we can divide the transition sequence into µ1 π′ 1 − − →ν′ 1 τ − − →ν1, where π1 = π′ 1 ◦ τ and π′ 1 is a degenerate witness

    Assume that the statements holds for |π1| = k ≥ 0. When |π1| = k + 1, we can divide the transition sequence into µ1 π′ 1 − − →ν′ 1 τ − − →ν1, where π1 = π′ 1 ◦ τ and π′ 1 is a degenerate witness. Since |π′ 1| = k and π′ 1 is a degenerate witness, by the induction hypothesis, for any number ϵ > 0, there exists ν′ 2 such that µ2 ⇝ ν′ 2 and |ν′ 2 − ν′ 1|≈p ≤...

    work page

  74. [74]

    Since |ν′ 2 − ν′ 1|≈p ≤ ϵ, we have |ν′ 2([P ]) − ν′ 1([P ])| ≤ ϵ

    such that P τ − − →ρP and ν1 = ν′ 1 + ν′ 1(P )(ρP − δP ). Since |ν′ 2 − ν′ 1|≈p ≤ ϵ, we have |ν′ 2([P ]) − ν′ 1([P ])| ≤ ϵ. Thus there exists a set of processes {Q1, · · · , Qm} ⊆ supp(ν′

    work page

  75. [75]

    Now consider any process Q ∈ {Q1, · · · , Qm}

    and a number p ∈ (0, 1] such that Qi ∈ [P ] for all i ∈ [m] and |p · (Pm i=1 ν′ 2(Qi)) − ν′ 1(P )| ≤ ϵ. Now consider any process Q ∈ {Q1, · · · , Qm}. Since P ≈p Q and P τ − − →ρP , there exists ρQ ∈ D(PRCCS) such that Q τ =⇒c ρQ and ρP ≈p ρQ. Suppose the weak combined transition Q τ =⇒c ρQ is induced by a scheduler σQ defined on frags∗(Q), we define a se...

    work page

  76. [76]

    Then P2 | Q α =⇒c µ2 := δP2 | ρ

    Q α − − →ρ for some ρ and µ1 = δP1 | ρ. Then P2 | Q α =⇒c µ2 := δP2 | ρ. Since δP1 ≈p δP2, by our claim, we have µ1 E † µ2

    work page

  77. [77]

    Since P1 ≈p P2, there exists ρ2 ∈ D(PRCCS) such that P2 α =⇒c ρ2 and ρ1 ≈p ρ2

    P1 α − − →ρ1 for some ρ1 and µ1 = ρ1 | δQ. Since P1 ≈p P2, there exists ρ2 ∈ D(PRCCS) such that P2 α =⇒c ρ2 and ρ1 ≈p ρ2. Hence, P2 | Q α =⇒c µ2 := ρ2 | δQ and by our claim, µ1 E † µ2 holds

    work page

  78. [78]

    Since P1 ≈p P2, there exists ρ2 ∈ D(PRCCS) such that P2 ℓ =⇒c ρ2 and ρ1 (≈p)† ρ2

    P1 ℓ − − →ρ1, Q ℓ − − →o for some distributions ρ1, o ∈ D(PRCCS) and ℓ ∈ L, µ1 = ρ1 | o ,and α = τ. Since P1 ≈p P2, there exists ρ2 ∈ D(PRCCS) such that P2 ℓ =⇒c ρ2 and ρ1 (≈p)† ρ2. By Lemma 39, we have P2 | Q τ =⇒c µ2 := ρ2 | o. Therefore, µ1 E † µ2. By symmetry, we conclude that E is a probabilistic weak bisimulation, therefore contained in the largest ...

    work page