### A Semantic Theory for Value–Passing Processes Late Approach Part II: A Behavioural Semantics and Full Abstractness

#### Abstract

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 <F=< !, where < ! is the strong bisimulation preorder induced by experiments

of nite depth, i.e. the preorder is obtained by iterated application of the

functional that denes the bisimulation. Note that in general the preorder < is

strictly ner than the preorder < !. However if the transition system is image

nite, i.e. if the number of arcs leading from a xed state and labelled with a

xed action is nite, then these two preorders coincide.

As mentioned above the main aim of this paper is to give a bisimulation

based behavioural semantics for our language CCSL from [Ing95]. To reflect the

late approach the operational semantics will be given in terms of an applicative

transition system, a concept that is a modication of that dened in [Abr90].

We generalize the notion of bisimulation [Par81, Mil83] to be applied to applicative

transition systems and introduce a preorder motivated by Abramsky's

applicative bisimulation [Abr90]. For this purpose we rst introduce the notion

of strong applicative prebisimulation and the corresponding strong applicative

bisimulation preorder. Following the standard practice this preorder is obtained

as the largest xed point of a suitably dened monotonic functional. We show

by an example that this preorder is not nitary in the sense described above

and is strictly ner than the preorder induced by the model.

Next we dene the strong applicative !-bisimulation preorder in the standard

way by iterative application of the functional that induces the bisimulation

preorder. This gives as a result a preorder which still is too ne to match thepreorder induced by the denotational model. This will be shown by an example.

Intuitively the reason for this is that we still need innite experiments to

decide the operational preorder, now because of an innite breadth due to the

possibility of an innite number of values that have to be checked.

Then we give a suitable denition of the notion of the \nitary part" of

the bisimulation preorder to meet the preorder induced by the denotational

model. We recall that in [Ing95] we dened the so-called compact terms as

the syntactically nite terms which only use a nite number of values in a nontrivial

way. We also showed that these terms correspond exactly to the compact

elements in the denotational model in the sense that an element in the model

is compact if and only if it can be denoted by a compact term. This motivates

a denition of the nitary part, <

F , of the bisimulation preorder < by

p <

F q i 8c: c < p ) c < q

where c ranges over the set of syntactically compact terms. We also dene

yet another preorder, <

f

!, a coarser version of < ! in which we only consider a

nite number of values at each level in the iterative denition of the preorder.

Here it is vital that the set of values is countable and can be enumerated as

V al = fv1; v2; g. Thus in the denition of <

f

1 we only test whether the

dening constraints of the preorder hold when the only possible input and

output value is v1, and in general in the denition of <

f

n we test the constraints

for the rst n values only. (Here we would like to point out that this idea

originally appears in [HP80].) It turns out that <

f

! is the nitary part of <

in our new sense and that the model is fully abstract with respect to <

f

!. We

will prove both these results in this paper using techniques which are similar

to those used by Hennessy in the above mentioned reference [Hen81].

The structure of the paper is as follows: In Section 2 we give a short survey of

the result from the companion paper [Ing95] needed in this study. The denition

of the operational semantics and the notion of applicative bisimulation are the

subject of Section 3. Section 4 is devoted to the analysis of the preorder and the

denition of the value-nitary preorder <

f

!. In Section 5 we give a denition of

the notion of nitary part of a relation and a nitary relation over processes. In

the same section we prove that the preorder <

f

! is nitary and that it coincides

with the nitary part of the preorder < . Finally we prove the soundness and

the completeness of the proof system with respect to the resulting preorder.

The full abstractness of the denotational semantics for CCSL, given in [Ing95],

then follows from the soundness and the completeness of the proof system with

respect to the denotational semantics. In Section 6 we give some concluding

remarks.

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 <F=< !, where < ! is the strong bisimulation preorder induced by experiments

of nite depth, i.e. the preorder is obtained by iterated application of the

functional that denes the bisimulation. Note that in general the preorder < is

strictly ner than the preorder < !. However if the transition system is image

nite, i.e. if the number of arcs leading from a xed state and labelled with a

xed action is nite, then these two preorders coincide.

As mentioned above the main aim of this paper is to give a bisimulation

based behavioural semantics for our language CCSL from [Ing95]. To reflect the

late approach the operational semantics will be given in terms of an applicative

transition system, a concept that is a modication of that dened in [Abr90].

We generalize the notion of bisimulation [Par81, Mil83] to be applied to applicative

transition systems and introduce a preorder motivated by Abramsky's

applicative bisimulation [Abr90]. For this purpose we rst introduce the notion

of strong applicative prebisimulation and the corresponding strong applicative

bisimulation preorder. Following the standard practice this preorder is obtained

as the largest xed point of a suitably dened monotonic functional. We show

by an example that this preorder is not nitary in the sense described above

and is strictly ner than the preorder induced by the model.

Next we dene the strong applicative !-bisimulation preorder in the standard

way by iterative application of the functional that induces the bisimulation

preorder. This gives as a result a preorder which still is too ne to match thepreorder induced by the denotational model. This will be shown by an example.

Intuitively the reason for this is that we still need innite experiments to

decide the operational preorder, now because of an innite breadth due to the

possibility of an innite number of values that have to be checked.

Then we give a suitable denition of the notion of the \nitary part" of

the bisimulation preorder to meet the preorder induced by the denotational

model. We recall that in [Ing95] we dened the so-called compact terms as

the syntactically nite terms which only use a nite number of values in a nontrivial

way. We also showed that these terms correspond exactly to the compact

elements in the denotational model in the sense that an element in the model

is compact if and only if it can be denoted by a compact term. This motivates

a denition of the nitary part, <

F , of the bisimulation preorder < by

p <

F q i 8c: c < p ) c < q

where c ranges over the set of syntactically compact terms. We also dene

yet another preorder, <

f

!, a coarser version of < ! in which we only consider a

nite number of values at each level in the iterative denition of the preorder.

Here it is vital that the set of values is countable and can be enumerated as

V al = fv1; v2; g. Thus in the denition of <

f

1 we only test whether the

dening constraints of the preorder hold when the only possible input and

output value is v1, and in general in the denition of <

f

n we test the constraints

for the rst n values only. (Here we would like to point out that this idea

originally appears in [HP80].) It turns out that <

f

! is the nitary part of <

in our new sense and that the model is fully abstract with respect to <

f

!. We

will prove both these results in this paper using techniques which are similar

to those used by Hennessy in the above mentioned reference [Hen81].

The structure of the paper is as follows: In Section 2 we give a short survey of

the result from the companion paper [Ing95] needed in this study. The denition

of the operational semantics and the notion of applicative bisimulation are the

subject of Section 3. Section 4 is devoted to the analysis of the preorder and the

denition of the value-nitary preorder <

f

!. In Section 5 we give a denition of

the notion of nitary part of a relation and a nitary relation over processes. In

the same section we prove that the preorder <

f

! is nitary and that it coincides

with the nitary part of the preorder < . Finally we prove the soundness and

the completeness of the proof system with respect to the resulting preorder.

The full abstractness of the denotational semantics for CCSL, given in [Ing95],

then follows from the soundness and the completeness of the proof system with

respect to the denotational semantics. In Section 6 we give some concluding

remarks.

#### Full Text:

PDFDOI: http://dx.doi.org/10.7146/brics.v2i22.19924

ISSN: 0909-0878

Hosted by the State and University Library and Aarhus University Library