BRICS RS-95-40 Ing� olfsd� ottir & Schalk: A Denotational Model for Observational Congruence

BRICS

Basic Research in Computer Science

A Fully Abstract Denotational Model for Observational Congruence

Anna Ing� olfsd� ottir Andrea Schalk

BRICS Report Series RS-95-40 ISSN 0909-0878 August 1995 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1995, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.aau.dk/BRICS/
ftp ftp.brics.aau.dk (cd pub/BRICS)

A Fully Abstract Denotational Model for Observational Congruence

Anna Ingólfsdóttir BRICS ^{∗}

Dep.of Maths and Computer Science

Aalborg University Denmark^{†}

Andrea Schalk Computer Laboratory University of Cambridge Cambridge England^{‡}

Abstract

A domain theoretical denotational model is given for a simple sublanguage of CCS extended with divergence operator. The model is derived as an abstraction on a suitable notion of normal forms for labelled transition systems. It is shown to be fully abstract with respect to observational precongruence.

1 Introduction

In describing the semantics of communicating processes the notion of bisimulation, [Par81, Mil83], has became standard in the literature. In this setting two processes are considered to be behaviourally equivalent if they can simulate each other’s behaviour. It is standard practice to distinguish between strong bisimulation, where the silent τ-moves are considered visible, and weak bisimulation, which abstracts away from them. Weak bisimulation equivalence turns out not to be a congruence with respect to some of the standard operators found in process algebras, e.g. the choice operator of CCS, and therefore the notion of weak bisimulation congruence, often called observational congruence, has been introduced.

One of the main characteristics of weak bisimulation equivalence, and of the associated congruence, is the fact that it allows for the abstraction from divergence, i.e. infinite sequences of internal computations, in process behaviours. Semantic theories for processes based on the bisimulation idea which take divergence into account have also been considered in the literature, see, e.g., [Wal90, AH92]. In those studies, bisimulation equivalence is extended to a bisimulation preorder, usually referred to as prebisimulation. Intuitively if a process p is smaller than a process q with respect to the bisimulation preorder, then the two processes are bisimilar, but p may diverge more often than q.

∗Basic Research in Computer Science, Centre of the Danish National Research Foundation.

†email: annai@iesd.auc.dk

‡email: Andrea.Schalk@cl.cam.ac.uk

For a further understanding and justification of the idea of bisimulation, many researchers have presented more abstract formal descriptions for it, using different theoretical tools to analyse in depth the nature of the concept. Examples of such alternative descriptions are characterizations of bisimulation by means of modal logics, [Sti87, Mil89], sound and complete axiomatizations, [Hen81, Wal90, AH92], and fully abstract denotational models, [Hen81, Abr91, AH92]. The denotational models are usually given in terms of Σ-domains, i.e. ωalgebraic cpos endowed with a continuous Σ-algebra structure. The existence of a fully abstract model in terms of a Σ-domain has the consequence that the behavioural preorder one is trying to model has to be finitary. Intuitively this means that the behavioural preorder is completely induced by finite observations of process behaviours. This is, in general, not the case for bisimulation as shown in, e.g., [Abr91]. For this reason, studies on mathematical models for such relations usually focus on providing denotational models for finitary versions of the bisimulation preorders [Hen81, Abr91, AH92].

There is a natural connection between sound and complete axiomatizations of behavioural preorders and fully abstract denotational models. Denotational models are often given in terms of initial Σ-domains satisfying a set of inequations [Hen88a]. In this kind of models the interpretation of a term is simply the set of terms which can be proved equal to it by the proof system. This type of denotational models is usually referred to as term models in the literature. Examples of such models may be found in, e.g., [Hen81], where the author defines a fully abstract term model for strong prebisimulation on a simple extension of SCCS, and in [AH92], where the authors give a fully abstract term model for observational congruence over an extension of the standard CCS.

Term models have been criticized for not giving much more insight into the semantics than the proof system already does. It is true that the existence of a fully abstract model for a behavioural preorder in terms of an algebraic cpo does imply that the behavioural preorder must be finitary, but usually this property has to be proven first anyway to prove the full abstractness of such a model. On the other hand by giving a syntax free representation of the term model we may gain some insight into the properties of the semantics we want to model. One way of obtaining such a syntax free representation, which is fully abstract with respect to a finitary behavioural preorder, is to investigate the preorder on the process graphs, that define the operational semantics. By investigating this preorder for finite processes we may gain enough information to be able to predict the behaviour for infinite processes. This is typically done by introducing some notion of semantic normal form for process graphs which contains enough information about the behavioural preorder. This kind of semantic normal forms may then induce a poset which coincides with the kernel of the behavioural preorder for finite processes. If all processes in the language can be turned into syntactic normal forms (i.e process terms whose process graph is in semantic normal form) in a sound way, i.e. preserving the behavioural semantics, it is sometimes possible to obtain a fully abstract model by taking the unique algebraic cpo which has the poset derived from semantic normal forms as its representation of its compact elements. A similar approach occurs in Hennessy’s model for testing equivalence based on finite acceptance trees which basically is a syntax free representation of the syntactic normal forms he defines, [Hen85, Hen88b].

Yet another, and maybe the most mathematically elegant, way of defining a denotational model is to define it as the initial solution to a recursive domain equation. The normal forms may now occur in the description of the compact elements derived from this definition. In [Abr91] Abramsky defines a fully abstract model for the finitary part of strong prebisimulation for SCCS. The domain theoretic constructions he uses are a variant of the Plotkin power construction and a notion of infinite sum. The poset of compact elements of the model may, roughly speaking, be represented as finite convex closed sets of finite synchronization trees ordered by the strong bisimulation preorder.

To give a short summary of the existing denotational models for bisimulation we have: For strong ω-prebisimulation on SCCS a fully abstract term model is given in [Hen81] and a fully abstract mathematical model in [Abr91]. For the ω-version of observational precongruence a fully abstract term model is given in [AH92] for an extension of CCS.

In this paper we will contribute to the investigation in a denotational setting of bisimulation preorders by defining a syntax free model for the ω-observational precongruence. Our aim is therefore to define a Σ-domain which is initial in the class of Σ-domains satisfying the set of equation that characterizes the ωobservational congruence and which does not mention terms or equations. Our approach is based on the idea of normal forms and ideal closure as described above. Thus we introduce semantic normal forms which are simply the process graphs derived from the syntactic normal forms introduced by Walker in [Wal90] ordered by strong bisimulation preorder. These normal forms may be represented as restricted form for finite synchronization trees ordered by the Egli-Milner preorder and can therefore be compared to Abramsky’s model in [Abr91]. Our hope was to, instead of using equivalence classes as the elements of our model, to represent the equivalence classes by some canonical elements, i.e. the normal forms. Unfortunately our approach did not work quite as well as we had hoped. All the equations turn out to be sound in this model apart from the equation

μ.τ.x = μ.x  (1)

which turns out to be difficult to model. Therefore our model is structured on two levels: on the first level we define the normal synchronization trees as described above whereas we obtain the second level by factoring out equation (1). We show the full abstractness of our model with respect to ω-observational precongruence.

We will focus on much simpler language than the one studied in [AH92]. Thus we only consider a language describing trees, finite or infinite, as all the aspects we are interested in investigating are captured by this simple language. (Most of the results we obtain may be easily extended to full CCS or similar languages with divergence added to them.) In our study we make an extensive use of properties already proven in the literature, e.g. in the definition of the existing models for bisimulation preorders. Thus we may assume the soundness and completeness of the proof system used to define the term model in [AH92] which of course is simplified and modified according to the different language. In the same reference it is also proved that the ω-observational precongruence is finitary. From [Wal90] we borrow a suitable notion of normal forms and a corresponding normalization theorem. Furthermore we also get from that reference an alternative characterization of the observational precongruence which turns out to be useful in our studies.

The structure of the paper is as follows: In Section 2 we give a short review of labelled transition systems with divergence and the diverse notions of prebisimulation and observational precongruence; in the same section we introduce the notion of normal forms and give an alternative characterization of the observational precongruence on these. In Section 3 we define the language T rees and give a short summary of existing results for this: a sound and complete axiomatization of the observational preorder and a normalization theorem for finite trees. In Section 4 we give a short overview over the domain theory we need whereas Section 5 is devoted to the definition of our domain and a proof of a full abstractness with respect to observational precongruence. We finish the paper by giving some concluding remarks.

2 Labelled Transition Systems with Divergence

The operational semantics of the languages considered in this paper will be given in terms of a variation on the notion of labelled transition systems [Kel76] that takes divergence information into account. We refer the interested readers to, e.g., [Hen81, Mil81, Wal90] for motivation and more information on (variations of) this semantic model for reactive systems.

Definition 2.1 [Labelled Transition Systems with Divergence] A labelled transition system with divergence (lts) is a quadruple (P, Lab, →, ↑), where:

• P is a set of processes or states, ranged over by s, s′, s_{i};

• Lab is a set of labels, ranged over by ℓ;

• →⊆ P × Lab × P is a transition relation. As usual, we shall use the more suggestive notation s →^{ℓ} s′ in lieu of (s, ℓ, s′) ∈→;

• ↑⊆ P is a divergence predicate, notation s ↑.

We let Λ range over all lts’s. A process graph is a pair of the form (s_{0}, Λ) where s_{0} ∈ P is the initial state and P is the set of processes in Λ. □

We write s ↓, read “s converges globally”, iff it is not the case that s ↑. The lts Λ = (P, Lab, →, ↑) is said to be a finite state lts if P is finite; it is said to be finite if it is a finite state lts and does not contain cycles. A finite tree lts is defined in the obvious way. We note here that each finite lts may be turned into a finite tree lts by making one copy of each state for each incoming arc where the outgoing arcs and their descendants are the same as from the original state. We note that the resulting lts is not isomorphic to the original one as in general it has more states. On the other hand it is strongly bisimilar to the original one in the sense to be defined later in this section. In our semantic theory the operational semantics for a process s, is given by a process graph with the process as the initial state. Intuitively, a process graph is an lts with a pointer to the initial state. If the underlying lts Λ is fixed we write s instead of the process graph (s, Λ). A finite tree lts Λ, has a canonical initial state, namely the root of the tree, root(Λ). Therefore, if Λ is a finite tree lts, we often refer to the process graph (root(Λ), Λ) as Λ. In this study we will follow this practice without further explanations.

We define the following operators on process graphs:

1. l : (s, (P, ⟶, ↑)) = (l : s, (P ∪ {l : s}, Lab ∪ {l}, ⟶ ∪{(l : s, l, s)}, ↑)) where l : s ∉ P is a new state.

2. ∑ ∘ _{i≤N}(s_{i}, (P_{i}, Lab_{i}, ⟶_{i}, ↑_{i})) = (s′, (P′, Lab′, ⟶′, ↑′)) where

(a) s′ = ∑_{i≤N} s_{i} ∉ ⋃_{i≤N} P_{i} is a new state,

(b) P′ = {s′} ∪ ⋃_{i≤N}(P_{i} \ {s_{i}}),

(c) Lab′ = ⋃_{i≤N} Lab_{i},

(d) ⟶′= \begin{matrix}⋃_{i≤N}(⟶_{i} \\{(s_{i}, l, s′_{i})| (s_{i}, l, s′_{i}) ∈⟶_{i}\} \\ ∪\{(s′, l, s′_{i})| (s_{i}, l, s′_{i}) ∈⟶_{i}\}), \end{matrix}

(e) ↑′= ⋃_{i≤N} ↑_{i} ∪{s′| ∃j.s_{j} ∈↑_{j}}.

We use the infix notation ⊕ for the sum over two lts’s. We assume that μ : has priority over ⊕. The finite tree lts’s may be represented as the set of finite synchronization trees over a set of labels Lab, denoted by ST(Lab). These are the sets generated by the following inductive definition:

1. ∅, {⊥} ∈ ST(Lab),

2. ℓ_{i} ∈ Lab, t_{i} ∈ ST(Lab) for i ≤ N implies {⟨ℓ_{i}, t_{i}⟩ | i ≤ N}[∪{⊥}] ∈ ST(Lab),

where the notation [∪{⊥}] means optional inclusion of ⊥. The divergence predicate and the transition relation are defined a follows:

• t ↑ iff ⊥ is in t, and

• t →^{ℓ_{i}} t_{i} iff ⟨ℓ_{i}, t_{i}⟩ is in t.

We let t range over ST(Lab).

We note that the process graph operators also apply for ST(Lab); in this representation we have μ : t = {⟨μ, t⟩} and ⊕ = ∪. Furthermore we often write μ instead of {⟨μ, ∅⟩} or μ : ∅. This may simplify our notation considerably later on.

The following norm on ST(Lab) will be needed in this study.

The depth of a normal form, d : NST(Act_{τ}) ⟶ Nat is defined by

1. d(∅) = d({⊥}) = 0 2. d(μ : t) = 1 + d(t)

3. (∑ ∘ _{i≤N}μ_{i} : t_{i}[⊕{⊥})] = max_{i} d(μ_{i} : t_{i})

We extend the function d to d : ST(Lab) × ST(Lab) ⟶ Nat by d(t_{1}, t_{2}) = d(t_{1}) + d(t_{2}).

In what remains of this section we let Λ = (P, Lab, →, ↑) be a fixed lts. Furthermore we let Rel(P) denote the set of binary relations over P. The behavioural relations over processes that we shall study in this paper are those of prebisimulation [Mil81, Hen81, Wal90]. (also known as partial bisimulation [Abr91]).

Definition 2.2 [Strong Prebisimulation] Define the functional F_{s} : Rel(P) → Rel(P) (s stands for “strong”) by:

Given R ∈ Rel(P), s_{1}F_{s}(R)s_{2} iff, for each μ ∈ Act_{τ},

1. If s_{1} ⟶^{μ} s′_{1} then, for some s′_{2}, s_{2} ⟶^{μ} s′_{2} and s′_{1}Rs′_{2}.

2. If s_{1} ↓ then (a) s_{2} ↓ and

(b) if s_{2} ⟶^{μ} s′_{2} then, for some s′_{1}, s_{1} ⟶^{μ} s′_{1} and s′_{1}Rs′_{2}.

The strong prebisimulation preorder (over Λ), ⊏_{∼}_{Λ} is defined as the largest fixedpoint for F_{s}. If Λ is known from the context we write ⊏_{∼} instead of ⊏_{∼}_{Λ}. □

The relation ⊏_{∼} is a preorder over P and its kernel will be denoted by ∼, i.e., ∼=⊏_{∼} ∩ ⊏_{∼}^{−1}. Intuitively, s_{1} ⊏_{∼} s_{2} if s_{2}’s behaviour is at least as specified as that of s_{1}, and s_{1} and s_{2} can simulate each other when restricted to the part of their behaviour that is fully specified. A divergent state s with no outgoing transition is a minimal element with respect to ⊏_{∼} and intuitively corresponds to a process whose behaviour is totally unspecified — essentially an operational version of the bottom element ⊥ in Scott’s theory of domains [SS71, Plo81].

The preorder ⊏_{∼} (and other similar relations) is extended to process graphs by

(s_{1}, Λ_{1}) ⊏_{∼} (s_{2}, Λ_{2}) if and only if s_{1} ⊏_{∼}_{Λ_{1}⊎Λ_{2}} s_{2}

where Λ_{1} ⊎ Λ_{2} is the standard disjoint union of Λ_{1} and Λ_{2}. Processes from different lts’s are compared in this way where we usually write only s_{1} ⊏_{∼} s_{2}. In the sequel, this will be done without further comment. (We will often need to compare states in an lts with finite synchronization trees.)

In this study, we shall be interested in relating the notion of prebisimulation to a preorder on processes induced by a denotational semantics given in terms of an algebraic domain [Plo81]. As such preorders are completely determined by how they act on finite processes, we shall be interested in comparing them with the “finitely observable”, or finitary, part of the bisimulation in the sense of, e.g., [Gue81, Hen81]. The following definition is from [Abr91].

Definition 2.3 Let R ∈ Rel(P). The finitary part of R, R^{F} is defined on any lts by

sR^{F} s′ ⇔ ∀t ∈ ST(Lab). tRs ⇒ tRs′ .
□

An alternative method for using the functional F_{s} to obtain a behavioural preorder is to apply it inductively as follows:

• ⊏_{∼}_{0}= Rel(P),

• ⊏_{∼}_{n+1}= F_{s}(⊏_{∼}_{n})

and finally ⊏_{∼}_{ω}= ⋂_{n≥0} ⊏_{∼}_{n}. Intuitively, the preorder ⊏_{∼}_{ω} is obtained by restricting the prebisimulation relation to observations of finite depth. The preorders ⊏_{∼}, ⊏_{∼}_{ω} and ⊏_{∼}^{F} are, in general, related thus:

⊏_{∼} ⊆ ⊏_{∼}_{ω} ⊆ ⊏_{∼}^{F} .

Moreover the inclusions are, in general, strict. The interested reader is referred to [Abr91] for a wealth of examples distinguishing these preorders, and a very deep analysis of their general relationships and properties. Here we simply state the following useful result, which is a simple consequence of [Abr91, Lem. 5.10]:

Lemma 2.4 For every t ∈ ST(Lab), s ∈ P, t ⊏_{∼} s iff t ⊏_{∼}_{ω} s.

Next we define the weak version of the prebisimulation and the derived observational precongruence. Following the standard practice we assume that the set of labels Lab has the form Act_{τ} = Act ∪ {τ} where Act is a set of visible actions and τ ∉ Act is an invisible action. We let a range over Act and μ over Act_{τ}. We let ⟹^{μ} denote (⟶^{τ})^{∗}· ⟶^{μ} ·(⟶^{τ})^{∗}. So s_{1} ⟹^{μ} s_{2} means that s_{1} may evolve to s_{2} performing the action μ and possibly silent moves. We will also use the relation ⟹^{ε}, defined as (⟶^{τ})^{∗}.

For any s, let Sort(s) = {μ ∈ Act_{τ} | ∃ σ ∈ Act_{τ}^{∗}, s′ ∈ P : s ⟶^{σμ} s′}, where,

for σ ∈ Act_{τ}^{∗}, ⟶^{σ} is defined in the natural way. In this study we only deal with lts’s which are sort finite, that is where Sort(s) is finite for each s ∈ P. Some of our results will depend on this fact.

Processes that can perform an infinite sequence of τ-actions are weakly divergent, which brings us to a definition of a weak divergence predicate. Let ⇓ be the least predicate over P which satisfies

s_{1} ↓ and (for each s_{2}, s_{1} ⟶^{τ} s_{2} then s_{2} ⇓) imply s_{1} ⇓ .

s ⇑ means that s ⇓ is not the case. In the semantic preorder to be defined we will use versions of ⇓ which are parameterized by actions:

s_{1} ⇓ μ if s_{1} ⇓ and , for each s_{2}, s_{1} ⟹^{μ} s_{2} implies s_{2} ⇓

We use the standard notation μ̂ where τ̂ stands for ε and â stands for a. The following definition is taken directly from [Wal90].

Definition 2.5 Given R ∈ Rel(P), s_{1}F_{w}(R)s_{2} (w for “weak”) iff, for each μ ∈ Act_{τ},

1. if s_{1} ⟶^{μ} s′_{1} then, for some s′_{2}, s_{2} ⟹^{μ̂} s′_{2} and s′_{1}Rs′_{2}

2. if s_{1} ⇓ μ then (a) s_{2} ⇓ μ

(b) if s_{2} ⟶^{μ} s′_{2} then, for some s′_{1}, s_{1} ⟹^{μ̂} s′_{1} and s′_{1}Rs′_{2}

The weak bisimulation preorder ⊏_{≈} is defined as the largest fixed-point for F_{w}. The weak ω-bisimulation preorder ⊏_{≈}_{ω} is defined by

• ⊏_{≈}_{0}= P × P (the top element in the lattice (Rel(P), ⊆))

• ⊏_{≈}_{n+1}= F_{w}(⊏_{≈}_{n})

and finally ⊏_{≈}_{ω}= ⋂_{n≥0} ⊏_{≈}_{n}. □

The following result is proved in [AH92].

Lemma 2.6 For all t ∈ ST(Act_{τ}) and s ∈ P, t ⊏_{≈}_{ω} s iff t ⊏_{≈} s.

The set Act_{τ} is assumed to be fixed throughout the paper from now on and we write ST instead of ST(Act_{τ}).

As it is well know from the literature, [Mil83, Mil89, Wal90], the preorder ⊏_{≈} is not a precongruence with respect to some of the standard operators, e.g the choice operator + of CCS. In terms of process graphs this is also the case. Thus the notion of observational precongruence is introduced. This will be done in the following:

For any R ∈ Rel(P) we define the new relation R^{c} by:

s_{1}R^{c}s_{2} if, for every context C[·], C[s_{1}]RC[s_{2}].

where a context for process graphs has the obvious meaning. Then R is said to be closed with respect to contexts if R = R^{c}. The observational precongruence is defined as ⊏_{≈}^{c} and may be described as the least precongruence contained in weak bisimulation preorder. In [Wal90] Walker gives an operational characterization of ⊏_{≈}^{c}. In order to obtain this he defines the operator ^{∗} on Rel(P) as follows:

Definition 2.7 For all R ∈ Rel(P) we let s_{1}R^{∗}s_{2} iff

1. if s_{1} ⟶^{a} s′_{1} then, for some s′_{2}, s_{2} ⟹^{a} s′_{2} and s′_{1}Rs′_{2}

2. if s_{1} ⟶^{τ} s′_{1} then

(a) if s′_{1} ⇓ then there exists s′_{2} such that s_{2} ⟹^{τ} s′_{2} and s′_{1}Rs′_{2}

(b) if s′_{1} ⇑ then there exists s′_{2} such that s_{2} ⟹^{ε} s′_{2} and s′_{1}Rs′_{2}.

3. if s_{1} ⇓ μ then

(a) s_{2} ⇓ μ

(b) if s_{2} ⟶^{μ} s′_{2} then, for some s′_{1}, s_{1} ⟹^{μ} s′_{1} and s′_{1}Rs′_{2} □

The following lemma is proved in [Wal90].

Lemma 2.8 ⊏_{≈}^{c}=⊏_{≈}^{∗} and ⊏_{≈}_{ω}^{c}=⊏_{≈}_{ω}^{∗}.

The following definition of normal forms for synchronization trees is also borrowed from [Wal90] with an obvious adaption to process graphs. Definition 2.9 (Normal Forms) An element n = {⟨μ_{1}, n_{1}⟩, …, ⟨μ_{l}, n_{l}⟩}[∪{⊥}] ∈ ST (where ∪{⊥} is optional) is a normal form if

1. n_{i} is a normal form for i ≤ l,

2. if μ_{i} = τ then n_{i} ⇓,

3. if n ⇓ and n ⇑ a then ⟨a, {⊥}⟩ ∈ n,

4. if n ⟹^{μ} n′ then ⟨μ, n′⟩ ∈ n. □

Note that if n is a normal form then n ⇑ iff n ↑ iff ⊥ ∈ n. This property will play an important role in our investigation of the preorder ⊏_{≈}^{∗} on normal forms. Now we will give a simple characterization of the normal forms as a subset of ST. For this purpose we introduce the following operators on ST: Definition 2.10 We define μ_{NST} by:

\begin{matrix}τ_{NST}.t = t ∪ \{⟨τ, t⟩|⊥ ∉ t\} \\ a_{NST}.t = \{⟨a, t⟩\} ∪ \{⟨a, t′⟩|⟨τ, t′⟩ ∈ t\} ∪ \{⟨a, ⊥⟩|⊥ ∈ t\} \end{matrix}

□

Now we define the subset NST of ST as follows: Definition 2.11 We define the set NST as the smallest set which satisfies:

1. {⊥}, ∅ ∈ NST.

2. n ∈ NST and μ ∈ Act_{τ} implies μ_{NST}.n ∈ NST.

3. n_{1}, n_{2} ∈ NST implies n_{1} ⊕ n_{2} ∈ NST.

□

We have the following lemma: Lemma 2.12 1. μ_{NST}. and ⊕ preserve ⊏_{∼}.

2. If n = ∑ ∘ _{i≤N}μ_{i} : n_{i}[⊕{⊥}] ∈ NST then n = ∑ ∘ _{i≤N}μ_{i}_{NST}.n_{i}[⊕{⊥}].

3. The set NST is exactly the subset of normal forms of ST.

Proof 1. Straight forward and is left to the reader.

2. We proceed as follows: Let m = ∑ ∘ _{i≤N}μ_{i}_{NST}.n_{i}[⊕{⊥}]. We will prove that n = m where “=” is set equality. The inclusion n ⊆ m is obvious. To prove that m ⊆ n we proceed as follows: Assume that ⟨μ, m′⟩ ∈ m. We will prove that ⟨μ, m′⟩ ∈ n. We know that ⟨μ, m′⟩ ∈ μ_{i}_{NST}.n_{i} for some i. If ⟨μ, m′⟩ = ⟨μ_{i}, n_{i}⟩ we are done so assume this is not the case. We have the following two cases:

μ_{i} = τ: In this case ⟨μ, m′⟩ ∈ n. μ_{i} = a ∈ Act: Then μ_{i}_{NST}.n_{i} = a : n_{i} ∪ ⋃{a : n′_{i}|τ : n′_{i} ∈ n_{i}} ∪

[{⟨a, ⊥⟩|⊥ ∈ n_{i}}]. Now either μ : m′ = a : n′_{i} for some n′_{i} where τ : n′_{i} ∈ n_{i} or μ : m′ = a : {⊥} where ⊥ ∈ n_{i}. In both cases, by definition of normal forms, μ : m′ ∈ n.

3. Let ST_{N} denote the subset of normal forms in ST. We will prove that ST_{N} = NST. We proceed as follows:

NST ⊆ ST_{N}: By definition NST ⊆ ST. That the elements of NST satisfy the defining conditions for normal forms follows from a simple induction on the definition of NST. Therefore NST ⊆ ST_{N}

ST_{N} ⊆ NST: Let

n = ∑_{i} ∘ μ_{i} : n_{i}[⊕{⊥}] ∈ ST_{N}.

By part 2. of the lemma

n = ∑_{i} ∘ μ_{i}_{NST}.n_{i}[⊕{⊥}],

which in turn implies that n ∈ NST.

□

In the following we define a finer version of a preorder originally defined in [Wal90]. (In the set of normal forms these two definitions coincide.) It gives a simplified characterization of the preorders ⊏_{≈} and ⊏_{≈}^{∗} on NST.

Definition 2.13 1. We define F_{w}^{g} : Rel(P) ⟶ Rel(P) (where g stands for “global convergence”) by: Given R ∈ Rel(P), s_{1}F_{w}^{g}(R)s_{2} iff, for each a ∈ Act,

(a) if s_{1} ⟶^{a} s′_{1} then, for some s′_{2}, s_{2} ⟶^{a} s′_{2} and s′_{1}Rs′_{2}

(b) if s_{1} ⟶^{τ} s′_{1} then, for some s′_{2}, s_{2} ⟹^{ε} s′_{2} and s′_{1}Rs′_{2}

(c) if s_{1} ↓ then the following holds: i. s_{2} ↓

ii. if s_{2} ⟶^{a} s′_{2} then, for some s′_{1}, s_{1} ⟶^{a} s′_{1} and s′_{1}Rs′_{2}

iii. if s_{2} ⟶^{τ} s′_{2} then, for some s′_{1}, s_{1} ⟹^{ε} s′_{1} and s′_{1}Rs′_{2}

We define ⊏_{≈}_{g} to be the largest fixed point of F_{ω}^{g}.

2. We define the preorder ⊏_{≈}_{g}^{◇} by: s_{1} ⊏_{≈}_{g}^{◇} s_{2} iff, for each μ ∈ Act_{τ},

(a) if s_{1} ⟶^{μ} s′_{1} then, for some s′_{2}, s_{2} ⟶^{μ} s′_{2} and s′_{1} ⊏_{≈}_{g} s′_{2},

(b) if s_{1} ↓ then i. s_{2} ↓ and

ii. if s_{2} ⟶^{μ} s′_{2} then, for some s′_{1}, s_{1} ⟶^{μ} s′_{1} and s′_{1} ⊏_{≈}_{g} s′_{2}. □

In [Wal90] the author shows that in general ⊏_{≈}_{g} is strictly finer than the weak bisimulation preorder ⊏_{≈}. However it turns out that for normal forms these two preorders and their derived preorders, ⊏_{≈}^{∗} and ⊏_{≈}_{g}^{◇}, coincide. This is the content of the following theorem.

Theorem 2.14 For all n_{1}, n_{2} ∈ NST, n_{1} ⊏_{≈} n_{2} iff n_{1} ⊏_{≈}_{g} n_{2} and n_{1} ⊏_{≈}^{∗} n_{2} iff

n_{1} ⊏_{≈}_{g}^{◇} n_{2}.

Proof See Appendix A. □

We observe that the characterization ⊏_{≈}_{s}^{◇} of the preorder ⊏_{≈}^{∗} on normal forms looks very much like the definition for the strong prebisimulation preorder ⊏_{∼}. The only difference is that on lower levels a τ transition may be matched by an empty transition. The following example shows that with the definition of normal forms we have chosen the preorders ⊏_{≈}^{∗} and ⊏_{∼} do indeed not coincide.

Example 2.15 Let n_{1} = τ : (τ : a ⊕ a ⊕ a : Ω) ⊕ τ : a ⊕ a ⊕ a : Ω and n_{2} = τ : a ⊕ a. Then n_{1} ⊏_{≈}^{∗} n_{2} but n_{1} ⊏̸_{∼} n_{2}. The reason for this is that the left hand side can perform a sequence of two τs to start with while the left hand side only can perform a sequence of τ-transitions of length one. On the other hand if we add τ : (τ : a ⊕ a) (adding only τ : τ : a would not preserve the normal form property) to the right hand side the τ-depth is balanced and we get that n_{1} ⊏_{∼} n_{2} ⊕ τ : (τ : a ⊕ a). Furthermore n_{2} ≈^{∗} n_{2} ⊕ τ : (τ : a ⊕ a) (where ≈^{∗} is the kernel of ⊏_{≈}^{∗}.

The example above illustrates that the preorders ⊏_{≈}^{∗} and ⊏_{∼} do not coincide on NST. But at the same time it also suggests that if n ⊏_{≈}^{∗} m then by performing a simple balancing operation on n and m, which is sound with respect to ≈^{∗} we may get a pair of normal forms, n′ and m′, where n′ ⊏_{∼} m′. In our attempt to give a simple characterization of the preorder ⊏_{≈}^{∗} on normal forms this would be a useful result. In the next section we will therefore formalize this informal statement and prove that it holds.

2.1 The Characterization Theorem for Observational Precongruence

In the proof for the characterization result for ⊏_{≈}^{∗} on NST outlined above we suggested a transformations on normal forms which is sound with respect to ⊏_{≈}^{∗}. To formalize this idea we introduce a notion of equivalence on NST meaning

A1 x ⊕ y = y ⊕ x  A3 x ⊕ x = x
A2 x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z A4 x ⊕ ∅ = x
τ 1 μ.τ.x = μ.x

Figure 1: The Graph Equations E

that two elements are equivalent if they can be transformed into the same terms applying the balancing operation described above. As we need to be able to apply the transformation mentioned above recursively on the structure of the normal form we want the equivalence to be a congruence with respect to the graph operators. On the other hand the operator μ : does not preserve normal forms whereas the operator μ_{NST} does. Also the operator ⊕ preserves normal forms. Furthermore we know from Lemma 2.12 that for normal forms

∑_{i≤N} ∘ μ_{i} : n_{i}[⊕{⊥}] = ∑_{i≤N} ∘ μ_{i}_{NST}.n_{i≤N}[⊕{⊥}].

Keeping this in mind we only require the equivalence to be a congruence with respect to the operators μ_{NST}. and ⊕. To define the equivalence suggested above we introduce a set of equations, E, which may be found in Figure 1. These equations are interpreted over NST with respect to the operators mentioned above. Now we let =_{E} denote the least congruence over NST with respect to μ_{NST}. and ⊕ generated by the equations in E. It is easy to see that the equations in E are sound with respect to ≈^{∗} on NST, i.e that =_{E}⊆≈^{∗} on NST.

Furthermore we need the following general theorem which is a slight modification of a similar theorem proved in [AH92].

Theorem 2.16 (Hennessy’s Theorem) For all t_{1}, t_{2} ∈ ST the following holds:

t_{1} ⊏_{≈} t_{2} iff t_{1} ⊏_{≈}^{∗} t_{2} or t_{1} ⊏_{≈}^{∗} τ_{NST}.t_{2} or τ_{NST}.t_{1} ⊏_{≈}^{∗} t_{2}.

The Characterization Theorem may now be stated as follows:

Theorem 2.17 (The Characterization Theorem) Let n, m ∈ NST. Then n ⊏_{≈}^{∗} m if and only if there exist some n′, m′ ∈ NST such that n′ ⊏_{∼} m′, n =_{E} n′ and m =_{E} m′.

Proof The “if” part follows immediately so we only have to concentrate on the “only” part. We proceed by induction on the combined depth of n and m, d(n, m).

d(n, m) = 0: The only possible combinations are the following:

1. n = m = ∅,

2. n = {⊥} and m = ∅, and

3. n = m = {⊥}.

All three cases are obvious.

d(n, m) = k + 1: Assume

n = ∑_{i≤N} ∘ μ_{i}_{NST}.n_{i}[⊕{⊥}] and m = ∑_{i≤M} ∘ γ_{j}_{NST}.m_{j}[⊕{⊥}].

Then By Lemma 2.12

n = ∑_{i≤N} ∘ μ_{i} : n_{i}[⊕{⊥}] and m = ∑_{i≤M} ∘ γ_{j} : m_{j}[⊕{⊥}].

First let us assume that ⊥ ∉ n and therefore ⊥ ∉ m. Now we recall that if n ⟶^{μ} n′ then m ⟶^{μ} m′ for some m′ where n′ ⊏_{≈} m′ and vice versa. We may therefore assume that N = M and that μ_{i} = γ_{i} and n_{i} ⊏_{≈} m_{i} for i ≤ N. (We may have to rearrange the summands and/or duplicate some of them as well to obtain this.) By Hennessy’s Theorem 2.16, for each i one of the following holds:

Case 1: n_{i} ⊏_{≈}^{∗} m_{i}: By induction there are n′_{i}, m′_{i} ∈ NST such that

n_{i} =_{E} n′_{i}, m_{i} =_{E} m′_{i} and n′_{i} ⊏_{∼} m′_{i}. Furthermore μ_{i}_{NST}.n_{i} =_{E} μ_{i}_{NST}.n′_{i}

and μ_{i}_{NST}.m_{i} =_{E} μ_{i}_{NST}.m′_{i}.

Case 2: n_{i} ⊏_{≈}^{∗} τ_{NST}.m_{i}:By induction there are n′_{i}, m′_{i} ∈ NST such that

n_{i} =_{E} n′_{i}, τ_{NST}.m_{i} =_{E} m′_{i} and n′_{i} ⊏_{∼} m′_{i}. Furthermore μ_{i}_{NST}.n_{i} =_{E}

μ_{i}_{NST}.n′_{i} and μ_{i}_{NST}.m_{i} =_{E} μ_{i}_{NST}.τ_{NST}.m_{i} =_{E} μ_{i}_{NST}.m′_{i}.

Case 3: τ_{NST}.n_{i} ⊏_{≈}^{∗} m_{i}: By induction there are n′_{i}, m′_{i} ∈ NST such that

τ_{NST}.n_{i} =_{E} n′_{i}, m_{i} =_{E} m′_{i} and n′_{i} ⊏_{∼} m′_{i}. Furthermore μ_{i}_{NST}n_{i} =_{E}

μ_{i}_{NST}.τ_{NST}.n_{i} =_{E} μ_{i}_{NST}.n′_{i} and μ_{i}_{NST}.m_{i} =_{E} μ_{i}_{NST}.m′_{i}.

We let

n′ = ∑_{i≤N} ∘ μ_{i}_{NST}.n′_{i}

and

m′ = ∑_{i≤N} ∘ μ_{i}_{NST}.m′_{i}

which both are normal forms. Obviously n =_{E} n′ and m =_{E} m′. Furthermore by Lemma 2.12

n′ = ∑_{i≤N} ∘ μ_{i} : n′_{i}

and

m′ = ∑_{i≤N} ∘ μ_{i} : m′_{i}.

It is now easy to see that n′ ⊏_{∼} m′.

Next assume that ⊥ ∈ n. The case when it is the only element is obvious, so assume this is not the case. Now we recall that if n ⟶^{μ} n′ then there is an m′ such that m ⟶^{μ} m′ and n′ ⊏_{≈} m′. By a similar reasoning as in the previous case we may now assume that

n = ∑_{i≤N} ∘ μ_{i} : n_{i} ⊕ {⊥} and m = ∑_{i≤N} ∘ μ_{i} : m_{i} ⊕ m′

where n_{i} ⊏_{≈} m_{i} for i ≤ N. We may also assume that ∑_{i≤N} μ_{i} : m_{i} and m′ are normal forms. Now the proof may proceed as in the previous case. □

3 The Language

In this section we will give a short survey of the theory of observational precongruence for a simple sublanguage of CCS extended with the divergence operator. The language T rees is a language that denotes trees, finite and infinite, and only contains the operators nil, + and μ. which all have the standard meaning [Mil80], plus the nullary operator Ω, which stands for the inactive divergent process [Hen81, Wal90]. Infinite processes are given in the standard way by means of the construction recx. where x is a process variable.

Definition 3.1 Let Var be a countable set of process variables, ranged over by x, y … and Act_{τ} have the same meaning as in the previous section, ranged over by μ. The syntax of the language T reeT erms is defined by

u ::= nil | Ω | μ.u | u + u | x | recx.u.

We let T rees denote the set of closed terms in T reeT erms and F inT rees the set of recursion free elements of T rees. We let u range over T reeT erms, p, q over T rees and d over F inT rees. □

The operational semantics in terms of a transition relation and a convergence (and divergence) predicate is also defined in the standard way (see e.g. [Hen81, Wal90, AH92]).

Definition 3.2 1. Let ↓ be the least subset of T rees which satisfies

(a) nil ↓, μ.p ↓

(b) p ↓ and q ↓ implies (p + q) ↓

(c) t[recx.t/x] ↓ implies recx.t ↓

We say that p ↑ iff p ↓ is not true.

2. For each μ ∈ Act_{τ}, let ⟶^{μ} be the least binary relation on T rees which satisfies the following axioms and rules:

(a) μ.p ⟶^{μ} p

(b) p ⟶^{μ} p′ implies p + q ⟶^{μ} p′ and q + p ⟶^{μ} p′

(c) t[recx.t/x] ⟶^{μ} p′ implies recx.t ⟶^{μ} p′.

□

This definition generates an lts, Λ_{T ree} = (T rees, Act_{τ}, ⟶, ↑) which obviously is sort finite, as we do not have any relabelling as a construction in the language. The operational semantics for a p ∈ T rees is defined as the process graph (p, Λ_{T ree}). For d ∈ F inT rees the process graph that gives its semantics may be represented as an element of ST. Thus the operational semantics for d is given by G(d) obtained by the following recursive definition:

1. G(nil) = ∅,

2. G(Ω) = {⊥},

3. G(μ.d) = μ : G(d),

4. G(d_{1} + d_{2}) = G(d_{1}) ⊕ G(d_{2}).

Of course the definitions of ⊏_{∼}, ⊏_{≈}, ⊏_{≈}^{c} and ⊏_{≈}^{∗} and their ω-versions apply for the lts Λ_{T ree} and as before we have that ⊏_{≈}^{c}=⊏_{≈}^{∗} and ⊏_{≈}_{ω}^{c}=⊏_{≈}_{ω}^{∗}.

In [Wal90] and [AH92] the preorder ⊏_{≈}_{ω}^{∗} is given an equational characterizations in terms of equationally based proof systems. In Figures 2 and 3 we define such a proof system for T rees, which is a slight modification of the proof systems in the afore mentioned references. The proof system consists of a set of inequations, Figure 2, and a set of inference rules, Figure 3. We refer to the full proof system as E_{rec} but the sub-system where the rules (ω) and (rec) are omitted we call E. We write ^{⊑}_{E_{rec}} and ^{⊑}_{E} for the induced preorders. The syntactic approximations p^{n}, that occur in the rule (ω), are also standard (see e.g. [Hen88b]) and are defined inductively as follows:

Definition 3.3 (Finite Syntactical Approximations)

1. u^{0} = Ω for all u ∈ T reeT erms.

2.

(a) nil^{n+1} = nil, Ω^{n+1} = Ω and x^{n+1} = x for x ∈ Var,
(b) (u_{1} + u_{2})^{n+1} = u_{1}^{n+1} + u_{2}^{n+1},
(c) (μ.u)^{n+1} = μ.(u^{n+1}),

(d) (recx.u)^{n+1} = u^{n+1}[(recx.u)^{n}/x]. □

Here we note that if p ∈ T rees then p^{n} ∈ F inT rees. We get the following soundness and completeness result as a special case of the more general soundness and completeness theorem in [AH92].

Theorem 3.4 The proof system E_{rec} is sound and complete for T rees with respect to the preorder ⊏_{≈}_{ω}^{c}.

From [Wal90] we borrow the following notion of syntactic normal forms.

A1 x + y = y + x  Ω1 Ω ^{⊑} x
A2 x + (y + z) = (x + y) + z Ω2 τ.(x + Ω) ^{⊑} x + Ω
A3 x + x = x  τ 1 μ.τ.x = μ.x
A4 x + nil = x  τ 2 τ.x + x = τ.x
τ 3 μ.(x + τ.y) = μ.(x + τ.y) + μ.y

Figure 2: The Inequations

(ref) p ^{⊑} p  (trans)  \frac{p ^{⊑} q, q ^{⊑} r}{p ^{⊑} r}
(pre) \frac{p ^{⊑} q}{μ.p ^{⊑} μ.q}  (sum)  \frac{p_{1} ^{⊑} p_{2}, q_{1} ^{⊑} q_{2}}{p_{1} + q_{1} ^{⊑} p_{2} + q_{2}}
(rec) \overline{recP.p = p[recP.p/P]}  (ω)  \frac{p^{(n)} ^{⊑} q for all n}{p ^{⊑} q}
(inst) \overline{p ^{⊑} q} p ^{⊑} p is a closed instantiation of the inequations inE

Figure 3: The Proof system E_{rec}

Definition 3.5 (Syntactic Normal Forms) We say that η ∈ F inT rees is a normal form if η = ∑_{i} μ_{i}.η_{i}[+Ω] and

1. each η_{i} is a normal form,

2. if μ_{i} = τ then η_{i} ⇓

3. if η ⇓ and η ⇑ a then a.Ω is a summand of η.

4. if η ⟹^{μ} η′ then η ⟶^{μ} η′.

We denote the set of syntactic normal forms by NF ranged over by η. □ The following lemma gives the relationship between the syntactic and the semantic normal forms. Lemma 3.6 η ∈ NF iff G(η) ∈ NST.

Proof Follows from a simple induction on η. □

The following result is proved in [Wal90].

Theorem 3.7 (Normalization Theorem) For all d ∈ F inT ree there is η ∈ NF such that d =_{E} η.

4 Preliminaries on Algebraic Semantics

In this section, we review the basic notions of algebraic semantics and domain theory that will be needed in the remainder of this study. We assume that the reader is familiar with the basic notions of ordered and continuous algebras (see, e.g., [Gue81, Hen88a, AJ95]); however, in what follows we give a quick overview of the way a denotational semantics can be given to a recursive language like T rees following the standard lines of algebraic semantics [Gue81]. The interested reader is invited to consult [Hen88a] for an explanation of the theory.

In what follows, we let Σ denote a signature, i.e. a set of syntactic operators provided with a function, arity: Σ ⟶ Nat which gives the number of arguments the operator takes. A Σ-algebra is a pair (A, Σ_{A}), where A is the carrier set and Σ_{A} is a set of semantic operators f_{A} : A^{l} → A, where f ∈ Σ and l = arity(f). We call f_{A} the interpretation of the syntactic operator f in A.

Let (A, Σ_{A}) and (B, Σ_{B}) be Σ-algebras. A mapping φ : A → B is a Σhomomorphism if it preserves the Σ-structure, i.e. if for every f ∈ Σ and vector a⃗ of elements of A of the length arity(f):

φ(f_{A}(a⃗)) = f_{B}(φ(a⃗)) .

The term algebra T (Σ) is the initial Σ-algebra, i.e., if (A, Σ_{A}) is a Σ-algebra then there is a unique Σ-homomorphism ι_{A} : T (Σ) → A. We refer to this homomorphism as the interpretation of T (Σ) in A. We write T (Σ, Var) for the term algebra that contains the set of variables Var as operators of arity 0 and T^{rec}(Σ, Var) if it also allows the recursion construction recx.t. It is worth pointing out that the initial Σ-algebra for a set of generators, Var, does indeed exist. Actually, more than just that is true: We can also require a set of equations to hold on the resulting Σ-algebra (such as x + x = x, for example). The initial Σ-algebra for a set of generators satisfying a given set of equations is constructed from the term-model by defining an equivalence relation on terms. The operations are well defined with respect to the equivalence classes so that the resulting quotient is again a Σ-algebra.

The obvious idea is to model a language like that of T rees by a Σ-algebra where Σ is the set of finite term-forming operations (in the example mentioned, we get Σ = {Ω, nil, +} ∪ {μ. | μ ∈ Act_{τ}}). However, this is not sufficient to model operations like recursion. For that, we need to consider a slightly more sophisticated concept.

A Σ-domain (A, ⊑_{A}, Σ_{A}) is a Σ-algebra whose carrier (A, ⊑_{A}) is an algebraic complete partial order (cpo) (see e.g. [Plo81]) and whose operators in Σ_{A} are continuous. The notion of Σ-poset (respectively Σ-preorder) may be defined in a similar way by requiring that (A, ⊑_{A}) is a partially ordered (resp. preordered) set and that the operators are monotonic. The notion of Σ-homomorphism extends to the ordered Σ-structures in the obvious way by requiring that such maps preserve the underlying order-theoretic structure as well as the Σ-structure. Any Σ-preorder induces a unique Σ-poset which we refer to as its kernel. For any Σ-algebra, A, ordered or not, the set (Var → A) of A-environments will be denoted by ENV_{A}, and ranged over by the metavariable ρ. The (unique) interpretation of T (Σ, Var) in A is the mapping A[[·]] : T (Σ, Var) → (ENV_{A} → A) defined recursively by:

A[[x]]ρ =^{Δ} ρ(x)
A[[f(p_{1}, …, p_{l})]]ρ =^{Δ} f_{A}(A[[p_{1}]]ρ, …, A[[p_{l}]]ρ)

If A is a Σ-domain the interpretation extends to the term algebra T^{rec}(Σ, Var) by setting

A[[recx.u]]ρ =^{Δ} Yλa. A[[u]]ρ[x → a]

where Y denotes the least fixed-point operator. As usual, ρ[x → a] denotes the environment which is defined as follows:

ρ[x → a](y) =^{Δ} \{ \begin{matrix}a & if x = y \\ ρ(y) & otherwise \end{matrix} .

Note that, for each closed recursive term p ∈ T^{rec}(Σ, Var), A[[p]]ρ does not depend on the environment ρ. The denotation of a closed term, p, will be denoted by A[[p]]. For recursion free closed terms the mapping A[[ ]] coincides with ι_{A}.

To find such models, we have to say how to construct them. For posets, the process is very much like that of constructing the initial Σ-algebra - only this time one can actually start with a poset of generators, and the order for the resulting Σ-poset is then defined recursively on the terms such that the operations become monotonic. We can even do more in that case: instead of giving a set of equations which we want to hold, we can now deal with a set of inequalities. A typical inequality that one wants to hold in models for languages like ours is Ω ≤ x which can thus be built in. We are, however, not interested in the initial Σ-poset for a set of generators and inequalities but in the initial Σ-domain. These two, however, are closely related: The initial Σ-domain can be obtained as the ideal completion of the corresponding Σ-poset - the operations are the unique continuous extensions of the corresponding operators for the Σ-poset. Similarly any Σ-preorder induces a unique Σ-domain; the ideal completion of its kernel. For more details on how this works, see Chapter 6 in [AJ95].

5 A Fully Abstract Denotational Model for T rees

In this section we will define a Σ-domain (where Σ consists of the operators nil, Ω, + and μ. , (μ ∈ Act_{τ})) in such a way that the derived denotational semantics for T rees is fully abstract with respect to observational precongruence. We show that the model is fully abstract with respect to the observational precongruence by showing that it is the initial Σ-algebra with respect to the operations in our language plus the inequations in E. We obtain this by proving that the proof system E, interpreted in the model, is sound and complete with respect to the preorder of the model. The full abstractness then follows from the fact that the proof system is sound and complete with respect to the observational precongruence as stated in Theorem 3.4.

The domain is obtained as an abstraction on the preorder (NST, ⊏_{≈}^{∗}) as explained in the Introduction.

Definition 5.1 We define the Σ-preorder (NST,^{⊑}_{NST}, Σ_{NST}) as follows:

1. The preorder ^{⊑}_{NST} is defined as the least binary relation over NST satisfying:

n ^{⊑}_{NST} m if (1) ⟨μ, n′⟩ ∈ n ⇒ ∃⟨μ, m′⟩ ∈ m : n′ ^{⊑}_{NST} m′ and
(2) ⊥ ∈ m ⇒ ⊥ ∈ n and
(3) ⟨μ, m′⟩ ∈ m ⇒ (⊥ ∈ n or ∃⟨μ, n′⟩ ∈ n : n′ ^{⊑}_{NST} m′)

2. The structure Σ_{NST} is defined as follows:

(a) Ω_{NST} = {⊥},

(b) nil_{NST} = ∅,

(c) μ_{NST}: (compare Definition 2.10)

τ_{NST}.n = \{ \begin{matrix}n & if ⊥ ∈ n \\ \{⟨τ, n⟩\} ∪ n & if ⊥ ∉ n \end{matrix}

a_{NST}.n = \{ \begin{matrix}\{⟨a, n⟩\} ∪ \{⟨a, n′⟩|⟨τ, n′⟩ ∈ n\} & if ⊥ ∉ n \\ \{⟨a, n⟩\} ∪ \{⟨a, n′⟩|⟨τ, n′⟩ ∈ n\} ∪ \{⟨a, ⊥⟩\} & if ⊥ ∈ n \end{matrix}

(d) +_{NST}: n_{1} +_{NST} n_{2} = n_{1} ∪ n_{2} □

Now we have:

Lemma 5.2 1. The preorders ^{⊑}_{NST} and ⊏_{∼} coincide on NST.

2. (NST,^{⊑}_{NST}, Σ_{NST}) is a Σ-preorder.

3. For all η ∈ NF, NST[[η]] = G(η).

Proof

1. Is proved in [Abr91].

2. Follows directly from Lemma 2.12.1.

3. Follows by Lemma 2.12.2 and a simple structural induction on η.

□

Part 3. of the lemma above says that the denotational interpretation in NST of a normal form is exactly its operational semantics, i.e. the process graph that is generated by the rules for the operational semantics for the language T rees. To ease the notational complexity we use the notation μ : n to denote {⟨μ, n⟩} in what follows as explained in Section 2.

Unfortunately the equation (τ 1) is not sound in NST as the following example shows.

Example 5.3 Let n = ∅. Then

τ_{NST}.∅ = τ : ∅ ∪ ∅ = τ : ∅

and therefore

τ_{NST}.τ_{NST}.∅ = τ : τ : ∅ ∪ τ : ∅.

It is easy to see that

τ_{NST}.τ_{NST}.∅ ≁ τ_{NST}.∅.

However we have the following partial soundness result and a completeness result. Let F denote the proof system E minus the equation ( τ 1). Then we have:

Lemma 5.4 The proof system F is sound and complete for (NST,^{⊑}_{NST}, Σ_{NST}).

Proof The soundness of the inequations (A1)–(A4) and (Ω1)–(Ω2) is obvious. The soundness of the inference rules follows from the fact that (NST,^{⊑}_{NST} , Σ_{NST}) is a Σ-preorder. What remains to prove is the soundness of (τ 2) and (τ 3). We proceed as follows:

(τ 2): Assume that n ∈ NST. We will prove that

τ_{NST}.n +_{NST} n =_{NST} n.

The case when ⊥ ∈ n is obvious so we may assume that ⊥ ∉ n. Then we have

τ_{NST}.n +_{NST} n = (τ : n ∪ n) ∪ n = τ : n ∪ n = τ_{NST}.n.

(τ 3) Assume that n_{1}, n_{2} ∈ NST, we will show that

μ_{NST}.(n_{1} +_{NST} τ_{NST}.n_{2}) =_{NST} μ_{NST}.(n_{1} +_{NST} τ_{NST}.n_{2}) + μ_{NST}.n_{2}

We have the two possible cases: μ = τ and μ ≠ τ. We proceed as follows: μ = τ: The case when ⊥ ∈ n_{1} ∪ n_{2} is obvious. So let us assume that

⊥ ∉ n_{1} ∪ n_{2}. Then

τ_{NST}.(n_{1} +_{NST} τ_{NST}.n_{2})

= τ : (n_{1} ∪ τ : n_{2} ∪ n_{2}) ∪ (n_{1} ∪ τ : n_{2} ∪ n_{2})
= τ : (n_{1} ∪ τ : n_{2} ∪ n_{2}) ∪ (n_{1} ∪ τ : n_{2} ∪ n_{2}) ∪ (τ : n_{2} ∪ n_{2})
= τ_{NST}.(n_{1} +_{NST} τ_{NST}.n_{2}) +_{NST} τ_{NST}.n_{2}.

μ = a ∈ Act: Again we have two possible sub-cases: ⊥ ∈ n_{2} and ⊥ ∉ n_{2}.

⊥ ∈ n_{2}: First we note that

⊥ ∈ n_{2} implies n_{2} ^{⊑}_{NST} n_{1} ∪ n_{2}.  (2)

Now we have the following:

a_{NST}.(n_{1} +_{NST} τ_{NST}.n_{2})

=  a : (n_{1} ∪ n_{2}) ∪ ⋃{a : n′|τ : n′ ∈ n_{1} ∪ n_{2}} ∪ a : {⊥}
=_{NST} a : (n_{1} ∪ n_{2}) ∪ ⋃{a : n′|τ : n′ ∈ n_{1} ∪ n_{2}} ∪ a : {⊥}∪

a : n_{2} ∪ ⋃{a : n′_{2}|τ : n′_{2} ∈ n_{2}} ∪ a : {⊥} ( as a : {⊥} ^{⊑}_{NST} a : n_{2} ^{⊑}_{NST} a : (n_{1} ∪ n_{2}) by (2))

=  a_{NST}.(n_{1} +_{NST} τ_{NST}.n_{2}) +_{NST} a_{NST}.n_{2}

⊥ ∉ n_{2}:

a_{NST}.(n_{1} +_{NST} τ_{NST}.n_{2})

= a_{NST}.(n_{1} ∪ τ : n_{2} ∪ n_{2})
= a : (n_{1} ∪ τ : n_{2} ∪ n_{2}) ∪ ⋃{a : n′|τ : n′ ∈ n_{1} ∪ n_{2}}

∪a : n_{2} ∪ {a : {⊥}|⊥ ∈ n_{1}}

= a : (n_{1} ∪ τ : n_{2} ∪ n_{2}) ∪ ⋃{a : n′|τ : n′ ∈ n_{1} ∪ n_{2}}∪

a : n_{2} ∪ {a : {⊥}|⊥ ∈ n_{1}}∪ a : n_{2} ∪ ⋃{a : n′|τ : n′ ∈ n_{2}}

= a_{NST}.(n_{1} +_{NST} τ_{NST}.n_{2}) +_{NST} a_{NST}.n_{2}.

Here we note that =_{NST} appears only once in the sequence of the proof above. All the other equalities are set equalities.

The completeness may be easily proved by induction on the combined depth of n and m using Lemma 2.12. (In fact we do not need the τ 2,τ 3 and Ω2 at all to prove the completeness as the preorder ^{⊑}_{NST} coincides with the strong bisimulation preorder ⊏_{∼}.) □

To obtain a Σ-preorder where the equation τ 1 is sound, we follow the suggestion after Example 2.15. This leads to the following definition (where =_{E} has the same meaning as in Section 2).

Definition 5.5 We define (K,^{⊑}_{K}, Σ_{K}) as follows:

1. K = {[n] | [n] = {n′ ∈ NST|n′ =_{E} n}}.

2. ^{⊑}_{K} is defined by

[n_{1}] ^{⊑}_{K} [n_{2}] iff ∃n′_{1}, n′_{2} ∈ NST.n′_{1} =_{E} n_{1}, n′_{2} =_{E} n_{2} and n′_{1} ^{⊑}_{NST} n′_{2}.

3. Σ_{K} is defined by

(a) nil_{K} = [∅] = {∅},

(b) Ω_{K} = [{⊥}] = {{⊥}},

(c) [n_{1}] +_{K} [n_{2}] = [n_{1} +_{NST} n_{2}],

(d) μ_{K}.[n] = [μ_{NST}.n]. □

We have the following lemma:

Lemma 5.6 1. For all n_{1}, n_{2} ∈ NST, [n_{1}] ^{⊑}_{K} [n_{2}] iff n_{1} ⊏_{≈}^{∗} n_{2}.

2. (K,^{⊑}_{K}, Σ_{K}) is a Σ − preorder.

3. The proof system E is sound and complete on (K,^{⊑}_{K}, Σ_{K}).

Proof It is easy to see that ^{⊑}_{K} is well defined this way, i.e. is independent of the representants for the classes [n_{1}] and [n_{2}]. As ^{⊑}_{NST}=⊏_{∼} on NST the first statement follows from the Characterization Theorem 2.17, and the fact that =_{E}⊆≈^{∗}. This in turn ensures that ^{⊑}_{K} is a preorder. To prove statement 2. it only remains to prove that the operators in Σ_{K} are well defined and monotonic. This is an easy consequence of the way they are defined and the fact that =_{E} is preserved by the operators in NST. What remains to proof is therefore statement 3., the soundness and the completeness of the proof system E on (K,^{⊑}_{K}, Σ_{K}). To prove this we proceed as follows:

Soundness: The only non trivial case is the soundness of τ 1. So assume n ∈ NST and we will prove that μ_{K}.τ_{K}.[n] =_{K} μ_{K}.[n]. We recall that by definition of =_{E},

μ_{NST}.τ_{NST}.n =_{E} μ_{NST}.n.

This implies

μ_{K}.τ_{K}.[n] =_{K} [μ_{NST}.(τ_{NST}.n)] =_{K}
[μ_{NST}.n] =_{K} μ_{K}.[n].

Completeness: It is easy to see that the equations in E are derivable from E. So let n_{1}, n_{2} ∈ NST and we have the following:

[n_{1}] ^{⊑}_{K} [n_{2}]
implies ∃n′_{1}, n′_{2} ∈ NST.n_{1} =_{E} n′_{1} ^{⊑}_{NST} n′_{2} =_{E} n_{2} by definition
implies ∃n′_{1}, n′_{2} ∈ NST.n_{1} =_{E} n′_{1} ^{⊑}_{E} n′_{2} =_{E} n_{2}  by Lem. 5.6
implies n_{1} ^{⊑}_{E} n_{2}.
□

We have the following result:

Lemma 5.7 1. For all d ∈ F inT ree, K[[d]] = [NST[[d]]].

2. For each k ∈ K there is an η ∈ NF such that K[[η]] = k.

Proof

1. The mapping [NST[[ ]]] is an interpretation of F inT rees in K. The result follows by uniqueness of such mappings.

2. By definition of K, k = [n] for some n ∈ NST. By a simple induction on the depth of n we may show that there exists a η ∈ NF such that NST[[η]] = n. By part 1. we get

K[[η]] = [NST[[η]]] = k.
□

5.1 Soundness, Completeness and Full Abstractness for T rees

We complete the construction of the the full domain by taking (\overline{K},^{⊑}\overline{K}, Σ\overline{K}) to be the unique Σ-domain generated by (K,^{⊑}_{K}, Σ_{K}) as described in Chapter 4. The following theorem is standard and is proved in e.g. [Hen88b].

Theorem 5.8 For all p ∈ T rees, \overline{K}[[p]] = ⨆_{n} \overline{K}[[p^{n}]].

Now we have the following equivalence result:

Theorem 5.9 For all p_{1}, p_{2} ∈ T rees

\overline{K}[[p_{1}]] ^{⊑}\overline{K} \overline{K}[[p_{2}]] iff p_{1} ^{⊑}_{E_{rec}} p_{2} iff p_{1} ⊏_{≈}^{∗} p_{2}.

Proof That p_{1} =_{E_{rec}} p_{2} iff p_{1} ⊏_{≈}^{∗} p_{2} is the content of Theorem 3.4. Therefore we only have to prove that \overline{K}[[p_{1}]] ^{⊑}\overline{K} \overline{K}[[p_{2}]] iff p_{1} =_{E_{rec}} p_{2}, i.e that the proof system E_{rec} is sound and complete with respect to the denotational model.

Soundness: The soundness of the (ω)-rule is the content of Theorem 5.8 whereas the soundness of the (rec)-rule follows from the definition of the semantics of rec.p as the least fixed point. It remains to prove the soundness of E. We do this by reducing the proof to a proof of the soundness over F inT rees with respect to K. For this purpose we need the following property:

p ^{⊑}_{E} q ⇒ ∀n.p^{n} ^{⊑}_{E} q^{n}  (3)

which may be proved by induction on the depth of the proof for p ^{⊑}_{E} q. The soundness of E over F inT rees with respect to K follows directly from the soundness of E in K. To prove the general result, i.e. the soundness of E over T rees with respect to \overline{K}, we may proceed as follows.

Assume p ^{⊑}_{E} q. Then, by (3), p^{n} ^{⊑}_{E} q^{n} for all n. As p^{n}, q^{n} ∈ F inT rees, the soundness of E with respect to K implies

K[[p^{n}]] ^{⊑}_{K} K[[q^{n}]] for all n,

or equivalently

\overline{K}[[p^{n}]] ^{⊑}\overline{K} \overline{K}[[q^{n}]] for all n.

Finally Theorem 5.8 implies

\overline{K}[[p]] ^{⊑} \overline{K}[[q]].

Completeness: Again we reduce the proof to proving that E is complete over F inT rees with respect to K. We first note that Theorem 5.8 and the ω-algebraicity of the model imply

\overline{K}[[p]] ^{⊑}\overline{K} \overline{K}[[q]]  implies
∀n.\overline{K}[[p^{n}]] ^{⊑}\overline{K} \overline{K}[[q]]  implies
∀n∃m.\overline{K}[[p^{n}]] ^{⊑}\overline{K} \overline{K}[[q^{m}]] implies
∀n∃m.K[[p^{n}]] ^{⊑}_{K} K[[q^{m}]].

(4)

If E is complete over F inT rees with respect to K then

K[[p^{n}]] ^{⊑}_{K} K[[q^{m}]] implies p^{n} ^{⊑}_{E} q^{m}.  (5)

Now q^{m} ^{⊑}_{E_{rec}} q may easily be shown so (4), (5) and the ω-rule give

\overline{K}[[p]] ^{⊑}\overline{K} \overline{K}[[q]] implies ∀n.p^{n} ^{⊑}_{E_{rec}} q implies p ^{⊑}_{E_{rec}} q.

So it only remains to prove the completeness of E over F inT rees with respect to K. Furthermore, by the the normalization Theorem 3.7, it is sufficient to prove the completeness over normal forms. To prove this completeness result we proceed as follows:

Assume η_{1}, η_{2} ∈ NF. By Lemma 5.2 and Lemma 5.7

K[[η_{i}]] = [NST[[η_{i}]]] = [G(η_{i})]

for i = 1, 2. Therefore we have:

K[[η_{1}]] ^{⊑}_{K} K[[η_{2}]]
iff [G(η_{1})] ^{⊑}_{K} [G(η_{2})]
iff G(η_{1}) ⊏_{≈}^{∗} G(η_{2})  by Lem. 5.6
iff η_{1} ⊏_{≈}^{∗} η_{2}  by definition of the op. sem.
iff η_{1} ^{⊑}_{E} η_{2}  as E is complete wrt. ⊏_{≈}^{∗} .
□

6 Conclusion and Future Work

Regarding the picture being drawn in the introduction about ways of getting fully abstract denotational models for concurrent languages with an observational preorder, we have obtained the following: By giving a set of inequations, we have found a way of having a term model. Also, we have constructed a syntax free model which is the ideal completion of a preordered set whose elements are finite synchronization trees like the ones that appear in the representation of Abramsky’s model for strong bisimulation preorder. These trees are a representation of transition graphs in normal forms which in turn are derived as the operational semantics for syntactic normal forms in the sense of [Wal90]. By defining the operators in a suitable way we obtained a Σ-preorder. Unfortunately the Σ-domain obtained directly as an ideal closure of this Σ-preorder does not satisfy the set of equation that characterize the ω-observational congruence as the equation μ.τ.x = μ.x is not sound in this domain. We obtain a fully abstract model as a further abstraction of this model; roughly speaking we factor out the missing equation and obtain a fully abstract model with respect to the behavioural preorder we had in mind.

What is still missing, is the last part: Finding a mathematical description of the model which does not mention equations at all. This has proved to be more difficult than we first expected. To illustrate the kind of difficulties one runs into, let us consider a related successful attempt of doing something like this. In [Abr91], Abramsky defines a fully abstract denotational model for synchronization trees with respect to strong bisimulation precongruence. It is given as the solution of the recursive domain equation

D ≅ P( ∑_{μ∈Act_{τ}} D)

where P is a variant of the Plotkin (or convex) power construction (including the empty set) and ∑ is a lifted disjoint union. His proof that this is indeed a fully abstract model for the feature in question is quite longish, but there is a shortcut to convince oneself that this is what one wants: Strong bisimulation precongruence can be characterized in terms of the equations A1 to A4 which say that + is idempotent, symmetric, associative and has a unit. There are no (in)equations concerning prefixing and in particular no (in)equations connecting prefixing with +. It is then not hard to see that the initial solution to the above domain equation is exactly the free Σ-domain for the empty set of generators where the equations A1 to A4 hold and where the set of operators Σ contains + as well as a unary operator for every element of Act_{τ}. The fact that this Σ-domain can be presented in such an appealing way crucially depends on the simplicity of the equations describing the modelled precongruence.

Since the domain we are looking for is the free Σ-domain for the same set of actions but with the additional inequations Ω1, Ω2 and τ 1 to τ 3, the domain we are looking for is a quotient of the one given by Abramsky (the mathematical details of this process can be found in [AJ95]). Although this is a mathematical definition, it is not quite what we had in mind since it doesn’t not give much insight into the semantics - forming quotients of this kind is a somewhat obscure process. It is our aim to find another way of presenting this Σ-domain, if possible also as the solution of a recursive domain equation.

A

In what follows we will prove Theorem 2.14. For this purpose we need the following definition.

Definition A.1 ([Wal90]) Given R ∈ Rel(P) we define s_{1}R^{⋄}s_{2} by: s_{1}R^{⋄}s_{2} iff

1. if s_{1} ⟶^{μ} s′_{1} then, for some s′_{2}, s_{2} ⟶^{μ} s′_{2} and s′_{1}Rs′_{2}

2. if s_{1} ↓ then

(a) s_{2} ↓

(b) if s_{2} ⟶^{μ} s′_{2} then, for some s′_{1}, s_{1} ⟶^{μ} s′_{1} and s′_{1}Rs′_{2}

□

Theorem 2.14 is a direct consequence of the following Lemma.

Lemma A.2 For all n_{1}, n_{2} ∈ NST

1. n_{1} ⊏_{≈} n_{2} ⇔ n_{1} ⊏_{≈}_{g} n_{2},

2. n_{1} ⊏_{≈}^{∗} n_{2} ⇔ n_{1} ⊏_{≈}_{g}^{◇} n_{2},

1. The “⟸” part is proved in [Wal90, Lemma 7]. Therefore we only have to concentrate on proving the “⟹” part, i.e that ⊏_{≈}⊆⊏_{≈}_{g}. By definition

⊏_{∼}_{g}= ⋃{R|R ⊆ F_{w}^{g}(R)}.

It is therefore sufficient to prove that ⊏_{≈}⊆ F_{w}^{g}(⊏_{≈}). First we recall that for normal forms n, n ⟹^{μ} n′ iff n ⟶^{μ} n′ and n ⇓ iff n ↓. Now we proceed as follows: Assume m_{1} ⊏_{≈} m_{2}. As ⊏_{≈} is a fixed point to F_{w} then m_{1}F_{w}(⊏_{≈})m_{2}. We will prove that m_{1}F_{w}^{g}(⊏_{≈})m_{2}.

(a) Assume m_{1} ⟶^{μ} m′_{1}. Then there is a m′_{2} such that m_{2} ⟶^{μ} m′_{2} and

m′_{1} ⊏_{≈} m′_{2}.

(b) Assume m_{1} ↓, then m_{2} ↓ as m_{1} ⊏_{≈} m_{2}.

(c) Assume that m_{1} ↓, m_{2} ↓ and m_{2} ⟶^{a} m′_{2}. We have the following cases:

m_{1} ⇓ a: As m_{1} ⊏_{≈} m_{2} then m_{2} ⇓ a and m_{1} ⟶^{a} m′_{1} for some m′_{1}

such that m′_{1} ⊏_{≈} m′_{2}. m_{1} ⇑ a: As m_{1} ↓ this implies that ⟨a, {⊥}⟩ ∈ m_{1}. Therefore

m_{1} ⟶^{a} {⊥} where {⊥} ⊏_{≈} m′_{2}.

(d) Finally assume m_{1} ↓, m_{2} ↓ and m_{2} ⟶^{τ} m′_{2}. Then there exists a m′_{1}

such that m_{1} ⟹^{ε} m′_{1} and m′_{1} ⊏_{≈} m′_{2}.

2. By part 1 it is sufficient to prove that

n_{1} ⊏_{≈}_{g}^{∗} n_{2} ⇔ n_{1} ⊏_{≈}_{g}^{◇} n_{2}

We only prove the “⟸” part as the “⟹” part may be proved in the same way as the “⟹” part for the previous case, part 1. Assume n_{1} ⊏_{≈}_{g}^{◇} n_{2}.

(a) Assume n_{1} ⟶^{μ} n′_{1}. As n_{1} ⊏_{≈}_{g}^{◇} n_{2}, there is a n′_{2} such that n_{2} ⟶^{μ} n′_{2}

and n′_{1} ⊏_{≈}_{g} n′_{2}.

(b) i. If n_{1} ⇓ τ then n_{2} ⇓ τ by definition of ⊏_{≈}_{g}^{◇} and as ↓ and ⇓ coincide

on NST. ii. Next assume that n_{1} ⇓ τ, n_{2} ⇓ τ and n_{2} ⟹^{ε} n′_{2}. By definition

of ⊏_{≈}_{g}^{◇}, n_{1} ⟹^{τ} n′_{2} for some n′_{1} where n′_{1} ⊏_{≈}_{g} n′_{2}.

(c) i. Assume n_{1} ⇓ a. We will prove that n_{2} ⇓ a. As n_{1} ⇓ then n_{2} ⇓. So assume n_{1} ⇓, n_{2} ⇓ and n_{1} ⇓ a but that n_{2} ⇑ a. This implies that ⟨a, {⊥}⟩ is an element in n_{2} but not in n_{1}. It is easy to see that this contradicts the fact that n_{1} ⊏_{≈}_{g}^{◇} n_{2} and that n_{1} and n_{2} are normal forms.

ii. Next assume that n_{1} ⇓ a, n_{2} ⇓ a and n_{2} ⟶^{a} n′_{2}. Since n_{1} ⊏_{≈}_{g}^{◇} n_{2},

n_{1} ↓ and n_{2} ↓ then n_{1} ⟶^{a} n′_{1} for some n′_{1} such that n_{1} ⊏_{≈}_{g} n′_{1}.

□

References

[Abr91] S. Abramsky. A domain equation for bisimulation. Information and Computation, 92:161–218, 1991.

[AH92] L. Aceto and M. Hennessy. Termination, deadlock and divergence. Journal of the ACM, 39(1):147–187, January 1992.

[AJ95] S. Abramsky and A. Jung. Domain theory. In Handbook of Logic in Computer Science. Oxford University Press, 1994.

[Gue81] I. Guessarian. Algebraic Semantics, volume 99 of Lecture Notes in Computer Science. Springer-Verlag, 1981.

[Hen81] M. Hennessy. A term model for synchronous processes. Information and Computation, 51(1):58–75, 1981.

[Hen85] M. Hennessy. Acceptance trees. Journal of the ACM, 32(4):896–928, 1985.

[Hen88a] M. Hennessy. Algebraic Theory of Processes. MIT Press, Cambridge, Massachusetts, 1988.

[Hen88b] M. Hennessy. Axiomatising finite concurrent processes. SIAM Journal on Computing, 17(5):997–1017, 1988.

[Ing95] A. Ingólfsdóttir. A semantic theory for value-passing processes late approach — Part I: A denotational model and its complete axiomatization. Report RS–95–3, brics, Institute for Electronic Systems, Department of Mathematics and Computer Science, Aalborg University Centre, 1995.

[Kel76] R.M. Keller. Formal verification of parallel programs. Communications of the ACM, 19(7):371–384, 1976.

[Mil80] R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.

[Mil81] R. Milner. Modal characterisation of observable machine behaviour. In G. Astesiano and C. Bohm, editors, Proceedings CAAP 81, volume 112 of Lecture Notes in Computer Science, pages 25–34. Springer-Verlag, 1981.

[Mil83] R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25:267–310, 1983.

[Mil89] R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989.

[Par81] D.M.R. Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, 5^{th} GI Conference, volume 104 of Lecture Notes in Computer Science, pages 167–183. Springer-Verlag, 1981.

[Plo81] G.D. Plotkin. Lecture notes in domain theory, 1981. University of Edinburgh.

[SS71] D.S. Scott and C. Strachey. Towards a mathematical semantics for computer languages. In Proceedings of the Symposium on Computers and Automata, volume 21 of Microwave Research Institute Symposia Series, 1971.

[Sti87] C. Stirling. Modal logics for communicating systems. Theoretical Computer Science, 49:311–347, 1987.

[Wal90] D.J. Walker. Bisimulation and divergence. Information and Computation, 85(2):202–241, 1990.

Recent Publications in the BRICS Report Series

RS-95-40 Anna Ing� olfsd� ottir and Andrea Schalk. A Fully Abstract Denotational Model for Observational Congruence. August 1995. 29 pp.

RS-95-39 Allan Cheng. Petri Nets, Traces, and Local Model Checking. July 1995. 32 pp. Full version of paper appearing in Proceedings of AMAST ’95, LNCS 936, 1995.

RS-95-38 Mayer Goldberg. G� odelisation in the λ-Calculus. July 1995. 7 pp.

RS-95-37 Sten Agerholm and Mike Gordon. Experiments with ZF Set Theory in HOL and Isabelle. July 1995. 14 pp. To appear in Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and its Applications, LNCS, 1995.

RS-95-36 Sten Agerholm. Non-primitive Recursive Function De�nitions. July 1995. 15 pp. To appear in Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and its Applications, LNCS, 1995.

RS-95-35 Mayer Goldberg. Constructing Fixed-Point Combinators Using Application Survival. June 1995. 14 pp.

RS-95-34 Jens Palsberg. Type Inference with Selftype. June 1995. 22 pp.

RS-95-33 Jens Palsberg, Mitchell Wand, and Patrick O’Keefe. Type Inference with Non-structural Subtyping. June 1995. 22 pp.

RS-95-32 Jens Palsberg. Ef�cient Inference of Object Types. June 1995. 32 pp. To appear in Information and Computation. Preliminary version appears in Ninth Annual IEEE Symposium on Logic in Computer Science, LICS ’94 Proceedings, pages 186�195.

RS-95-31 Jens Palsberg and Peter �rb�k. Trust in the λ-calculus. June 1995. 32 pp. To appear in Static Analysis: 2nd International Symposium, SAS ’95 Proceedings, 1995.