A Complete Axiomatization of Branching Bisimilarity for a Simple Process Language with Probabilistic Choice
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.
Keywords
Cite
@article{arxiv.2502.05631,
title = {A Complete Axiomatization of Branching Bisimilarity for a Simple Process Language with Probabilistic Choice},
author = {Rob van Glabbeek and Jan Friso Groote and Erik de Vink},
journal= {arXiv preprint arXiv:2502.05631},
year = {2025}
}
Comments
Written in 2019. Dedicated to Catuscia Palamidessi, on the occasion of her 60th birthday. Extended abstract in 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, LNCS 11760, Springer, 2019, pp. 139-162, doi:10.1007/978-3-030-31175-9_9