A Complete Axiomatization of Branching Bisimilarity for a Simple Process Language with Probabilistic Choice

• DOI: 10.48550/arxiv.2502.05631
• Publication Date: 2025-02-08
• Authors: Rob van Glabbeek; Jan Friso Groote; E.P. de Vink
• Keywords: Branching (polymer chemistry); Branching process

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