## A Complete Protocol Verification using Relativized
Bisimulation

**K.G. Larsen and R. Milner**
*Abstract:* 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 demonsrating 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 express the behavioural constraint which is imposed
upon each subsystem by the others, since it may be difficult to
demonstrate a suitable property of the subsystem's behaviour in the
absence of the constraint.

Our method is an extension of the well established notion of
bisimulation; it is called *relative bisimulation*, and was
developed specifically to express the behavioural constraints
between subsystems. We illustrate the method in a proof of
correctness for a version of the Alternating Bit Protocol.

*LFCS report ECS-LFCS-86-13*

Previous |

Index |

Next