Back to University of Twente portal
Vertical Bisimulation
Rensink, Arend and Gorrieri, Roberto (1995) Vertical Bisimulation. [Report]
![[img]](http://doc.utwente.nl/style/images/fileicons/application_pdf.png)
| PDF 578Kb |
| 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: | http://purl.utwente.nl/publications/66677 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page