Deriving denotational models for bisimulation from structured operational semantics
Jan J. M. M. Rutten · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1989
We take as a starting point the notion of labelled transition system (L TS) in the style of the Structured Operational Semantics of Plotkin.Every L TS gives rise to a model that maps the states of the L TS (usually terms over some signature) to a representation of their bisimulation equivalence class, namely a so-called process.(Such a model is often called operational.)These processes are elements of a metric domain which was first introduced by De Bakker and Zucker.Next we show how the transition system specification (a set of rules for deriving transitions) by which the L TS is defined, induces a denotational model, given that it satisfies certain syntactic restrictions.Finally we prove that both models are equal by showing that they are fixed points of the same contraction , which has a unique fixed point by Banach's Theorem.