Vertical Bisimulation


Rensink, Arend and Gorrieri, Roberto (1995) Vertical Bisimulation. [Report]

open access
Abstract: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.
Item Type:Report
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page