A new equivalence for processes with timing. With an application to protocol verification

We propose a variant of the version of branching bisimilation 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 Glabbeek and Weijland in the case without timing