Bisimulation semantics for concurrency with atomicity and action refinement

J.W. Bakker, de, E.P. Vink, de

    Research output: Contribution to journalArticleAcademicpeer-review

    8 Citations (Scopus)

    Abstract

    A comparative semantic study is made of two notions in concurrency, viz. atomicity and action refinement. Parallel composition is modeled by interleaving, and refinement is taken in the version where actions are refined by atomized statements. The bisimulation domain used in the semantic definitions is obtained as solution of a system of domain equations over complete metric spaces. Both operational and denotational models are developed, and their equivalence is established using higher-order techniques and Banach's fixed point theorem. The operational semantics for refinement is based on transition rules rather than on some form of syntactic substitution.
    Original languageEnglish
    Pages (from-to)3-34
    JournalFundamenta Informaticae
    Volume20
    Issue number1-3
    Publication statusPublished - 1994

    Fingerprint

    Dive into the research topics of 'Bisimulation semantics for concurrency with atomicity and action refinement'. Together they form a unique fingerprint.

    Cite this