Vertical Bisimulation

We investigate criteria to relate specifications and implementations belonging to conceptually different abstraction levels, and propose vertical bisimulation as a candidate relation for this purpose. Vertical bisimulation is indexed by a function mapping abstract actions onto concrete processes, which lays down the basic connection between the levels. Vertical bisimulation is compatible with the standard interleaving semantics; in fact, if the refinement function is the identity, then vertical bisimulation collapses to the standard notion of rooted bisimulation. We prove that vertical bisimulation satisfies a number of congruence-like proof rules (notably a structural one for recursion) that offer a powerful, compositional proof technique to verify whether a certain process is an implementation for some specification. We give a number of small examples to demonstrate the advantages of this approach.