ON REDUCTION-BASED PROCESS SEMANTICS

A formulation of semantic theories for processes which does not rely on the notion of observables or convergence is studied. The new construction is based solely on a reduction relation and equational reasoning, but can induce meaningful theories for processes, both in weak and strong settings. The resulting theories in many cases coincide with, and sometimes generalise, observation-based formulation of behavioural equivalence. The basic construction of reduction-based theories is studied, taking a simple name passing calculus (called nu-calculus) and its extensions as an example. Results concerning the application of our construction to other calculi are also briefly discussed.