Dormancy-aware timed branching bisimilarity, with an application to communication protocol analysis

TL;DR

This paper introduces a new, coarser variant of branching bisimilarity for timed processes, enabling more effective analysis of protocol correctness and performance within an algebraic framework.

Contribution

It proposes a dormancy-aware timed branching bisimilarity and demonstrates its application to analyzing communication protocols using an adapted ACP framework.

Findings

The new bisimilarity simplifies protocol analysis.

It accurately captures both correctness and performance aspects.

A single axiom schema characterizes the difference from standard bisimilarity.

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.