摘要：This is the second of two companion papers on a semantic theory for communicating processes with values based on the late approach. In the first one, [Ing95], we explained the general idea of the late semantic approach. Furthermore we introduced a general syntax for value-passing process algebra based on the late approach and a general class of denotational models for these languages in the Scott-Strachey style. Then we defined a concrete language, CCSL, which is an extension of the standard CCS with values according to the late approach. We also provided a denotational model for it, which is an instantiation of the general class. This model is a direct extension of the model given by Abramsky [Abr91] to model the pure calculus SCCS. Furthermore we gave an axiomatic semantics by means of a proof system based on inequations and proved its soundness and completeness with respect to the denotational semantics. In this paper we will give a behavioural semantics to the language CCSL in terms of a Plotkin style operational semantics and a bisimulation based preorder. Our main aim is to relate the behavioural view of processes we present here to the domain-theoretical one developed in the companion paper [Ing95]. In the Scott-Strachey approach an infinite process is obtained as a chain of finite and possibly partially specified processes. The completely unspecified process is given by the bottom element of the domain. An operational interpretation of this approach is to take divergence into account and give the behavioural semantics in terms of a prebisimulation or bisimulation preorder [Hen81,Wal90] rather than by the standard bisimulation equivalence [Par81, Mil83]. One of the results in the pure case presented in [Abr91] is that the denotational model given in that reference is fully abstract with respect to the "finitely observable" part of the bisimulation preorder but not with respect to the bisimulation preorder which turns out to be too fine. Intuitively this is due to the algebraicity of the model and the fact that the finite elements in the model are denotable by syntactically finite terms. The algebraicity implies that the denotational semantics of a process is completely decided by the semantics of its syntactically finite approximations, whereas the same can not be said about the bisimulation preorder. In fact we need experiments of an infinite depth to investigate bisimulation while this is not the case for the preorder induced by the model as explained above. An obvious consequence of this observation is that in general, a bisimulation preorder can not be expected to be modeled by an algebraic cpo given that the compact elements are denotable by syntactically nite elements. In [Hen81] Hennessy defined a term model for SCCS. This model is !- algebraic and fails to be fully abstract with respect to the strong bisimulation preorder. In the same paper the author introduces the notion of "the finitary part of a relation" and "a finitary relation". The finitary part of a relation R over processes, denoted by RF , is defined by pRF q i 8d:dRp) dRq where d ranges over the set of syntactically finite processes. A relation R is finitary if RF = R. Intuitively this property may be interpreted as algebraicity at the behavioural level provided that syntactically nite terms are interpreted as compact elements in the denotational model; if a relation is nitary then it is completely decided by the syntactically nite elements. In both [Hen81] and [Abr91] the full abstractness of the respective denotational semantics with respect to < F is shown. In [Abr91] it is also shown that if the language is sort nite and satises a kind of nite branching condition, then
