A compositional protocol verification using relativized bisimulation

Citations of this article
Mendeley users who have this article in their library.


The purpose of this paper is to illustrate a compositional proof method for communicating systems; that is, a method in which a property P of a complete system is demonstrated by first decomposing the system, then demonstrating properties of the subsystems which are strong enough to entail property P for the complete system. In any compositional proof method, it is essential that one can abstract away the behavioural aspects of the subsystem which are irrelevant in the context of the complete system. Our method is an extension of the well established notion of bisimulation; it is called relative bisimulation, and was developed specifically to allow for such abstractions. We illustrate the method in a proof of correctness for a version of the Alternating Bit Protocol. © 1992.




Larsen, K. G., & Milner, R. (1992). A compositional protocol verification using relativized bisimulation. Information and Computation. https://doi.org/10.1016/0890-5401(92)90025-B

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free