  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.

Logic in Computer Science