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.
CITATION STYLE
van Glabbeek, R. J., Groote, J. F., & de Vink, E. P. (2019). A Complete Axiomatization of Branching Bisimilarity for a Simple Process Language with Probabilistic Choice: (Extended Abstract). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11760 LNCS, pp. 139–162). Springer Verlag. https://doi.org/10.1007/978-3-030-31175-9_9
Mendeley helps you to discover research relevant for your work.