Vertical Bisimulation

Arend Rensink, Roberto Gorrieri

    Research output: Book/ReportReportOther research output

    45 Downloads (Pure)


    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.
    Original languageUndefined
    Place of PublicationHildesheim
    PublisherUniversity of Hildesheim
    Number of pages57
    Publication statusPublished - Sept 1995

    Publication series

    NameHildesheimer Informatikbericht
    PublisherInstitut für Informatik, University of Hildesheim
    ISSN (Print)0941-3014


    • IR-66677
    • EWI-8320

    Cite this