Concrete Branching Bisimilarity for Processes with Time-outs
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.
Keywords
Cite
@article{arxiv.2412.19805,
title = {Concrete Branching Bisimilarity for Processes with Time-outs},
author = {Gaspard Reghem and Rob van Glabbeek},
journal= {arXiv preprint arXiv:2412.19805},
year = {2024}
}
Comments
Whereas the bisimilarity of arXiv:2408.10117 elides timeouts, just like branching bisimilarity elides $\tau$-transitions, the one of this paper instead treats time-outs more like visible actions. We obtained this paper from arXiv:2408.10117 by systemically suppressing this eliding feature, thereby obtaining simpler definitions and proofs. arXiv admin note: substantial text overlap with arXiv:2408.10117