Reactive Bisimulation Semantics for a Process Algebra with Time-Outs
Rob van Glabbeek
TL;DR
This paper develops a reactive bisimulation semantics for a process algebra with time-outs, providing modal characterisation, congruence results, and a complete axiomatisation to analyze timed process behaviors.
Contribution
It introduces a novel reactive bisimulation semantics for timed process algebra, including modal characterisation, congruence proofs, and a complete axiomatisation, extending traditional bisimulation concepts.
Findings
Reactive bisimulation semantics successfully characterises process equivalence with time-outs.
The approach supports congruence results for process algebra with recursion.
A complete axiomatisation for the semantics is provided.
Abstract
This paper introduces the counterpart of strong bisimilarity for labelled transition systems extended with time-out transitions. It supports this concept through a modal characterisation, congruence results for a standard process algebra with recursion, and a complete axiomatisation.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Advanced Software Engineering Methodologies