Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Concrete Branching Bisimilarity for Processes with Time-outs

Gaspard Reghem, Rob van Glabbeek

TL;DR

The paper advances branching bisimilarity for reactive systems with time-outs by introducing concrete branching reactive bisimilarity that treats time-out transitions as visible actions, avoiding elision of time-outs. It provides a modal characterisation, rooted and generalised forms, and shows that rooted concrete branching time-out bisimilarity is a full congruence for the CCSP$^\theta_t$ language. A complete axiomatisation is given for strongly guarded processes, employing RDP/RSP, branching and reactive-approximation principles, plus canonical representatives to handle infinite cases. Together, these results enable rigorous verification of timed reactive systems within an untimed process-algebraic framework, with preserveability under recursion and environment-driven timing semantics.

Abstract

This paper provides an adaptation of branching bisimilarity to reactive systems with time-outs that does not enable eliding of time-out transitions. Multiple equivalent definitions are procured, along with a modal characterisation and a proof of its congruence property for a standard process algebra with recursion. The last section presents a complete axiomatisation for guarded processes without infinite sequences of unobservable actions.

Concrete Branching Bisimilarity for Processes with Time-outs

TL;DR

The paper advances branching bisimilarity for reactive systems with time-outs by introducing concrete branching reactive bisimilarity that treats time-out transitions as visible actions, avoiding elision of time-outs. It provides a modal characterisation, rooted and generalised forms, and shows that rooted concrete branching time-out bisimilarity is a full congruence for the CCSP language. A complete axiomatisation is given for strongly guarded processes, employing RDP/RSP, branching and reactive-approximation principles, plus canonical representatives to handle infinite cases. Together, these results enable rigorous verification of timed reactive systems within an untimed process-algebraic framework, with preserveability under recursion and environment-driven timing semantics.

Abstract

This paper provides an adaptation of branching bisimilarity to reactive systems with time-outs that does not enable eliding of time-out transitions. Multiple equivalent definitions are procured, along with a modal characterisation and a proof of its congruence property for a standard process algebra with recursion. The last section presents a complete axiomatisation for guarded processes without infinite sequences of unobservable actions.
Paper Structure (27 sections, 34 theorems, 7 equations, 3 figures, 4 tables)

This paper contains 27 sections, 34 theorems, 7 equations, 3 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Branching Reactive Bisimilarity
  3. Rooted Version
  4. Alternative Forms of Definition \ref{['def:intuitive']}
  5. Modal Characterisation
  6. Process Algebra and Congruence
  7. Time-out Bisimulation
  8. Congruence
  9. Axiomatisation
  10. Recursive Principles
  11. Axioms and Soundness
  12. Completeness
  13. Canonical Representative
  14. Examples
  15. Generalised concrete branching reactive bisimulation
  16. ...and 12 more sections

Key Result

Lemma 2

Let $\R$ be a concrete branching reactive bisimulation.

Figures (3)

  • Figure 1: Operational semantics of $\hbox{CCSP}^\theta_t$
  • Figure 2: Counter-Example to a Naive Clause 1.a.
  • Figure 3: Counter-Example to the Absence of a Stability Respecting Clause

Theorems & Definitions (55)

  • Definition 1
  • Lemma 2
  • Lemma 3: Stuttering Lemma
  • Proposition 4
  • Definition 5
  • Proposition 6
  • Definition 7
  • Definition 8
  • Definition 9
  • Definition 10
  • ...and 45 more