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

TL;DR

The paper delivers a complete equational characterization of rooted branching bisimilarity for a minimal, non-recursive process language with both nondeterministic and probabilistic choice. It first establishes completeness for the nondeterministic fragment using concrete processes to bridge to strong bisimilarity, then extends the framework to probabilistic processes by introducing a distribution-based rooted branching probabilistic bisimulation and a corresponding axiom system $ extit{AX}^b_p$ with BP and G. The probabilistic completeness is achieved by reducing to strong probabilistic bisimilarity and proving congruence for probabilistic choice, yielding a sound and complete theory for reasoning about branching behaviour under both nondeterministic and probabilistic effects. This delivers a principled foundation for equational reasoning in probabilistic process languages and suggests practical avenues for algorithmic minimization and future extensions to parallelism and recursion.

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.

Figures (1)

• Figure 1: Probabilistic automaton of EHKTZ13:qest