A compositional protocol verification using relativized bisimulation

  • Larsen K
  • Milner R
  • 3


    Mendeley users who have this article in their library.
  • 17


    Citations of this article.


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.

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • Kim G. Larsen

  • Robin Milner

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free