Abstract
We propose a variant of the version of branching bisimulation
equivalence for processes with discrete relative timing from Baeten,
Bergstra, and Reniers.
We show that this new equivalence allows for the functional correctness of the PAR protocol as well as its performance properties
to be analyzed.
The new equivalence still coincides with the original version of
branching bisimulation equivalence from van Glabbeek and Weijland in
the case without timing.
Electronic version.