Trustworthy Systems

A complete axiomatization of branching bisimilarity for a simple process language with probabilistic choice

Authors

Rob van Glabbeek, Jan Friso Groote and Erik de Vink

DATA61

Technical University of Eindhoven

UNSW Sydney

Abstract

This paper proposes a notion of branching bisimilarity for non-deterministic probabilistic processes. In order to characterize the corresponding notion of rooted branching probabilistic bisimilarity, an equational theory is proposed for a basic, recursion-free process language with non-deterministic as well as probabilistic choice. The proof of completeness of the axiomatization builds on the completeness of strong probabilistic bisimilarity on the one hand and on the notion of a concrete process, i.e. a process that does not display (partially) inert τ-moves, on the other hand. The approach is first presented for the non-deterministic fragment of the calculus and next generalized to incorporate probabilistic choice, too.

BibTeX Entry

  @inproceedings{vanGlabbeek_Gd_19,
    address          = {Paris},
    author           = {van Glabbeek, Robert and Groote, Jan Friso and de Vink, Erik},
    booktitle        = {The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and
                        Privacy --- Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday},
    date             = {2019-11-4},
    doi              = {https://doi.org/10.1007/978-3-030-31175-9\_9},
    editor           = {{M.S. Alvim, K. Chatzikokolakis, C. Olarte \& F. Valencia}},
    keywords         = {Process algebra; probabilistic processes; nondeterminism; branching bisimulation; complete
                        axiomatisation},
    month            = nov,
    pages            = {139-162},
    paperurl         = {https://trustworthy.systems/publications/full_text/vanGlabbeek_Gd_19.pdf},
    publisher        = {Springer},
    series           = {LNCS 11760},
    title            = {{A} Complete Axiomatization of Branching Bisimilarity for a Simple Process Language with
                        Probabilistic Choice},
    volume           = {11760},
    year             = {2019}
  }

Download