Processes as Terms: Non-Well-Founded Models for Bisimulation

摘要

A compositional semantics characterizing bisimulation equivalence is derived fromtransition system specifications in the Structural Operational Semantics (SOS) style, satisfying certain syntactic conditions. Aczel's nonstandard set theory is used for solving a recursive equation for a domain of processes. It contains non well founded elements modeling possibly infinite behavior. Semantic interpretations of syntactic operators are obtained by defining the operational semantics for terms consisting of both syntactic and semantic (processes) entities. It is possible to return to standard set theory by observing that a similar though less general result can be obtained with the use of complete metric spaces.