Vertical Implementation

Arend Rensink, Roberto Gorrieri

    Research output: Contribution to journalArticleAcademicpeer-review

    16 Citations (Scopus)
    51 Downloads (Pure)

    Abstract

    We investigate criteria to relate specifications and implementations belonging to conceptually different levels of abstraction. For this purpose, we introduce the generic concept of a vertical implementation relation, which is a family of binary relations indexed by a refinement function that maps abstract actions onto concrete processes and thus determines the basic connection between the abstraction levels. If the refinement function is the identity, the vertical implementation relation collapses to a standard (horizontal) implementation relation. As desiderata for vertical implementation relations we formulate a number of congruence-like proof rules (notably a structural rule for recursion) that offer a powerful, compositional proof technique for vertical implementation. As a candidate vertical implementation relation we propose vertical bisimulation. Vertical bisimulation is compatible with the standard interleaving semantics of process algebra; in fact, the corresponding horizontal relation is rooted weak bisimulation. We prove that vertical bisimulation satisfies the proof rules for vertical implementation, thus establishing the consistency of the rules. Moreover, we define a corresponding notion of abstraction that strengthens the intuition behind vertical bisimulation and also provides a decision algorithm for finite-state systems. Finally, we give a number of small examples to demonstrate the advantages of vertical implementation in general and vertical bisimulation in particular.
    Original languageEnglish
    Article number10.1006/inco.2001.2967
    Pages (from-to)95-133
    Number of pages39
    JournalInformation and computation
    Volume170
    Issue number1
    DOIs
    Publication statusPublished - 2001

    Fingerprint Dive into the research topics of 'Vertical Implementation'. Together they form a unique fingerprint.

    Cite this