A compositional semantics characterizing bisimulation equivalence is derived from transition system specifications in the SOS style, satisfying certain syntactic syntactic conditions. We use Aczel's nonstandard set theory for solving a recursive equation for a domain fo processes. It contains non-well-founded elements modelling possibly infinite behaviour. Semantic interpretations of syntactic operators are obtained by defining the operational semantics for terms consisting of both syntactic and semantic (processes)entities. Finally, we return to standard set theory by observing that a similar, though less general, result can be obtained with the use of complete metric spaces.
Mathematical Structures in Computer Science