Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
An approach to the semantics of CCS-like communicating processes is proposed that is based upon evaluation of processes to input- or output-committed form, with no explicit mention of silent actions. This leads to a co-inductively defined notion of evaluation bisimilarity---a form of weak branching-time equivalence which is shown to be a congruence, even in the presence of summation. The relationship between this evaluation-based approach and the more traditional, labelled transition semantics is investigated. In particular, with some restriction on sums, CCS observation equivalence is characterised purely in terms of evaluation to committed form, and evaluation bisimilarity is characterised as a weak delay equivalence. These results are extended to the higher order case, where evaluation bisimilarity coincides with Sangiorgi's weak context bisimilarity. An evaluation-based approach to pi-calculus and the relationship with Milner and Sangiorgi's reduction-based notion of barbed bisimulation are also examined.