Branching Bisimilarity for Processes with Time-outs

TL;DR

This paper adapts branching bisimilarity to reactive systems with time-outs, providing multiple definitions, modal characterisation, and a complete axiomatisation for guarded processes, ensuring congruence and formal reasoning capabilities.

Contribution

It introduces a novel adaptation of branching bisimilarity for systems with time-outs, including definitions, modal characterisation, and axiomatisation, advancing formal analysis tools.

Findings

Multiple equivalent definitions of the adapted bisimilarity.

A modal characterisation of the adapted bisimilarity.

A complete axiomatisation for guarded processes without infinite unobservable actions.

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.