Concrete 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, ensuring congruence and handling guarded processes without infinite unobservable actions.

Contribution

It introduces a novel adaptation of branching bisimilarity for systems with time-outs, including modal characterisation and a complete axiomatisation.

Findings

Multiple equivalent definitions of the adapted bisimilarity

Modal characterisation established

Complete axiomatisation for guarded processes

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.