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 the functional correctness of the
PAR (Positive Acknowledgement with Retransmission) protocol as well as
its performance properties to be analyzed.
In the version of ACP concerned, the difference between the standard
notion and its proposed variant is characterized by a single axiom
schema.