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

TL;DR

This paper develops a complete axiomatization for branching bisimilarity in a simple process language that includes both non-deterministic and probabilistic choices, providing a formal foundation for reasoning about such processes.

Contribution

It introduces a new axiomatization for rooted branching probabilistic bisimilarity and proves its completeness, extending previous work on probabilistic process equivalences.

Findings

The axiomatization is complete for the probabilistic process language.

The approach generalizes from non-deterministic to probabilistic choices.

The proof leverages the completeness of strong probabilistic bisimilarity.

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 $\tau$-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.