Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

C. A. Middelburg

TL;DR

The paper addresses how to analyze timing-sensitive communication protocols within ACP by introducing a coarser, dormancy-aware variant of branching bisimilarity that remains faithful in timing-free cases. It develops both time-stamped and two-phase operational semantics, extends ACP with guarded recursion, and provides an axiom schema that captures the difference between standard and dormancy-aware equivalences. The PAR protocol serves as a core application, showing functional correctness under appropriate timing assumptions and enabling thorough performance analysis once internal actions are suitably abstracted away via the new equivalence. The resulting framework combines a time-aware process algebra, a time-free projection, and a two-phase verification approach to yield a practical, robust method for verifying timed protocols and potentially other timing-sensitive systems. The work thus contributes a principled way to separate timing analysis from functional correctness in a rigorous, algebraic setting, with clear implications for protocol design and verification in security and networking domains.

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.

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

TL;DR

The paper addresses how to analyze timing-sensitive communication protocols within ACP by introducing a coarser, dormancy-aware variant of branching bisimilarity that remains faithful in timing-free cases. It develops both time-stamped and two-phase operational semantics, extends ACP with guarded recursion, and provides an axiom schema that captures the difference between standard and dormancy-aware equivalences. The PAR protocol serves as a core application, showing functional correctness under appropriate timing assumptions and enabling thorough performance analysis once internal actions are suitably abstracted away via the new equivalence. The resulting framework combines a time-aware process algebra, a time-free projection, and a two-phase verification approach to yield a practical, robust method for verifying timed protocols and potentially other timing-sensitive systems. The work thus contributes a principled way to separate timing analysis from functional correctness in a rigorous, algebraic setting, with clear implications for protocol design and verification in security and networking domains.

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.

Paper Structure

This paper contains 20 sections, 18 theorems, 22 equations, 4 figures, 8 tables.

Table of Contents

  1. Introduction
  2. Process Algebraic Preliminaries
  3. ACP$_\mathrm{drt}^\tau$
  4. ACP$_\mathrm{drt}^\tau$ with Guarded Recursion
  5. Time-free projection
  6. The PAR Protocol
  7. Informal Description of the PAR Protocol
  8. Formal Specification of the PAR Protocol
  9. Analysis of the PAR Protocol: Expansion
  10. Analysis of the PAR Protocol: Abstraction
  11. The Standard Version of Branching Bisimilarity
  12. A Definition Referring to a Two-Phase Semantics
  13. Properties of Rooted Branching Bisimilarity
  14. A Definition Referring to a Time-Stamped Semantics
  15. A Coarser Version of Branching Bisimilarity
  16. ...and 5 more sections

Key Result

theorem thmcountertheorem

For each closed ACP$_\mathrm{drt}^\tau$ term $t$, there exists a basic term $t' \in \mathcal{B}$ such that $t = t'$ is derivable from the axioms of ACP$_\mathrm{drt}^\tau$.

Figures (4)

  • Figure 1: Connection diagram for PAR protocol
  • Figure 2: Graphical two-phase presentation of two processes
  • Figure 3: Graphical time-stamped presentation of two processes
  • Figure 4: Graphical two-phase and time-stamped presentation of one process

Theorems & Definitions (35)

  • theorem thmcountertheorem: Elimination
  • proof
  • theorem thmcountertheorem: Standard Concurrency
  • proof
  • theorem thmcountertheorem: Expansion
  • proof
  • theorem thmcountertheorem
  • proof
  • theorem thmcountertheorem: Equivalence
  • proof
  • ...and 25 more