Results on embeddings between state-based and event-based systems

M.A. Reniers, R.J.A. Schoren, T.A.C. Willemse

Research output: Contribution to journalArticleAcademicpeer-review

7 Citations (Scopus)
5 Downloads (Pure)

Abstract

Kripke Structures (KSs) and Labelled Transition Systems (LTSs) are the two most prominent semantic models used in concurrency theory. Both models are commonly believed to be equi-expressive. One can find manyad hoc embeddings of one of these models into the other. We build upon the seminal work of De Nicola and Vaandrager that firmly established the correspondence between stuttering equivalence in KSs and divergence-sensitive branching bisimulation in LTSs. We show that their embeddings can also be used for a range of other equivalences of interest, such as strong bisimilarity, simulation equivalence and trace equivalence. Furthermore, we extend the results by De Nicola and Vaandrager by showing that there are additional translations that allow one to use minimization techniques in one semantic domain to obtain minimal representatives in the other semantic domain for these equivalences.
Original languageEnglish
Pages (from-to)73-92
JournalThe Computer Journal
Volume57
Issue number1
DOIs
Publication statusPublished - 2014

Fingerprint Dive into the research topics of 'Results on embeddings between state-based and event-based systems'. Together they form a unique fingerprint.

  • Cite this