Rooted Divergence-Preserving Branching Bisimilarity is a Congruence

TL;DR

This paper proves that rooted divergence-preserving branching bisimilarity remains a congruence within a specific process language, ensuring compositional reasoning in process algebra.

Contribution

It establishes that rooted divergence-preserving branching bisimilarity is a congruence for a process language with nil, action prefix, choice, and recursion.

Findings

Rooted divergence-preserving branching bisimilarity is a congruence.

The result applies to a process language with recursion.

Ensures compositional reasoning in process algebra.

Abstract

We prove that rooted divergence-preserving branching bisimilarity is a congruence for the process specification language consisting of nil, action prefix, choice, and the recursion construct.