Abstract
A variant of the standard notion of branching bisimilarity for processes
with discrete relative timing is proposed which is coarser than the
standard notion.
Using a version of ACP (Algebra of Communicating Processes) with
abstraction for processes with discrete relative timing, it is shown
that the proposed variant allows of both the functional correctness and
the performance properties of the PAR (Positive Acknowledgement with
Retransmission) protocol to be analyzed.
In the version of \ACP\ concerned, the difference between the standard
notion of branching bisimilarity and its proposed variant is
characterized by a single axiom schema.