Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Branching Bisimilarity for Processes with Time-outs

Gaspard Reghem, Rob van Glabbeek

TL;DR

The paper develops branching reactive bisimilarity for reactive systems with time-outs, integrating time-elapse semantics and environment-triggered actions. It provides a modal characterisation via an extended Hennessy–Milner logic, proves full congruence results for a CCSP$^\theta_t$-like language, and offers complete axiomatisations for guarded processes. Key contributions include rooted variants, multiple equivalent definitions, and a canonical-representative method to achieve completeness for complex recursive specifications. These results enable algebraic verification and equational reasoning about time-out aware reactive systems with concurrency and recursion.

Abstract

This paper provides an adaptation of branching bisimilarity to reactive systems with time-outs. 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.

Branching Bisimilarity for Processes with Time-outs

TL;DR

The paper develops branching reactive bisimilarity for reactive systems with time-outs, integrating time-elapse semantics and environment-triggered actions. It provides a modal characterisation via an extended Hennessy–Milner logic, proves full congruence results for a CCSP-like language, and offers complete axiomatisations for guarded processes. Key contributions include rooted variants, multiple equivalent definitions, and a canonical-representative method to achieve completeness for complex recursive specifications. These results enable algebraic verification and equational reasoning about time-out aware reactive systems with concurrency and recursion.

Abstract

This paper provides an adaptation of branching bisimilarity to reactive systems with time-outs. 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 (29 sections, 35 theorems, 7 equations, 3 figures, 4 tables)

This paper contains 29 sections, 35 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. Concrete Time-out Version
  16. ...and 14 more sections

Key Result

Lemma 2

Let $\R$ be a 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 (56)

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