Folk theorems on the correspondence between state-based and event-based systems

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

13 Citations (Scopus)


Kripke Structures and Labelled Transition Systems are the two most prominent semantic models used in concurrency theory. Both models are commonly believed to be equi-expressive. One can find many ad-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 Kripke Structures and divergence-sensitive branching bisimulation in Labelled Transition Systems. 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 minimisation techniques in one semantic domain to obtain minimal representatives in the other semantic domain for these equivalences.
Original languageEnglish
Title of host publicationSOFSEM 2011: Theory and Practice of Computer Science (37th Conference on Currents Trends, Novy Smokovec, Slovakia, January 22-28, 2011. Proceedings)
EditorsI. Cerná, T. Gyimóthy, J. Hromkovic, K. Jeffery, R. Kralovic, M. Vukolic, S. Wolf
Place of PublicationBerlin
ISBN (Print)978-3-642-18380-5
Publication statusPublished - 2011

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743

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

Cite this