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.

翻译：提出了一种针对具有离散相对定时的过程的标准分支双相似性概念的变体，该变体比标准概念更粗粒度。通过使用一种带有抽象机制的离散相对定时过程通信代数（ACP）版本，证明所提出的变体能够同时分析PAR（带重传的肯定确认）协议的功能正确性和性能属性。在所涉及的ACP版本中，标准分支双相似性概念与其提出的变体之间的差异通过单一公理模式进行了刻画。