A Cancellation Law for Probabilistic Processes

Rob van Glabbeek (Corresponding author), Jan Friso Groote, Erik de Vink

Onderzoeksoutput: Bijdrage aan tijdschriftCongresartikelpeer review

5 Downloads (Pure)


We show a cancellation property for probabilistic choice. If µ ⊕ ρ and ν ⊕ ρ are branching probabilistic bisimilar, then µ and ν are also branching probabilistic bisimilar. We do this in the setting of a basic process language involving non-deterministic and probabilistic choice and define branching probabilistic bisimilarity on distributions. Despite the fact that the cancellation property is very elegant and concise, we failed to provide a short and natural combinatorial proof. Instead we provide a proof using metric topology. Our major lemma is that every distribution can be unfolded into an equivalent stable distribution, where the topological arguments are required to deal with uncountable branching.

Originele taal-2Engels
Pagina's (van-tot)42-58
Aantal pagina's17
TijdschriftElectronic Proceedings in Theoretical Computer Science, EPTCS
StatusGepubliceerd - 14 sep. 2023
EvenementCombined 30th International Workshop on Expressiveness in Concurrency and 20th Workshop on Structural Operational Semantic, EXPRESS/SOS 2023 - Antwerp, België
Duur: 18 sep. 202318 sep. 2023


Supported by Royal Society Wolfson Fellowship RSWF\R1\221008

Royal Dutch Chemical SocietyRSWF\R1\221008


    Duik in de onderzoeksthema's van 'A Cancellation Law for Probabilistic Processes'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit