Models for Name-Passing Processes: Interleaving and Causal

Gian Luca Cattani^{∗} and Peter Sewell^{†} Computer Laboratory University of Cambridge England

         {Luca.Cattani,Peter.Sewell}@cl.cam.ac.uk

September 2000

Abstract

We study syntax-free models for name-passing processes. For interleaving semantics, we identify the indexing structure required of an early labelled transition system to support the usual π-calculus operations, defining Indexed Labelled Transition Systems. For noninterleaving causal semantics we define Indexed Labelled Asynchronous Transition Systems, smoothly generalizing both our interleaving model and the standard Asynchronous Transition Systems model for CCS-like calculi. In each case we relate a denotational semantics to an operational view, for bisimulation and causal bisimulation respectively. We establish completeness properties of, and adjunctions between, categories of the two models. Alternative indexing structures and possible applications are also discussed. These are first steps towards a uniform understanding of the semantics and operations of name-passing calculi.

Contents

1 Introduction 3 2 Background on the π-calculus 7 3 N -LTS 10 4 Denotational semantics 15 5 N -LATS 22 6 Relating N -LTSs and N -LATSs 27 7 Alternative indexing structure 30 8 Future work and applications 31 A Proof of Theorem 5.6 35

∗supported by EPSRC grant GR/L62290: Calculi for Interactive Systems: Theory and Experiment †supported by a Royal Society University Research Fellowship

1 Introduction

The study of concurrency has involved rich interplay between model-theoretic and syntactic approaches. The first takes a notion of behaviour – perhaps defined as some class of automata or labelled transition systems – as primary; the second focuses on some particular signature of process terms, perhaps giving it only an axiomatic semantics. It is now common to take an intermediate approach: to fix a signature of process terms and equip it with an operational semantics defining behaviour (e.g. transition relations) over those terms. This has been followed for almost all work on π-calculi, beginning with [40], in which an operational semantics defines transition relations with particular labels over π-terms. By contrast, in this paper we study purely model-theoretic notions of behaviour for π-calculi, with definitions that do not involve process syntax, to support the uniform development of metatheory for a range of calculi and semantics. For interleaving semantics we introduce Indexed Labelled Transition Systems with data specifying how transitions change under renaming – thus picking out the essential structure of a π early transition relation that is required for defining the normal operations and equivalences over π-terms. For non-interleaving causal semantics, we define Indexed Labelled Asynchronous Transition Systems, smoothly generalizing both our interleaving model and the standard Asynchronous Transition Systems model for CCS-like calculi [3, 55, 58]. In each case we give a denotational semantics of a π-calculus; we prove that the operational early and causal bisimulations [47, 6] coincide with model-theoretic notions. We also establish completeness properties of and adjunctions between categories of the two models, as first steps towards a uniform understanding of the semantics and operations of name-passing calculi. A number of alternative structures and applications of the models can be envisaged, including applications to model-checking and security reasoning; we briefly outline some possible directions.

Interleaving The standard notion of labelled transition system (LTS) for calculi without value-passing is straightforward. For example, given a set N of channel names (ranged over by a, b, …) the CCS fragment

P ::= 0 | \overline{a}.P | a.P | P | Q | (νc)P

can be given semantics in terms of LTSs

⟨S, ⟶, i⟩

where S is a set of states, ⟶⊆ S×L×S is a transition relation with labels L = \{τ, a, \overline{a}, b, \overline{b}, … \}, and i ∈ S is the initial state. Introducing value-passing, however, makes the situation more complex – particularly with scope extrusion. Consider the π-calculus fragment below, in which the ‘c’ in the input bc.P and restriction (νc)P bind in the process P.

P ::= 0 | \overline{a}d.P | bc.P | P | Q | (νc)P

Defining the behaviour of bc.P involves substitution. For example, the communication of a free name

\overline{a}d.P | ac.Q ⟶^{τ} P | \{^{d}/_{c}\}Q

is inferred in the ‘early’ semantics of [41, 47] with the rules below.

Out \overline{\overline{a}d.P ⟶^{\overline{a}d} P} In \overline{ac.Q ⟶^{ad} \{^{d}/_{c}\}Q}

Com \frac{P ⟶^{\overline{a}d} P′ Q ⟶^{ad} Q′}{P | Q ⟶^{τ} P′ | Q′}

Note that d might or might not be in the free names of Q. Moreover, unlike in CCS, π-calculus τ-transitions can also involve scope extrusion:

((νd)\overline{a}d.P) | ac.Q ⟶^{τ} (νd)(P | \{^{d}/_{c}\}Q) if d ∉ fn(Q)

To define the τ-transitions of P | Q compositionally, in terms of the transitions of P and Q, the semantics must distinguish between outputs of free and bound names, by taking transitions with labels \overline{a}d and \overline{a}(d) respectively. The τ-transition above can be inferred with the rules:

Open \frac{P ⟶^{\overline{a}d} P′ d ≠ a}{(νd)P ⟶^{\overline{a}(d)} P′}

Close \frac{P ⟶^{\overline{a}(d)} P′ Q ⟶^{ad} Q′ d ∉ fn(Q)}{P | Q ⟶^{τ} (νd)(P′ | Q′)}

The full semantics requires also the rules

Res \frac{P ⟶^{ℓ} P′ d ∉ fn(ℓ)}{(νd)P ⟶^{ℓ} (νd)P′}

Par \frac{P ⟶^{ℓ} P′ bn(ℓ) ∩ fn(Q) = ∅}{P | Q ⟶^{ℓ} P′ | Q}

(in which bn(\overline{a}(d)) = \{d\}, and bn(ℓ) = ∅ for labels of other forms) for restricted transitions that do not involve scope extrusion and for parallel.

These SOS rules involve subtle conditions on the free names of process terms (relating them to names in labels), in addition to name substitution on process terms. To give a syntax-free notion of LTS that has enough structure to define the operations we must therefore consider states not simply to be elements of an arbitrary set but of a set indexed by finite sets of names – the ‘free’ names of the states – and add data specifying how states change under renaming. In Section 3 we will define an Indexed Labelled Transition System (or N -LTS) to have data

⟨S: N → Set, ⟶, ⟨I, i⟩⟩

where S is a functor from an indexing category N of name-sets and renamings into Set (the category of all sets and functions), giving the set of states above each name-set; the transition relation is over the coproduct ∐_{A∈|N |} S(A); and the initial state ⟨I, i⟩ is an element of that coproduct. Axioms must be imposed, enforcing:

1. the name-sets of the endpoints of a transition must be related to each other and to the label;

2. input transitions occur in families related by renaming of the result states;

3. (a) transitions are preserved by injective renaming, both of the names of states and of

new names in labels;

(b) inputs of new names above a name-set give rise to inputs of old names above larger name-sets; and

4. the transitions of an injective renaming of a state are determined by the transitions of the state.

We give the precise definition of N -LTS in Section 3, following a description of the π-calculus we are using in Section 2. We also introduce categories N -LTS_{I} (for each initial-name set I) of N - LTSs and study their completeness properties. Many variant definitions of N -LTS are possible; we discuss the alternatives in Section 7. In Section 4 we define constructions over N -LTSs, giving a denotational semantics, and relate bisimulation over N -LTSs with the bisimulation defined using the operational semantics.

Non-Interleaving models for process calculi have been much studied; they can support modelchecking techniques that mitigate the state-explosion problem, and strong proof techniques. They are also required in cases where the desired properties of systems are most naturally stated in terms of causality or locality. Here again there are model-theoretic and syntactic approaches – the first is surveyed in [58]; the second is represented by various annotated operational semantics, e.g. [16, 8, 15, 32, 58]. The two seem to have been carried out almost independently – to our knowledge, the only works to make precise connections are [16, 8, 58]. Moreover, only the syntactic approach has been developed to address name-passing, in the annotated operational models of [6, 18]. There is also work that does not fit this categorisation, having both syntactic and model-theoretic aspects, with Petri nets and graph rewriting [9, 42].

Our goal in the second half of this paper is to develop the model-theoretic approach, and to make precise connections to the annotated operational notions. We develop a simple syntax-free non-interleaving model for name-passing that generalises both our interleaving model and the standard Asynchronous Transition Systems model for calculi without name-passing [3, 55, 58]. This is precisely related to causal bisimulation [6].

In CCS causal dependency arises from prefixing – in the behaviour of the process \overline{x}.\overline{y}.0 the y output causally depends on the x output. In π-calculus, name-binding introduces new dependencies, as thoroughly discussed in [18]. Transitions occurring in different parallel components of a process term, naively regarded as independent, may be forced to occur in a fixed order. For example, in the process (νy)(\overline{x}y | \overline{y}z) the transition \overline{y}z can be observed only after \overline{x}y – before this occurs the new-bound channel is not known to the environment. The two transitions of (νy)(\overline{x}y | \overline{z}y) are independent, however, despite the fact that the first to occur will be an output of a new name and the second will not. Further, an input of a previously-extruded name, e.g. (νy)(\overline{x}y | xw.0) ⟶^{\overline{x}y}⟶^{xy} 0, or output of a previously-input new name, e.g. xw.\overline{x}w ⟶^{xy}⟶^{\overline{x}y} 0 (where y is new) involves dependency. Moreover, one can choose whether or not to distinguish between the prefix and name dependency, e.g. whether to identify (νy)(\overline{x}y.\overline{y}z) and (νy)(\overline{x}y | \overline{y}z).

In Section 5 we define a relation of name-dependency between two labels (wrt. a name-set), and then an Indexed Labelled Asynchronous Transition System (or N -LATS) to have data

⟨S: N → Set, ⟶, ⟨I, i⟩, E, I⟩

where now transitions are annotated by elements of a set E of events and I ⊆ E × E is an independence relation between events. We impose axioms requiring that one obtains an Indexed LTS when considering each e ∈ E separately, and (roughly), that independent transitions can be permuted. As one would expect, name dependency is involved in the relationship between the transition and independence relations. We discuss how the constructions of Section 4 can be extended to N -LATS, define history-preserving bisimulation and a name-dependency aware variant (respectively distinguishing and identifying the example two processes above), and prove correspondence results.

In Section 6 we continue the abstract study of the structures defined in the paper. We define categories N -LATS_{I} of Indexed LATS (each for initial name-set I) and study their completeness properties as well as their relationship with the categories N -LTS_{I}. These are first steps towards an abstract understanding of the equivalences and constructions involved in the semantics of π-like process languages.

Further Motivation, Future Directions and Related Work Viewing models categorically has proven useful in study of the interleaving/non-interleaving and linear-time/branching-time distinctions [49]. Moreover, the categorical study of process calculi gives the possibility of obtaining general congruence results: in [58] categorical models of CCS-like processes are axiomatised and in [31] an abstract model-theoretic notion of bisimulation is introduced (via open maps); in [13, 14] these two are combined to give abstract congruence results for strong bisimulation over a wide range of models. It is our hope that the present work serves as a first step towards similar results for π-calculus-like process languages. In particular, we would like a categorical understanding of our operations for the two models, related by the results presented in Section 6. One could then use these results to address the problem of giving causal semantics to variants of the π-calculus, e.g. the box-π of [53, 54], for which an approximate notion of causality is used to state security properties. Preliminary discussion of this, and of other future directions, can be found in Section 8.

Among earlier models of π-processes, the name passing synchronisation trees of [27] and presheaves of [12] are the closest to our N -LTS, though they employ a slightly different indexing structure (cf. Section 7). In [12] the models are defined using domain theoretical techniques similar to those employed in [56, 20], as the solutions to semantic equations. By contrast here we take a more concrete approach, with several advantages. Firstly, it is easy to conceive of minor modifications to our definitions to suit calculi such as the asynchronous π-calculus [7, 28]. In particular it should be quite straightforward to adapt the axioms of [50] to our models. It should also be easy to address the πI-calculus [48], in which only new names are communicated (though this can also be done domain-theoretically). Secondly, it supports a direct definition of weak bisimulation, something the domain model lacks completely and the presheaf model can, as far as we know, only achieve indirectly by means of a saturation construction [19].

It is also worth noticing that while the domain models are tailored for late bisimulation, our focus here is on early semantics, both to obtain a simpler notion of transition system, and because we have found the early style suits work on concurrent language semantics and on secure encapsulation [51, 53, 54, 52]. Presheaf models exist for both early and late notions [10]. Moreover we should add that, in contrast to [56, 20] (which have full-abstraction results wrt. strong bisimulation), we focus on intensional models, over which a number of equivalences can be defined (though we give results only for bisimulation). The literature contains also testing-based models [24, 4]. The precise relationships with these and other models defined in the literature, e.g. [42, 9, 30] requires further work.

More speculatively, we believe our structures may form a useful basis for π-calculus interleaving and partial-order model checking, via notions of finitely-generable N -LTS and N -LATS – the former of which may have interesting relationships with the HD-automata of [43], and wonder what the relationships are with the recent [22, 21, 26], where similar indexing structure is used in a λ-calculus setting.

Finally, notice that in this paper we introduce transition systems with indexed sets of states, but not indexed sets of transitions. This is because, as remarked above, when moving from a name-set to a larger one, transitions labelled with inputs of new names in the former give rise to input transitions of both new and old names in the latter – the correspondence between transitions is not functional, even for injective renamings. It may be possible to use more sophisticated indexing structures which allow transitions as well as states to be indexed; the pay-off for the extra complication being e.g. the possibility of using the notion of internal category to formally relate our Indexed Transition Systems with the standard ones.

This paper is a full and extended version of [11].

Out \overline{A ⊢ \overline{x}v.P ⟶^{\overline{x}v} P}  In \overline{A ⊢ xp.P ⟶^{xv} \{^{v}/_{p}\}P}

Tau \overline{A ⊢ τ.P ⟶^{τ} P}  Sum \frac{A ⊢ P ⟶^{ℓ} P′}{A ⊢ P + Q ⟶^{ℓ} P′}

Par \frac{A ⊢ P ⟶^{ℓ} P′}{A ⊢ P | Q ⟶^{ℓ} P′ | Q}  Com \frac{A ⊢ P ⟶^{\overline{x}v} P′ A ⊢ Q ⟶^{xv} Q′}{A ⊢ P | Q ⟶^{τ} (ν\{v\} \ A)(P′ | Q′)}

Res \frac{A, x ⊢ P ⟶^{ℓ} P′ x ∉ fn(ℓ)}{A ⊢ (νx)P ⟶^{ℓ} (νx)P′} Open \frac{A, x ⊢ P ⟶^{\overline{y}x} P′ y ≠ x}{A ⊢ (νx)P ⟶^{\overline{y}x} P′}

Match \frac{A ⊢ P ⟶^{ℓ} P′}{A ⊢ [x = x]P ⟶^{ℓ} P′}  Mismatch \frac{A ⊢ P ⟶^{ℓ} P′ x ≠ y}{A ⊢ [x ≠ y]P ⟶^{ℓ} P′}

In all rules with conclusion of the form A ⊢ P ⟶^{ℓ} Q there is an implicit side condition fn(P) ⊆ A. Symmetric versions of Par, Com and Sum are elided.

Figure 1: π operational semantics

2 Background on the π-calculus

Many variant π-calculi have been studied in the literature since the original was introduced in [40]. Here, to show the wide applicability of our models, we take a rich set of primitives including summation, matching, mismatching and synchronous output. For notational simplicity, however, we treat only a monadic untyped calculus without basic values, and also omit replication. These could be easily added.

Syntax We take an infinite set N of names of channels, ranged over by a, b etc. The process terms are then those defined by the grammar

P, Q ::= 0  nil
P | Q  parallel composition
P + Q  choice
τ.P  internal action
\overline{a}d.P  output d on channel a
ac.P  input from channel a
(νc)P  new channel name creation
[a = b]P  match
[a ≠ b]P  mismatch

Here the c in the input bc.P and restriction (νc)P bind in the process P; we work up to alpha renaming of bound names. We write fn(P) for the set of free names of P, and {a/b}P for the process term obtained from P by replacing all free occurrences of b by a.

Operational semantics We equip the calculus with a mild variant, explicitly-indexed, of the early labelled transition semantics of [47, 41], in which transitions are given for processes with respect to explicit supersets of their free name sets. This style simplifies the SOS rules, allowing sideconditions in Par and Close (here coalesced with Com) to be removed, gives a simple notion of trace, and supports subtype systems; it has been useful for work on concurrent language semantics and on secure encapsulation [51, 53, 54]. It is related to the original semantics at the end of this section. The labelled transition relation has the form

A ⊢ P ⟶^{ℓ} Q

where A is a finite set of names and fn(P) ⊆ A; it should be read as ‘in a state where the names A may be known by process P and by its environment, the process P can do ℓ to become Q. The labels Lab are \{τ\} ∪ \{ \overline{x}y | x, y ∈ N \} ∪ \{ xy | x, y ∈ N \}. Note that we now have only one form of output label – a transition A ⊢ P ⟶^{\overline{x}v} Q is an output of a new name iff v ∉ A. The transition relation is defined as the smallest relation satisfying the rules in Figure 1. The free names of a label are fn(τ) = \{\}, fn(\overline{x}v) = fn(xv) = \{x, v\}. We write A, x for A ∪ \{x\} where x is assumed not to be in A. If A = ∅ then (νA)P denotes P.

Note that the set of free names of a process can grow along transitions, for example {a} ⊢ (νd)\overline{a}d.\overline{a}d ⟶^{\overline{a}d} \overline{a}d, and that the rules depend in an essential way on alpha-conversion – the process R = (νd)\overline{a}d must be able to perform a bound output with label \overline{a}d̂ for any d̂ ≠ a; derivations of such transitions require use of the alpha-equivalence R = (νd̂)\overline{a}d̂. Note also that the SOS rules do not involve any structural congruence.

Example Properties We illustrate the SOS with some example transitions and properties – these will be special cases of the axioms imposed on N -LTS in Section 3.

1. If A ⊢ P ⟶^{\overline{x}z} Q then x ∈ A. We might have z new, i.e. z ∉ A or not, i.e. z ∈ A. In either case, Q has free names contained in A ∪ {x, z}. The same holds for input transitions.

2. A transition A ⊢ P ⟶^{xz} Q must arise from an input prefix in P, which must therefore be able to input any other name (new or old). Moreover, the resulting states can all be obtained by substitution from the resulting state after a new name is input.

3. (a) If A ⊢ P ⟶^{\overline{x}z} Q and z ∈ A then for any injective substitution, say f : A →_{inj} B, there

is a transition B ⊢ fP ⟶^{\overline{fx}fz} fQ. For output of a new name, i.e. z ∉ A, the value z

can also be renamed to any ẑ ∉ B, giving B ⊢ fP ⟶^{\overline{fx}ẑ} (f + [ẑ/z])Q. The same holds for input transitions.

(b) A derivation of an input A ⊢ P ⟶^{xz} Q of a new name z ∉ A is preserved by extending the name-set – so P above (A, z) has an input of an old name A, z ⊢ P ⟶^{xz} Q.

4. Non-injective renaming can enable and (with mismatch) disable transitions, but the behaviour of an injective renaming of P is determined by that of P.

Operational Equivalences The normal notion of early bisimulation can be easily adapted to the explicitly-indexed setting. Take bisimulation ˙∼ to be the largest family of relations indexed by finite sets of names such that each ˙∼_{A} is a symmetric relation over { P | fn(P) ⊆ A } and for all P ˙∼_{A} Q,

• if A ⊢ P ⟶^{ℓ} P′ then ∃Q′ . A ⊢ Q ⟶^{ℓ} Q′ ∧ P′ ˙∼_{A∪fn(ℓ)} Q′.

We do not develop other equivalences in this paper, but linear-time notions can also be defined straightforwardly. For example, for partial traces write

A_{1} ⊢ P_{1} ⟶^{ℓ_{1}} … ⟶^{ℓ_{n}} P_{n+1}

to mean ∃P_{2}, …, P_{n}, A_{2}, …, A_{n} . ∀i ∈ 1..n . A_{i+1} = A_{i} ∪ fn(ℓ_{i}) ∧ A_{i} ⊢ P_{i} ⟶^{ℓ_{i}} P_{i+1}. If

fn(P) ⊆ A then the partial A-traces of P are simply { ℓ_{1} .. ℓ_{n} | ∃P′ . A ⊢ P ⟶^{ℓ_{1}} … ⟶^{ℓ_{n}} P′ }.

Out \overline{\overline{x}v.P ⟶^{\overline{x}v} P}  In \overline{xp.P ⟶^{xv} \{^{v}/_{p}\}P}

Tau \overline{τ.P ⟶^{τ} P}  Sum \frac{P ⟶^{μ} P′}{P + Q ⟶^{μ} P′}

Par \frac{P ⟶^{μ} P′ bn(μ) ∩ fn(Q) = ∅}{P | Q ⟶^{μ} P′ | Q}  Com \frac{P ⟶^{\overline{x}v} P′ Q ⟶^{xv} Q′}{P | Q ⟶^{τ} P′ | Q′}

Close \frac{P ⟶^{\overline{x}(v)} P′ Q ⟶^{xv} Q′ v ∉ fn(Q)}{P | Q ⟶^{τ} (νv)(P′ | Q′)}

Res \frac{P ⟶^{μ} P′ x ∉ n(μ)}{(νx)P ⟶^{μ} (νx)P′}  Open \frac{P ⟶^{\overline{y}x} P′ x ≠ y}{(νx)P ⟶^{\overline{y}(x)} P′}

Match \frac{P ⟶^{μ} P′}{[x = x]P ⟶^{μ} P′}  Mismatch \frac{P ⟶^{μ} P′ x ≠ y}{[x ≠ y]P ⟶^{μ} P′}

Symmetric versions of Par, Com, Close and Sum are elided.

Figure 2: π conventional early operational semantics

Conventional Early Semantics

We conclude this section by recalling the ‘conventional’ operational semantics, without explicit indexing sets, in the original style of [47, 41], and showing that the two early bisimulation relations coincide. The conventional labelled transition relation has the form

P ⟶^{μ} Q

where the label μ is taken from

μ ::= \overline{x}v | \overline{x}(v) | xv | τ

In the absence of an explicit index set outputs of old and new names must be distinguished in the label – as \overline{x}v and \overline{x}(v) respectively. The transitions are defined in Figure 2, which uses the following auxiliary functions for the free, ‘bound’ and all names of a label. Note that (despite the bn( ) notation) the semantics does not involve alpha conversion of labels.

\begin{matrix}μ & fn(μ) & bn(μ) & n(μ) \\ \overline{x}v & \{x, v\} & \{\} & \{x, v\} \\ \overline{x}(v) & \{x\} & \{v\} & \{x, v\} \\ xv & \{x, v\} & \{\} & \{x, v\} \\ τ & \{\} & \{\} & \{\} \end{matrix}

Again following [47, 41], take conventional early bisimulation ˙ ∼_{con} to be the largest symmetric relation over terms such that each for all P ˙ ∼_{con} Q,

• if P ⟶^{μ} P′ and bn(μ) ∩ fn(P, Q) = ∅ then ∃Q′ . Q ⟶^{μ} Q′ ∧ P′ ˙ ∼_{con} Q′.

Note that the conventional LTS includes pathological transitions such as \overline{x}v.0+(νv)\overline{x}v.P ⟶^{\overline{x}(v)} P, in which a name v both occurs free in the left hand side and is output as new. The condition bn(μ) ∩ fn(P, Q) = ∅ in the definition of bisimulation disregards such transitions, among others.

Lemma 2.1 If P ⟶^{μ} Q then fn(Q) ⊆ fn(P) ∪ n(μ).

Lemma 2.2 If P ˙∼_{A}P′ then P ˙∼_{fn(P,P′)}P′.

Lemma 2.3 If A ⊇ fn(P) then

1. A ⊢ P ⟶^{\overline{x}v} Q ∧ v ∈ A iff P ⟶^{\overline{x}v} Q

2. A ⊢ P ⟶^{\overline{x}v} Q ∧ v ∉ A iff P ⟶^{\overline{x}(v)} Q ∧ v ∉ A

3. A ⊢ P ⟶^{xv} Q iff P ⟶^{xv} Q

4. A ⊢ P ⟶^{τ} Q iff P ⟶^{τ} Q

Theorem 2.4 If A ⊇ fn(P, Q) then P ˙∼_{A}Q iff P ˙ ∼_{con}Q.

Proof: We check R = { P, P′ | ∃A . A ⊇ fn(P, P′) ∧ P ˙∼_{A}P′ } and R_{A} = { P, P′ | A ⊇ fn(P, P′) ∧ P ˙ ∼_{con}P′ } are bisimulations of the two forms. The first is straightforward using Lemmas 2.3 and 2.2. The second is straightforward using Lemmas 2.3 and 2.1.

□

3 N -LTS

In this section we introduce Indexed Labelled Transition Systems. To account for name substitution of π-terms, we take an indexing structure of name-sets and renaming functions on the set of states. We then axiomatize the key properties of the transition relation with respect to this indexing structure. We have also considered other choices of indexing structure, as briefly discussed in Section 7.

Definition 3.1 Take N to be the category with objects finite subsets of N and arrows functions f : A → B between them.

As before, given the fixed name set N, we define the set of π-labels as follows:

Definition 3.2 Define Lab to be the set \{τ\} ∪ \{xy | x, y ∈ N\} ∪ \{\overline{x}y | x, y ∈ N\}

Notation:

• If f : A → B and g: A′ → B′ are two functions we write f + g for the obvious function A ⊎ A′ → B ⊎ B′. If f : A → B and g: A′ → B we write [f, g] for the obvious copairing function A ⊎ A′ → B.

• Given two names x and y, write [y/x] for the unique function {x} → {y}. If f : A → B is a function with x ∉ A and y ∈ B, by abuse of notation, we write [f, [y/x]] for the obvious function A, x → B.

• If S : N → Set is a functor and if ∐_{A∈|N |} S(A) is the disjoint union of the sets S(A) for objects A of N, write ⟨A, s⟩ for the element s ∈ S(A) as an element of the disjoint union and S for the set ∐_{A∈|N |} S(A) itself.

• If ⟶⊆ S × Lab × S is a (transition) relation, we will write A ⊢ s ⟶^{ℓ} t to mean that there exists an s ∈ S(A), a set B and a t ∈ S(B) such that s = ⟨A, s⟩, t = ⟨B, t⟩ and s ⟶^{ℓ} t. Sometimes we want to make explicit the existence of B and write A ⊢ s ⟶^{ℓ} t ⊣ B to this purpose. Also if f : A → B is a function, write fs for ⟨B, S(f)(s)⟩.

• If S, S′: N → Set are two functors, s = ⟨A, s⟩ ∈ S and α: S ⟹ S′ is a natural transformation, we write αs for ⟨A, α_{A}s⟩ ∈ S′.

Definition 3.3 For any label ℓ ∈ Lab, define the channel names of ℓ, chan(ℓ) and the value names of ℓ, val(ℓ)as follows:

chan(τ) = ∅  val(τ) = ∅
chan(\overline{x}y) = \{x\}  val(\overline{x}y) = \{y\}
chan(xy) = {x}  val(xy) = {y}

Definition 3.4 Define an Indexed Labelled Transition System (N -LTS) to be a structure

T = ⟨S: N → Set, ⟶, i⟩

where i = ⟨I, i⟩ ∈ S, ⟶⊆ S × Lab × S and the following conditions hold.

1. (Naming) A ⊢ s ⟶^{ℓ} t ⊣ B ⟹ chan(ℓ) ⊆ A ∧ B = A ∪ fn(ℓ)

2. (a) (Input – new)A ⊢ s ⟶^{xy} t ⊣ A, y ⟹ ∀z ∈ A. A ⊢ s ⟶^{xz} [1_{A}, [z/y]]t

(b) (Input – old)A ⊢ s ⟶^{xy} t ⊣ A ⟹ ∀z ∉ A∃ t_{z}. A ⊢ s ⟶^{xz} t_{z} ⊣ A, z ∧ t = [1_{A}, [y/z]]t_{z}

3. (a) (Injective substitution)

For f : A →_{inj} B, A ⊢ s ⟶^{ℓ} t ∧ g:(fn(ℓ)\A) →_{bij} B̂ ∧ B̂∩B = ∅ ⟹ fs ⟶^{(f+g)ℓ} (f +g)t

(b) (Shifting)

A ⊢ s ⟶^{xy} t ⊣ A, y ⟹ A, y ⊢ ιs ⟶^{xy} t, where ι : A ↪ A, y is the set inclusion function

4. For f : A →_{inj} B, if fs ⟶^{ℓ′} t′ then one of the following two cases applies

(a) there exist ℓ, t, g: fn(ℓ)\A →_{bij} B̂ such that B̂ ∩B = ∅ and ℓ′ = (f +g)(ℓ) and s ⟶^{ℓ} t and t′ = (f + g)t

(b) there exist x ∈ A, y ∉ A, z ∈ B \ ran(f) and t such that ℓ′ = f(x)z and A ⊢ s ⟶^{xy} t ⊣ A, y and t′ = [f, [z/y]]t

Condition 1 ensures that communication with the environment occurs only along publicly known channels and that the knowledge of such channels is correctly propagated from one state to another when a transition occurs. Conditions 2 ensure that if a name can be received as input along a specific channel, then any other name can be received as well. Condition 3a asserts that transitions are preserved along injective renamings, while condition 3b shows how inputs of new names generate inputs of “old” names when moving from a name set to a larger one. Finally, condition 4 ensures that the transitions out of a state which has been injectively renamed are determined by those of the state itself (cf. the example properties of Section 2). Clause 4b differs from that stated in [11] by requiring z ∉ ran(f) – in the presence of the other axioms the two are equivalent, but this version is more elegant and supports the definition of N_{inj}-LTS in Section 7.

In fact the definition contains some redundancy:

Proposition 3.5 Condition 3b ‘shifting’ is implied by conditions 2a ‘input-new’ and 3a ‘injective substitution’.

Proof: Suppose that A ⊢ s ⟶^{xy} t ⊣ A, y, then by condition 3a, A, y ⊢ ιs ⟶^{xz} (ι+[z/y])t ⊣ A, y, z, for any z ∉ A, y. Thus by condition 2a we deduce that A, y ⊢ ιs ⟶^{xy} [1_{A,y}, [y/z]](ι+[z/y])t ⊣ A, y. But [1_{A,y}, [y/z]](ι + [z/y]) = [1_{A,y}ι, [y/z][z/y]] = [ι, 1_{{y}}] = 1_{A,y} and therefore A, y ⊢ ιs ⟶^{xy} t.

□

Despite this we keep condition 3b, for two reasons. Firstly, we regard the condition as conceptually important, thus we did not want to omit it from the main definition. Secondly, conditions 2a and 2b, introduced to ensure uniform behaviour of input transitions, can be argued to be unnecessary from the model-theoretic point of view (just as their analogues are neglected in the reduction of value-passing CCS to pure CCS [39]). When 2a and 2b are omitted, 3b becomes essential.

For illustrative purposes we list now a few simple consequences of Definition 3.4. Analogous properties of π-terms are often established as lemmas, e.g. to prove correspondence between labelled and reduction semantics (see [53, 52] for explicitly-indexed developments).

Proposition 3.6 (Weakening) If A ⊢ s ⟶^{ℓ} t and x ∉ A ∪ fn(ℓ) then ιs ⟶^{ℓ} ȷt, where ι: A ↪ A, x and ȷ: A ∪ fn(ℓ) ↪ (A ∪ fn(ℓ)), x.

Proof: Suppose that A ⊢ s ⟶^{ℓ} t and x ∉ A ∪ fn(ℓ) for some states s and t. Observe, first of all that by condition 3a A, x ⊢ ιs ⟶^{ℓ} (ι + g)t, for any g: fn(ℓ) \ A →_{bij} B, with B ∩ (A, x) = ∅. Choose then g to be 1_{fn(ℓ)\A}. Then ȷ = ι + g and so the required property is satisfied.

□

Proposition 3.7 (Strengthening) If A, x ⊢ ιs ⟶^{ℓ} t′, and x ∉ fn(ℓ), where ι: A ↪ A, x, then there exists t such that A ⊢ s ⟶^{ℓ} t and t′ = ȷt, where ȷ: A ∪ fn(ℓ) ↪ (A ∪ fn(ℓ)), x.

Proof: Suppose that A, x ⊢ ιs ⟶^{ℓ} t′ and x ∉ fn(ℓ) for some states s and t′. By condition 4, there can be two possibilities. It might be that there exist ℓ̄, t and g: fn(ℓ̄) \ A →_{bij} B such

that B ∩ A, x = ∅, ℓ = (ι + g)(ℓ̄), s ⟶^{ℓ̄} t and t′ = (ι + g)t. Because of the properties above and by condition 3a, s ⟶^{ℓ} (1_{A} + g)t. Moreover ȷ = (ι + g)(1_{A} + g^{−1}), thus ȷ(1_{A} + g)t = (ι + g)(1_{A} + g^{−1})(1_{A} + g)t = (ι + g)t = t′.

Otherwise, there exist x′ ∈ A, y ∉ A, z ∈ A, x and t̄ such that ℓ = x′z, A ⊢ s ⟶^{x′y} t̄ and t′ = [ι, [z, y]]t̄. Now, since x ∉ fn(ℓ), then it must be that z ∈ A. So by condition 2a,

A ⊢ s ⟶^{x′z} [1_{A}, [z/y]]t̄. Moreover ȷ = ι and [ι, [z/y]] = ι[1_{A}, [z/y]]. Thus, taking t = [1_{A}, [z/y]]t̄, gives us ȷt = t′.

□

Proposition 3.8 (Converse of Shifting) If A, y ⊢ ιs ⟶^{xy} t, where ι: A ↪ A, y, then A ⊢

s ⟶^{xy} t.

Proof: Suppose A, y ⊢ ιs ⟶^{xy} t, then either condition 4a or condition 4b must apply. Since y is not in A, 4a does not apply. Thus, by condition 4b there exist ŷ ∉ A and t̂, such that A ⊢ s ⟶^{xŷ} t̂ and t = [ι, [y/ŷ]]t̂. By condition 3a, we then have that A ⊢ s ⟶^{xy} (1_{A} + [y/ŷ])t̂. But

1_{A} + [y/ŷ] = [ι, [y/ŷ]], hence A ⊢ s ⟶^{xy} t.

□

The terms of the π-calculus can be easily structured into an indexed sets of states, leading to the interpretation of π-terms as N -LTSs all having the same set of states and transition relation, but different initial state.

Definition 3.9 For every π-term P with free names in A and function f : A → B, write fP for the π-term obtained by simultaneously substituting (avoiding capturing) f(x) for x in P, for every x ∈ A.

Definition 3.10 Define π: N → Set to be the following functor:

π(A) = {P | P is a π-term and fn(P) ⊆ A}
π(f)(P) = fP .

Definition 3.11 For every π-term P with free names in I, define

([P])_{I} = ⟨π, ⟶, ⟨I, P ⟩⟩

where ⟨A, Q⟩ ⟶^{ℓ} ⟨B, R⟩ if and only if A ⊢ Q ⟶^{ℓ} R according to the operational semantics of Figure 1 and B = A ∪ fn(ℓ).

It is simple to verify using the operational semantics that ([P])_{I} is a N -LTS.

In the next section we will provide a compositional semantics of π-terms as N -LTSs. Before doing so, we conclude this section by structuring the class of N -LTSs into a category and prove some of its main completeness and structural properties.

Definition 3.12 Define a morphism α: T_{1} → T_{2} between N -LTSs, with initial state over the same name-set I, to be a natural transformation α : S_{1} ⟹ S_{2} such that

1. αi_{1} = i_{2}

2. s ⟶^{ℓ} s′ implies αs ⟶^{ℓ} αs′.

Define N -LTS_{I} to be the category of N -LTSs with initial name-set I and these morphisms.

Theorem 3.13 For every name-set I, the category N -LTS_{I} is complete and cocomplete.

Proof: Completeness By a well-known result of category theory [36], it suffices to show that N -LTS_{I} has equalisers and small products.

\underline{Equalisers}: If T_{1} ^{α}_{β} T_{2} are two morphisms in N -LTS_{I}, define T_{0} = ⟨S_{0}, ⟶_{0}, i_{1}⟩ and γ :

T_{0} ↪ T_{1} as follows:

• S_{0} ^{γ} S_{1} ^{α}_{β} S_{2} is the equaliser in Set^{N}, defined as S_{0}(A) = {s ∈ S_{1}(A) | α_{A}(s) =

β_{A}(s)}, while γ_{A} is the inclusion function.

• ⟶_{0} is the largest subset of S_{0}×Lab×S_{0} which satisfies conditions 2b and 4 of Definition 3.4

and is such that

A ⊢ s ⟶^{ℓ}_{0} t ⊣ B ⟹ A ⊢ γ_{A}s ⟶^{ℓ}_{1} γ_{B}t ⊣ B.

It is a matter of easy verification to check that ⟶_{0} is well-defined, i.e. that such a largest subset exists as the partial order of transition relations in S_{0} × Lab × S_{0} satisfying conditions 2b and 4 is a complete lattice. Moreover all the other conditions of Definition 3.4 are met as a consequence of the fact that ⟶_{0} is essentially a subrelation of ⟶_{1}. The universal property

follows from the fact that the diagram S_{0} ^{γ} S_{1} ^{α}_{β} S_{2} is an equaliser in Set^{N}.

\underline{Products}: Let (T_{k})_{k∈K} be a family of transition systems. Define their product

T = ⟨S, ⟶, ⟨I, ⟨i_{k}⟩_{k∈K}⟩⟩

and (π_{k}: T → T_{k})_{k∈K} as follows:

• (π_{k}: S → S_{k})_{k∈K} is the product in Set^{N} of the S_{k}’s. That is, S(A) = {⟨s_{k}⟩_{k∈K} | s_{k} ∈ S_{k}(A)}, with S(f) and π_{k} defined in the obvious way.

• The transition relation is defined as A ⊢ s ⟶^{ℓ} t iff for every k, A ⊢ π_{k}s ⟶^{ℓ} π_{k}t.

It is very easy to verify that (π_{k}: T → T_{k})_{k∈K} satisfies the universal property of products.

The terminal object, i.e. the empty product is given by, ⟨1, ⟶, ⟨I, ⋆⟩⟩, where for every A, 1(A) = {⋆} and for every A and ℓ, ⟨A, ⋆⟩ ⟶^{ℓ} ⟨A ∪ fn(ℓ), ⋆⟩.

Cocompleteness Similarly, it suffices to show that N -LTS_{I} has coequalisers and small coproducts.

\underline{Coequalisers}: If T_{1} ^{α}_{β} T_{2} are two morphisms in N -LTS_{I}, define T_{0} = ⟨S_{0}, ⟶_{0}, i_{0}⟩ and

γ : T_{2} → T_{0} as follows:

• S_{1} ^{α}_{β} S_{2} ^{γ} S_{0} is a coequaliser in Set^{N}.

• ⟶_{0} is defined as s ⟶^{ℓ}_{0} t if there exists s̄ and t̄ such that γs̄ = s, γt̄ = t and s̄ ⟶^{ℓ}_{2} t̄.

• i_{0} =^{def} γi_{2}.

Naturality of γ ensures that T_{0} is an N -LTS and by the definition of ⟶_{0}, we immediately also have that γ is a morphism in N -LTS_{I}. The universal property follows from that of

S_{1} ^{α}_{β} S_{2} ^{γ} S_{0} .

\underline{Coproducts}: The initial object is 0_{I} = ⟨N (I, −), ∅, ⟨I, 1_{I}⟩⟩, where N (I, −) is the representable

functor [37], N (I, −)(A) =^{def} N (I, A) = {f | f : I → A}, N (I, −)(g)(f) =^{def} N (I, g)(f) = gf, for any g: A → B and f : I → A in N. Observe in fact that for any functor S: N → Set and element i ∈ S(I), there exists a unique natural transformation 0_{S} : N (I, −) → S such that 0_{S,I}(1_{I}) = i.

Suppose now that (T_{k})_{k∈K} is a family of N -LTS’s. Define T = ⟨S, ⟶, i⟩ and (in_{k}: T_{k} → T)_{k∈K} to be

• (in_{k}: S_{k} → S)_{k∈K} a colimit in Set^{N} of the wide-span diagram of vertex 0_{I} and edges (0_{S_{k}})_{k∈K} • i = in_{k}i_{k} (notice that it does not matter which k is chosen) and s ⟶^{ℓ} t if there exists k, s̄

and t̄ such that in_{k}s̄ = s, in_{k}t̄ = t and s̄ ⟶^{ℓ}_{k} t̄.

□

Every reindexing function f : A → B induces an obvious functor R(f) : N -LTS_{A} → N -LTS_{B} that reindexes the initial state according to f.

Definition 3.14 Define the reindexing functor R: N → CAT as follows: for every name-set A, R(A) = N -LTS_{A}, while for every function f : A → B, R(f) is the functor

R(f)(⟨S, ⟶, i⟩) = ⟨S, ⟶, fi⟩
R(f)(α) = α .

This allows us to employ the Grothendieck construction [29] to produce a category N -LTS cofibred over N. In more concrete terms we have the following:

Definition 3.15 Define N -LTS to be the following category:

Objects: N -LTSs Arrows: ⟨α, f⟩:⟨S, ⟶, ⟨A, i⟩⟩ →⟨S′, ⟶′, ⟨B, i′⟩⟩ is an arrow if f : A → B is a function and α:⟨S, ⟶, ⟨B, S(f)(i)⟩⟩ →⟨S′, ⟶′, ⟨B, i′⟩⟩ is a morphism in N -LTS_{B} (see Definition 3.12).

The composition is defined using the reindexing functor (that in this case have the only effect of providing the right type for composing arrows), i.e.

⟨β, g⟩⟨α, f⟩ =^{def} ⟨βR(f)(α), gf⟩ .

By construction the obvious projection functor N -LTS → N which sends a N -LTS to its initial name-set and any arrow ⟨α, f⟩ to f is a cofibration [29]. The category N is equivalent to the category of finite sets, which is known to have all finite colimits. By a well-known result of fibred category theory [29] we can then immediately deduce that N -LTS has finite colimits as well.

4 Denotational semantics

We describe now operations on N -LTS that we will use in giving a compositional semantics to the π-calculus. It will be straightforward to turn the operations below into functors, in fact into ω-continuous functors. As we have shown, for every name-set I, the category N -LTS_{I} is cocomplete and therefore has colimits of ω-chains. Thus a semantics of recursively defined processes, such as replicated ones, can be obtained using initial algebras in the usual way [58].

The most interesting operations are deadlock, which to obtain initiality has what may be a slightly surprising definition, and restriction and parallel composition. For restriction an equivalence relation, a semantic analogue of α-conversion, needs to be imposed on states – just as in the operational semantics a transition of (νx)P may be derived from a transition of (νx̂){x̂/_{x}}P for any x̂ ∉ (fn(P) \ x). For parallel, in the operational semantics states reachable by transitions from P | Q may involve restriction of P′ | Q′ for P′, Q′ reachable from P, Q. The construction over the model involves a similar quotienting as for restriction. The equivalence relation used in both cases is defined as follows.

Definition 4.1 If S: N → Set is a functor and A is a finite subset of N, take ↔_{A} to be the equivalence relation on (possibly subsets of) the set ∐_{B⊇A} S(B) defined by ⟨B_{1}, s_{1}⟩ ↔_{A} ⟨B_{2}, s_{2}⟩ if there exists a bijection b: B_{1} →_{bij} B_{2}, such that for every x ∈ A, b(x) = x and such that S(b)(s_{1}) = s_{2}.

Observe that elements of S(A) can only be related to themselves, i.e. their equivalence class is a singleton. For this reason, when no confusion arises, we will write s for [⟨A, s⟩]_{↔_{A}}. Notice also that, because of naturality, any arrow α: T → T′ in N -LTS_{I} preserves ↔_{A}, i.e.

⟨B_{1}, s_{1}⟩ ↔_{A} ⟨B_{2}, s_{2}⟩ implies ⟨B_{1}, α_{B_{1}}(s_{1})⟩ ↔_{A} ⟨B_{2}, α_{B_{1}}(s_{2})⟩ ,

for any pair of states of T. Thus for any set A, the function α_{↔_{A}} : ∐_{B⊇A} S(B) → ∐_{B⊇A} S′(B)

given by α_{↔_{A}}([⟨B, s⟩]_{↔_{A}}) =^{def} [⟨B, α_{B}(s)⟩]_{↔_{A}} is well-defined.

In the constructions below we shall often extend a transition system with new initial state over a chosen name set (say I), but now all of its reindexings must also be added. This can be expressed using the representable functor N (I, −) which we met in the proof of Theorem 3.13 and that provides the state space of the initial object of N -LTS_{I}. Notice that we write e.g. S + N (I, −) for the coproduct of functors which is given by the pointwise disjoint union of sets.

Notation: If U and V are two sets and U ⊎ V their disjoint union and no confusion arises, we will write l : U → U ⊎ V and r : V → U ⊎ V for the obvious left and right injections. If s = ⟨A, u⟩, write ls for ⟨A, lu⟩ and similarly for r. In what follows, unless otherwise stated we suppose that T = ⟨S: N → Set, ⟶, i⟩ and T_{k} = ⟨S_{k}: N → Set, ⟶_{k}, i_{k}⟩ (for k = 1, 2) are N -LTSs, with i = ⟨I, i⟩ and i_{k} = ⟨I, i_{k}⟩. Note that the initial name-sets I coincide.

Restriction If T = ⟨S: N → Set, ⟶, ⟨(I, x), i⟩⟩ define the restriction ν_{x∈(I,x)}(T) to be

⟨S′: N → Set, ⟶′, ⟨I, r[⟨(I, x), i⟩]_{↔_{I}} ⟩⟩ ,

where

• S′(A) = S(A) ⊎ (∐_{y∉A} S(A, y))/↔_{A}

• ⟶′ is defined by the following three rules:

\frac{A ⊢ s ⟶^{ℓ} t}{A ⊢ ls ⟶′^{ℓ} lt}

\frac{A, z ⊢ s ⟶^{ℓ} t}{A ⊢ r[s]_{↔_{A}} ⟶′^{ℓ} r[t]_{↔_{A∪fn(ℓ)}}} z ∉ fn(ℓ)

\frac{A, z ⊢ s ⟶^{\overline{x}z} t}{A ⊢ r[s]_{↔_{A}} ⟶′^{\overline{x}z} lt} x ≠ z

If α: T_{1} → T_{2} is an arrow in N -LTS_{I,x}, define ν_{x∈(I,x)}(α) to be α + α_{↔_{−}}, where for every A, α_{↔_{A}} is restricted in this case to operate only on equivalence classes [⟨B, s⟩] where B = A, y for some y ∉ A.

Output and τ prefix If x, y ∈ I, define \overline{x}y(T) to be

⟨S + N (I, −) : N → Set, ⟶′, ⟨I, r1_{I}⟩⟩ ,

where ⟶′ is defined by the following rules:

\frac{f : I → A}{⟨A, rf⟩ ⟶′^{\overline{f(x)}f(y)} l(fi)}

\frac{s ⟶^{ℓ} t}{ls ⟶′^{ℓ} lt}

Define τ(T) similarly by labelling the transition in the first rule τ rather than \overline{f(x)}f(y). If α: T_{1} → T_{2} is an arrow in N -LTS_{I}, define \overline{x}y(α) (and equally τ(α))

Input prefix If T = ⟨S: N → Set, ⟶, ⟨(I, y), i⟩⟩ is a transition system and y ≠ x ∈ I, define xy(T) to be

⟨S + N (I, −) : N → Set, ⟶′, ⟨I, r1_{I}⟩⟩ ,

where

\frac{f : I → A ι : A ↪ A ∪ \{z\}}{⟨A, rf⟩ ⟶′^{f(x)z} ⟨A ∪ \{z\}, lS([ιf, [z/y]])(i)⟩}

\frac{s ⟶^{ℓ} t}{ls ⟶′^{ℓ} lt}

Deadlock at I For every set of names I, define the deadlock N -LTS with free names in I as 0_{I} = ⟨N (I, −), ∅, ⟨I, 1_{I}⟩⟩. Recall, from the proof Theorem 3.13 that 0_{I} is the initial object of the category N -LTS_{I}.

Matching and Mismatching If x, y ∈ I, define [x = y](T) to be

⟨S + N (I, −) : N → Set, ⟶′, ⟨I, r1_{I}⟩⟩ ,

where ⟶′ is defined by the following rules:

\frac{f : I → A  fi ⟶^{ℓ} s  f(x) = f(y)}{⟨A, rf⟩ ⟶′^{ℓ} ls}

\frac{s ⟶^{ℓ} t}{ls ⟶′^{ℓ} lt}

Define [x ≠ y](T) similarly by requiring f(x) ≠ f(y) in the first rule.

Sum Define the sum,

T_{1} ⊕ T_{2} = ⟨(S_{1} + N (I, −) + S_{2}) : N → Set, ⟶_{0}, ⟨I, m1_{I}⟩⟩

where ⟶_{0} is defined by the following rules:

\frac{f : I → A ⟨A, S_{k}(f)(i_{1})⟩ ⟶^{ℓ}_{1} s}{⟨A, mf⟩ ⟶^{ℓ}_{0} ls} (and sym. for 2, r)

\frac{s ⟶^{ℓ}_{1} t}{ls ⟶^{ℓ}_{0} lt}  \frac{s ⟶^{ℓ}_{2} t}{rs ⟶^{ℓ}_{0} rt}

where we now use l, m, r rather than just l and r. If α: T_{1} → T′_{1} and β: T_{2} → T′_{2} are two arrows, define α ⊕ β = α + 1_{N (I,−)} + β.

Remark: If we assume the N -LTSs to be non-restarting, i.e. with no loops involving the initial state or any of its reindexings, we can simply use the categorical coproduct to model non-deterministic sum.

Parallel composition Notation: If S_{1} and S_{2} are two functors N → Set, and if ↔_{A} is the equivalence relation on ∐_{B⊇A}(S_{1} × S_{2})(B) = ∐_{B⊇A} S_{1}(B) × S_{2}(B) defined as in Definition 4.1, and if s_{1} = ⟨B, s_{1}⟩ and s_{2} = ⟨B, s_{2}⟩ write s_{1}|_{A}s_{2} for the equivalence class [(B, s_{1}, s_{2})]_{↔_{A}}. If T_{1} and T_{2} are two N -LTSs as before, define their parallel composition,

T_{1}|T_{2} = ⟨S_{0} : N → Set, ⟶_{0}, i_{1}|_{I}i_{2}⟩

where

• S_{0}(A) = (∐_{B⊇A}(S_{1} × S_{2})(B))/↔_{A}, while S_{0}(f : A → A′)([(B, s_{1}, s_{2})]_{↔_{A}}) = [(B′, t_{1}, t_{2})]_{↔_{A′}}, where t_{k} = S(f + g)(s_{k}), for k = 1, 2 and g: B \ A →_{bij} B′ \ A′ is a bijection

• ⟶_{0} is defined by the following three rules (and symmetric versions of the first two):

\frac{A, A′ ⊢ s_{1} ⟶^{ℓ}_{1} t_{1} ι: A, A′ ↪ A ∪ fn(ℓ), A′}{A ⊢ s_{1}|_{A}s_{2} ⟶^{ℓ}_{0} t_{1}|_{A∪fn(ℓ)}ιs_{2}}

\frac{A, A′ ⊢ s_{1} ⟶^{\overline{x}y}_{1} t_{1} A, A′ ⊢ s_{2} ⟶^{xy}_{2} t_{2}}{A ⊢ s_{1}|_{A}s_{2} ⟶^{τ}_{0} t_{1}|_{A}t_{2}}

\frac{A, y ⊢ s_{1}|_{A,y}s_{2} ⟶^{\overline{x}y}_{0} t_{1}|_{A,y}t_{2}}{A ⊢ s_{1}|_{A}s_{2} ⟶^{\overline{x}y}_{0} t_{1}|_{A,y}t_{2}}

It is routine to verify that the functor S_{0} is well defined, i.e. that the definition of S_{0}(f) is independent of the choice of representatives and of the choice of the functions g.

If α: T_{1} → T′_{1} and β: T_{2} → T′_{2} are two arrows, define (α|β)_{A}([⟨B, s_{1}, s_{2}⟩]_{↔_{A}}) = [⟨B, α_{B}(s_{1}), β_{B}(s_{2})⟩]_{↔_{A}}. Compositional semantics to π-terms is given using the operations defined above in the usual

way. For a process term P, with free names in I, we write [[P]]_{I} for the corresponding N -LTS. So in particular we have

• [[0]]_{I} = 0_{I}

• [[P | Q]]_{I} = [[P]]_{I} | [[Q]]_{I}

• [[P + Q]]_{I} = [[P]]_{I} ⊕ [[Q]]_{I}

• [[τ.P]]_{I} = τ([[P]]_{I})

• [[\overline{x}y.P]]_{I} = \overline{x}y([[P]]_{I})

• [[xy.P]]_{I} = xy([[P]]_{I})

• [[νx.P]]_{I} = (νx)([[P]]_{I,x})

• [[[x = y]P]]_{I} = [x = y]([[P]]_{I})

• [[[x ≠ y]P]]_{I} = [x ≠ y]([[P]]_{I})

Bisimilarity is defined in the usual way, but thanks to the indexing, we can also define directly in the model the closure under name substitutions, which for the π-calculus characterises the largest congruence included in bisimilarity.

Definition 4.2 Define two N -LTSs T_{1} and T_{2} to be

• strongly bisimilar if the LTS ⟨S_{1}, ⟶_{1}, i_{1}⟩ and ⟨S_{2}, ⟶_{2}, i_{2}⟩ are bisimilar in the usual sense of Milner [39].

• strongly equivalent if, for every f : I → A, the N -LTSs ⟨S_{1}, ⟶_{1}, fi_{1}⟩ and ⟨S_{2}, ⟶_{2}, fi_{2}⟩ are strongly bisimilar.

Weak bisimilarity and equivalence are defined similarly.

By taking full account of the indexing structure of the state space we naturally characterise ‘open bisimilarity’ [47].

Definition 4.3 If S_{1}, S_{2} : N → Set are functors, define a relation between S_{1} and S_{2} to be a subobject R ↪ S_{1} × S_{2} of their product.

In other words (cf. [37]) a relation R is an indexed set of pairs (R(A))_{A∈|N |} such that, for every A,

R(A) ⊆ S_{1}(A) × S_{2}(A)

and for every f : A → B,

⟨s_{1}, s_{2}⟩ ∈ R(A) implies ⟨S_{1}(f)(s_{1}), S_{2}(f)(s_{2})⟩ ∈ R(B) .

Any relation R ↪ S_{1} × S_{2}, induces a relation

R ⊆ S_{1} × S_{2} ,

defined as R =^{def} {⟨s, t⟩ | ∃A, s, t. ⟨s, t⟩ ∈ R(A) ∧ s = ⟨A, s⟩ ∧ t = ⟨A, t⟩}.

Definition 4.4 If T_{1} and T_{2} are two N -LTSs with indexed sets of states S_{1} and S_{2}, respectively, define a relation R ↪ S_{1} × S_{2} to be an open bisimulation if the relation

R ⊆ S_{1} × S_{2}

is a strong bisimulation for the transition systems ⟨S_{1}, ⟶_{1}, i_{1}⟩ and ⟨S_{2}, ⟶_{2}, i_{2}⟩.

Clearly open bisimilarity is the finest among all the equivalence relations defined above.

We conclude this section with the result which relates bisimulation in the model with bisimulation in the operational semantics.

Theorem 4.5 Let P and Q be two π-terms with free names in I. Then P ˙∼_{I}Q if and only if [[P]]_{I} is bisimilar to [[Q]]_{I}.

To prove this theorem we first need the following lemma.

Lemma 4.6 For every π-term P, with free names in I, ([P])_{I} is open bisimilar to [[P]]_{I}.

Proof: The proof goes by structural induction on P. We show how to inductively define open bisimulations. It will be generally trivial to verify that the induced relations on the states of the transition systems are bisimulations. Thus we omit the verification in all but a few less trivially clear cases.

• P = 0 Define B(A) = {⟨0, f⟩ | f : I → A}. For any g: A → B, B(g)⟨0, f⟩ = ⟨0, gf⟩. Since there are no transitions to match, this induces trivially a bisimulation.

• P = \overline{x}y.Q Suppose B ⊆ ([Q])_{I} × [[Q]]_{I} is an open bisimulation. Define

(\overline{x}y.B)(A) = \{⟨R, ls⟩ | ⟨R, s⟩ ∈ B(A)\} + \{⟨\overline{fx}fy.fQ), rf⟩ | f : I → A\}

If g: A → B, (\overline{x}y.B)(g)⟨R, ls⟩ = ⟨gR, l[[Q]]_{I}(g)(s)⟩, while (\overline{x}y.B)(g)⟨\overline{fx}fy.fQ), rf⟩ = ⟨\overline{(gf)x}(gf)y.(gf)Q), r(gf)⟩.

• P = τ.Q and P = xy.Q These cases are dealt with similarly to the output case.

• P = [x = y]Q and P = [x ≠ y]Q Suppose B ⊆ ([Q])_{I} ×[[Q]]_{I} is an open bisimulation. Define

([x = y]B)(A) = {⟨R, ls⟩ | ⟨R, s⟩ ∈ B(A)} + {⟨R, rf⟩ | f : I → A&R = ([fx = fy]fQ)}

The case of mismatching has R = ([fx ≠ fy]fQ)} in the definition of the second set above. The action on renaming functions is defined as in the case of the prefixes.

• P = (νx).Q Suppose B ⊆ ([Q])_{I,x} × [[Q]]_{I,x} is an open bisimulation. Define

((νx).B)(A) = {⟨R, ls⟩ | ⟨R, s⟩ ∈ B(A)} + ⋃_{y∈N \A}{⟨(νy).R, r[s]_{↔_{A}}⟩ | ⟨R, s⟩ ∈ B(A, y)}

• P = P_{1} | P_{2} Suppose that B ⊆ ([P_{1}])_{I} ×[[P_{1}]]_{I} and C ⊆ ([P_{2}])_{I} ×[[P_{2}]]_{I} are open bisimulations. Define

(B | C)(A) = {⟨νx⃗(Q_{1} | Q_{2}), s_{1} |_{A} s_{2}⟩ | ⟨Q_{1}, s_{1}⟩ ∈ B(A, x⃗)&⟨Q_{2}, s_{2}⟩ ∈ C(A, x⃗)}

with the obvious action on renaming functions. Let us see in some detail why the relation on states induced by B | C is a bisimulation. Suppose for instance that

⟨νx⃗(Q_{1} | Q_{2}), s_{1} |_{A} s_{2}⟩ ∈ (B | C)(A)

with, without loss of generality, ⟨Q_{1}, s_{1}⟩ ∈ B(A, x⃗) and ⟨Q_{2}, s_{2}⟩ ∈ C(A, x⃗), and that A ⊢ νx⃗(Q_{1} | Q_{2}) ⟶^{ℓ} Q. Then one of the following three cases (or one of their symmetric versions) must hold:

1. There exist y⃗, \overline{Q}_{1} and \overline{Q}_{2} such that

– νx⃗(Q_{1} | Q_{2}) = νy⃗(\overline{Q}_{1} | \overline{Q}_{2})

– fn(ℓ) ∉ y⃗

– A, y⃗ ⊢ \overline{Q}_{1} ⟶^{ℓ} Q′_{1}

– Q = νy⃗(Q′_{1} | \overline{Q}_{2}).

Then there exists a bijection b: A, x⃗ →_{bij} A, y⃗ such that b(a) = a for every a ∈ A, bQ_{1} = \overline{Q}_{1} and bQ_{2} = \overline{Q}_{2}. Thus ⟨\overline{Q}_{1}, S_{1}(b)(s_{1})⟩ ∈ B(A, y⃗) and ⟨\overline{Q}_{2}, S_{2}(b)(s_{2})⟩ ∈ C(A, y⃗). So, by inductive hypothesis A, y⃗ ⊢ bs_{1} ⟶^{ℓ} t_{1} with ⟨Q′_{1}, t_{1}⟩ ∈ B(A ∪ fn(ℓ), y⃗). Hence

A ⊢ s_{1} |_{A} s_{2} = bs_{1} |_{A} bs_{2} ⟶^{ℓ} t_{1} |_{A∪fn(ℓ)} ιbs_{2} ,

with ⟨Q, t_{1} |_{A∪fn(ℓ)} ιbs_{2}⟩ ∈ (B | C)(A ∪ fn(ℓ)).

2. There exist y⃗, \overline{Q}_{1} and \overline{Q}_{2} such that

– νx⃗(Q_{1} | Q_{2}) = νy⃗(\overline{Q}_{1} | \overline{Q}_{2})

– ℓ = τ

– A, y⃗ ⊢ \overline{Q}_{1} ⟶^{\overline{w}z} Q′_{1}, A, y⃗ ⊢ \overline{Q}_{2} ⟶^{wz} Q′_{2}

– Q = νy⃗(Q′_{1} | Q′_{2}), if z ∈ A, y⃗

– Q = νy⃗νz(Q′_{1} | Q′_{2}), if z ∉ A, y⃗

We then have a bijection b with the same properties as above. Therefore it is the case that there exists states t_{1} and t_{2} such that A, y⃗ ⊢ bs_{1} ⟶^{\overline{w}z} t_{1} and A, y⃗ ⊢ bs_{2} ⟶^{wz} t_{2}, with ⟨Q′_{1}, t_{1}⟩ ∈ B({z} ∪ (A, y⃗)) and ⟨Q′_{2}, t_{2}⟩ ∈ C({z} ∪ (A, y⃗)). Thus

A ⊢ s_{1} |_{A} s_{2} = bs_{1} |_{A} bs_{2} ⟶^{τ} t_{1} |_{A} t_{2} ,

with ⟨Q, t_{1} |_{A} t_{2}⟩ ∈ (B | C)(A).

3. There exist y⃗, \overline{Q}_{1} and \overline{Q}_{2} such that

– νx⃗(Q_{1} | Q_{2}) = νy⃗(\overline{Q}_{1} | \overline{Q}_{2})

– ℓ = \overline{w}z, with z ∈ y⃗ and w ∈ A

– A, y⃗ ⊢ \overline{Q}_{1} ⟶^{\overline{w}z} Q′_{1}

– Q = νy⃗ \ \{z\}(Q′_{1} | \overline{Q}_{2})

Again we have a bijection b with the same properties as above and thus there exists t_{1} such that A, y⃗ ⊢ bs_{1} ⟶^{\overline{w}z} t_{1} with ⟨Q′_{1}, t_{1}⟩ ∈ B(A, y⃗ \ \{z\}). Therefore we also have that

A ⊢ s_{1} |_{A} s_{2} = bs_{1} |_{A} bs_{2} ⟶^{\overline{w}z} t_{1} |_{A,z} ιbs_{2} .

The matching of transitions of [[P_{1} | P_{2}]]_{I} by transitions of ([P_{1} | P_{2}])_{I} is proven with a similar analysis (cf. the rules that define the parallel composition of two N -LTSs).

□

Using the lemma above it is now easy to prove the Theorem 4.5:

Proof:[of Theorem 4.5] Suppose P and Q are two π-terms with free names in I. Then by definition, P ˙∼_{I}Q if and only if ([P])_{I} is bisimilar to ([Q])_{I}. By Lemma 4.6, then [[P]]_{I} is bisimilar to [[Q]]_{I}. Conversely, if [[P]]_{I} is bisimilar to [[Q]]_{I}, then, by Lemma 4.6, ([P])_{I} is bisimilar to ([Q])_{I} and thus P ˙∼_{I}Q.

□

It is worth noticing that since open bisimilarity is the finest equivalence that we have defined, Theorem 4.5 holds also if we change ˙∼_{I} with any of the other strong or weak standard (early) equivalences.

Replication From the point of view of a denotational semantics, a concrete description of a replication operator can be bypassed using initial algebras, i.e. fixed points, to model recursively defined and thus also replicated processes. The crucial point is establishing, by tedious verification, the following:

Theorem 4.7 If T is a N -LTS with initial name set I, x a name not in I, y and z names in I, then the functors:

• (T ⊕ −) : N -LTS_{I} → N -LTS_{I},

• (T | −) : N -LTS_{I} → N -LTS_{I},

• ν_{x∈(I,x)}(−) : N -LTS_{I,x} → N -LTS_{I}, • \overline{y}z(−) : N -LTS_{I} → N -LTS_{I},

• τ(−) : N -LTS_{I} → N -LTS_{I},

• yx(−) : N -LTS_{I,x} → N -LTS_{I},

• [y = z](−) : N -LTS_{I} → N -LTS_{I} and

• [y ≠ z](−) : N -LTS_{I} → N -LTS_{I}

preserve colimits of ω-chains.

The semantics can then be given as follows.

• [[!P]]_{I} =![[P]]_{I}, where for every N -LTS T with initial name set I, !T is defined to be μ(T | −). This is the object part of an initial algebra

T | μ(T | −) ⟶^{≃} μ(T | −)

for the endofunctor (T | −) : N -LTS_{I} → N -LTS_{I}. Notice that such an initial algebra exists since N -LTS_{I} has colimits of ω-chains and every operation involved in the semantics preserves this kind of colimits (Theorem 4.7). Moreover it can be calculated in the usual way as the colimit of the “standard” chain

0_{I} → T | 0_{I} → T | (T | 0_{I}) → T | (T | (T | 0_{I})) → · · · .

To generalise Theorem 4.5 to a calculus with replication, exhibiting a correspondence between this construction and the standard operational semantics for replication

Rep \frac{A ⊢ P |!P ⟶^{ℓ} P′}{A ⊢ !P ⟶^{ℓ} P′}

would require a lemma showing that if ([P])_{I} and [[P]]_{I} are bisimilar then so are their n-way parallel compositions, and then a verification of a bisimulation relation. We do not develop the details here.

5 N -LATS

In this section we define a class of causal models by smoothly lifting the notion of labelled asynchronous^{1} transition system [3, 55, 58] (LATS for short) to our indexed setting. LATS are a simple extension of standard LTS in which transitions have both standard labels and events, upon which an independence relation is defined. Roughly speaking, concurrency is modelled by requiring that transitions tagged with independent events might occur in any order. As discussed in the introduction, in π-calculi dependencies between transitions may arise from their name usage:

Definition 5.1 If A is a set of names and ℓ_{1} and ℓ_{2} are two labels, we say that ℓ_{2} is A-dependent on ℓ_{1} if one of the following two cases applies:

1. val(ℓ_{1}) = chan(ℓ_{2}) ⊈ A

1There is an unfortunate clash of terminology here: this usage of ‘asynchronous’ is unrelated to the usage describing process calculi without output prefixing.

2. val(ℓ_{1}) = val(ℓ_{2}) ⊈ A, one of ℓ_{1}, ℓ_{2} is an input action and the other is an output action.

Definition 5.2 Define an Indexed LATS (N -LATS) to be a structure

T = ⟨S: N → Set, ⟶, i, E, I⟩

where i = ⟨I, i⟩ ∈ S,

⟶ ⊆ S × (Lab × E) × S ,

E is a set of events, I ⊆ E × E is an independence relation between events and the following conditions hold.

1. For every event e ∈ E, the structure ⟨S: N → Set, ⟶_{e}, i⟩ is a N -LTS, where ⟶_{e} is the

set { ⟨s, ℓ, t⟩ | ⟨s, ℓ, e, t⟩ ∈⟶ }.

2. I is irreflexive and symmetric

3. If A ⊢ s⟶_{e_{1}}^{ℓ_{1}}t, and t⟶_{e_{2}}^{ℓ_{2}}u, and e_{1}Ie_{2}, and moreover ℓ_{2} is not A-dependent on ℓ_{1}, then there

exists a state t′ such that s⟶_{e_{2}}^{ℓ_{2}}t′ and t′⟶_{e_{1}}^{ℓ_{1}}u.

Often LATS are defined using more axioms (see [3, 58]). Here we have decided to keep the axiomatisation as light as possible, as none of the extra axioms is directly relevant for the definability of the semantic constructions that we consider. Moreover we allow the same event to carry different labels. This is particularly useful in coping with the proliferation of transitions induced by reindexing and by the input actions. It is not difficult to devise simple variations of our definition which adhere more closely to the traditional case.

Building on the independence relation, transitions occurring in a run of a process can be given a causal partial order describing which transitions are necessary conditions for the occurrence of others. Roughly speaking one transition causes the following one if the corresponding events are not independent of each other. As discussed in the introduction, one can choose whether or not to consider name dependencies – for N -LATS there are two natural ways of defining partial orders out of runs, one taking account only of the independence relation and another which also takes name dependencies into account.

Notation: For every natural number n, write [n] for the set {k | 1 ≤ k ≤ n}. Observe that, in particular, [0] = ∅.

Definition 5.3 For every run ρ

A_{0} ⊢ s_{0}⟶_{e_{1}}^{ℓ_{1}}s_{1}⟶_{e_{2}}^{ℓ_{2}}s_{2} ⋯ ⟶_{e_{n}}^{ℓ_{n}}s_{n}

of an N -LATS we define two labelled partial orders:

1. Define po(ρ)_{I} = ⟨[n], ⊴_{I}^{ρ}, l^{ρ}⟩, where

(a) n is the length of the run ρ.

(b) ⊴_{I}^{ρ} is the transitive closure of ⪯_{I}^{ρ} which is defined as i ⪯_{I}^{ρ} j if i ≤ j and ¬(e_{i}Ie_{j})

(c) l^{ρ}(k) = ℓ_{k}, for every k ∈ [n]

2. Define po(ρ)_{ID} = ⟨[n], ⊴_{ID}^{ρ}, l^{ρ}⟩, where n and l^{ρ} are obtained as above, while ⊴_{ID}^{ρ} is the transitive closure of ⪯_{ID}^{ρ} which is defined as i ⪯_{ID}^{ρ} j if i ≤ j and either not e_{i}Ie_{j} or ℓ_{j} is A_{i}-dependent on ℓ_{i}, where s_{i} = (A_{i}, s_{i}).

History preserving bisimulation [46, 23, 17] is a bisimulation between runs of processes which accounts for causality by requiring related runs to originate isomorphic partial orders of transitions:

Definition 5.4 If T is an N -LATS, define Run(T) to be the set of runs of T. If ρ is a run

I ⊢ i⟶_{e_{1}}^{ℓ_{1}}s_{1}⟶_{e_{2}}^{ℓ_{2}}s_{2}⟶ ⋯ ⟶_{e_{n}}^{ℓ_{n}}s_{n} of T then define

1. end(ρ) =^{def} s_{n}

2. names(ρ) =^{def} A_{n}, where s_{n} = ⟨A_{n}, s⟩.

Notation: If ρ is a run of an N -LATS and names(ρ) ⊢ end(ρ)⟶_{e}^{ℓ}s is a transition, we write

ρ⟶_{e}^{ℓ}s for the run which extends ρ with that transition. If ρ and ρ′ are runs, we write ρ⟶_{e}^{ℓ}ρ′ if

ρ′ extends ρ with the transition names(ρ) ⊢ end(ρ)⟶_{e}^{ℓ}end(ρ′).

Definition 5.5 Let T_{1} and T_{2} be two N -LATSs with initial name-set I. A relation B ⊆ Run(T_{1}) × Run(T_{2}) is an history preserving bisimulation (hpb) if it satisfies the following conditions

1. (I ⊢ i_{1}, I ⊢ i_{2}) ∈ B

2. (ρ_{1}, ρ_{2}) ∈ B implies

(a) po(ρ_{1})_{I} = po(ρ_{2})_{I}

(b) if ρ_{1}⟶_{1}_{e_{1}}^{ℓ}ρ′_{1} then there exists a run ρ′_{2} of T_{2} and an event e_{2} ∈ E_{2} such that ρ_{2}⟶_{2}_{e_{2}}^{ℓ}ρ′_{2}

and (ρ′_{1}, ρ′_{2}) ∈ B

(c) the symmetric condition to the above.

The relation B is a name-dependency aware hpb (ndahpb) if the condition 2(a) is changed into po(ρ_{1})_{ID} = po(ρ_{2})_{ID}.

The constructions of Section 4 can be easily adapted to become constructions on N -LATS. We shall now briefly indicate how they need to be extended to take account of the presence of events and of the independence relation. In all cases where a label is carried from the premise to the conclusion, the event is also carried (suitably injected).

Restriction The set of events and the independence relation does not change.

Prefixes A new event, not in the independence relation with any other is added and it decorates all of the new transitions.

Deadlock The set of events is empty and so is the independence relation.

Matching and Mismatching Events and the independency relation are left untouched.

Sum The set of events is taken to be the disjoint union of the originals but no new independence pairs are added.

Parallel composition If E_{1} and E_{2} are the two sets of events we define E_{0} to be the disjoint union E_{1} ⊎ (E_{1} × E_{2}) ⊎ E_{2}. Writing this as (E_{1} × {⋆}) ∪ (E_{1} × E_{2}) ∪ ({⋆} × E_{2}) for ⋆ ∉ E_{1} ∪ E_{2}, the independence relation is defined by ⟨e_{1}, e_{2}⟩I_{0}⟨e′_{1}e′_{2}⟩ if both e_{1}Î_{1}e′_{1} and e_{2}Î_{2}e′_{2}, where Î_{k} is the union of I_{k} and ⟨⋆, ⋆⟩. The new τ-transitions are decorated by the pairs of enabling events.

Process terms can then be given a denotational semantics and be related by (nda) history preserving bisimilarity. In the remainder of this section we will mostly concentrate on the relationship between our semantics and the causal bisimulation of [6]. In particular we present correspondence results relating our hbp semantics to causal bisimulation, and further discuss name-dependency.

In the paper [6], no notion of strong causal bisimulation is defined – the authors directly defined causal bisimulation in the weak form, abstracting away from τ actions. To match with our definitions we therefore need either to define weak history-preserving bisimulation or to modify their setting in order to make τ actions visible. We will in fact do both, ending up with two correspondence results, one for strong and one for weak bisimulation. We now briefly recall the definition of causal bisimulation of loc. cit. which also requires defining a variant of the π-calculus with explicit causality information. We refer to loc. cit. for a detailed discussions of the relevance of their approach. Also, we show here what modifications are needed in order to define, in their setting, strong causal bisimulation.

As in [6] we take a set K of causes, distinct from the names N, and extend the process syntax with a construct K :: P where K ⊆_{fin} K is the set of causes that have affected P. For simplicity we also omit matching and mismatching (as in [6]), omit replication, and adopt the unstratified grammar below (in contrast to [6]).

P ::= 0 | P | P | τ.P | \overline{x}v.P | xp.P | P + P | (νx)P | K :: P

Notation: We write K(P) for the set of causes occurring anywhere in P, and [k ⇝ K]P for P with each cause-set K′ containing k replaced by K ∪ (K′ \ {k}). In the appendix we let P, Q range over terms of the grammar that do not contain subterms K :: R and C, D range over arbitrary terms.

The causal operational semantics is given in Figure 3 which defines a transition relation

A ⊢ P ⟶_{K;k}^{ℓ}Q

Here K is the set of prior causes of this transition and k is a new cause. The definition differs slightly from that of [6] – it is explicitly indexed and it maintains causes for τ-transitions.

Strong causal bisimulation can now be defined in the usual way, by requiring transitions to agree not only on the labels but on the causes too. In detail, take strong causal bisimulation ˙∼^{c} to be the largest family of relations indexed by finite sets of names such that each ˙∼^{c}_{A} is a symmetric relation over { P | fn(P) ⊆ A } and for all P ˙∼^{c}_{A} Q,

• if A ⊢ P ⟶_{K;k}^{ℓ}P′ then ∃Q′ . A ⊢ Q⟶_{K;k}^{ℓ}Q′ ∧ P′ ˙∼^{c}_{A∪fn(ℓ)} Q′.

This is the obvious adaptation of the definition in [6] to the explicitly-indexed strong case. We can now state our first non-interleaving correspondence result:

Theorem 5.6 Let P and Q be two terms of the π-calculus with free names in I and let [[P]]_{I}^{c} and [[Q]]_{I}^{c} be their interpretations as N -LATS’s. Then [[P]]_{I}^{c} is history preserving bisimilar to [[Q]]_{I}^{c} if and only if P is strongly causal bisimilar to Q.

Proof:[Hint] The proof requires some constructions and lemmas. First of all one relates the (causal) operational semantics of π-terms with transitions in asynchronous transition systems, in terms of so-called run-bisimulations. These are relations between runs of processes and runs of N -LATS’s satisfying the usual coinductive properties as well as a condition relating corresponding partial order of causes and of events. The crucial step is then that of establishing

Out \overline{A ⊢ \overline{x}v.P ⟶_{∅;k}^{\overline{x}v}k :: P}  In \overline{A ⊢ xp.P ⟶_{∅;k}^{xv}k :: \{^{v}/_{p}\}P}

Tau \overline{A ⊢ τ.P ⟶_{∅;k}^{τ}k :: P}  Cau \frac{A ⊢ P ⟶_{K;k}^{ℓ}P′}{A ⊢ K′ :: P ⟶_{K∪K′;k}^{ℓ}K′ :: P′}

Res \frac{A, x ⊢ P ⟶_{K;k}^{ℓ}P′ x ∉ fn(ℓ)}{A ⊢ (νx)P ⟶_{K;k}^{ℓ}(νx)P′} Open \frac{A, x ⊢ P ⟶_{K;k}^{\overline{y}x}P′ y ≠ x}{A ⊢ (νx)P ⟶_{K;k}^{\overline{y}x}P′}

Sum \frac{A ⊢ P ⟶_{K;k}^{ℓ}P′}{A ⊢ P + Q⟶_{K;k}^{ℓ}P′}  Par \frac{A ⊢ P ⟶_{K;k}^{ℓ}P′}{A ⊢ P | Q⟶_{K;k}^{ℓ}P′ | Q}

Com \frac{A ⊢ P_{1}⟶_{K_{1};k}^{\overline{x}y}P′_{1}  A ⊢ P_{2}⟶_{K_{2};k}^{xy}P′_{2}}{A ⊢ P_{1} | P_{2} ⟶_{K_{1}∪K_{2}:k}^{τ}(ν\{y\} − A)([k ⇝ (K_{2} ∪ k)]P′_{1} | [k ⇝ (K_{1} ∪ k)]P′_{2})}

In all rules with conclusion of the form A ⊢ P ⟶_{K;k}^{ℓ}Q there are implicit sideconditions fn(P) ⊆

A and k ∉ K(P). Symmetric versions of Par, Com, and Sum are elided.

Figure 3: π causal operational semantics

that every π-term P, with free names in I, is run-bisimilar to its corresponding N -LATS, [[P]]_{I}^{c}. This latter result paves the way for the proof of the Theorem. Details can be found in Appendix A.

□

A weak version of history preserving bisimulation can be given in the spirit of [57].

Definition 5.7 Let ρ be a run in an asynchronous transition system, let n be the length of ρ, and let n^{τ} be the number of transitions in ρ which are not labelled τ. For every i ≤ n^{τ}, define n_{i} ≤ n inductively as follows: n_{1} is the smallest number h such that the h-th transition of ρ has label ℓ_{h} ≠ τ; n_{j+1} is the smallest number h such that the h-th transition of ρ has label ℓ_{h} ≠ τ and that moreover is strictly bigger than n_{j}.

Starting with a run ρ of an N -LATS, by means of the above definition, we can define partial orders of observable events in runs as follows:

Definition 5.8 Let ρ be a run of an N -LATS and let po(ρ)_{I} and po(ρ)_{ID} be the corresponding partial orders as in Definition 5.3. Define po(ρ)_{wI} and po(ρ)_{wID} to be the partial orders ⟨[n^{τ}], ⊴_{wI}, l_{w}^{ρ}⟩ and ⟨[n^{τ}], ⊴_{wID}, l_{w}^{ρ}⟩, respectively, where l_{w}^{ρ}(i) = l^{ρ}(n_{i}), i ⊴_{wI} j if n_{i} ⊴_{I} n_{j} and i ⊴_{wID} j if n_{i} ⊴_{ID} n_{j}.

Weak history preserving bisimulations are now defined as relations between runs as in Definition 5.5 but where, as usual, “strong” transitions ρ_{1}⟶_{1}_{e_{1}}^{ℓ}ρ′_{1} are simulated by “weak” ones

ρ_{2} ⟹_{2}_{e_{2}}^{ℓ̂} ρ′_{2} (and symmetrically) and with condition 2(a) replaced by

po(ρ_{1})_{wI} = po(ρ_{2})_{wI}

or by po(ρ_{1})_{wID} = po(ρ_{2})_{wID}, for the name-dependency aware case. One can use the main lemma developed for the proof of Theorem 5.6, to prove the following result:

Theorem 5.9 Let P and Q be two terms of the π-calculus with free names in I and let [[P]]_{I}^{c} and [[Q]]_{I}^{c} be their interpretations as N -LATSs. Then [[P]]_{I}^{c} is weak history preserving bisimilar to [[Q]]_{I}^{c} if and only if P is causal bisimilar to Q in the sense of [6].

Proof:[Sketch] Weak causal bisimulations between π-terms, generate relations between runs of the corresponding processes. These can be composed with the run-bisimulations of Lemma A.9 to give weak history preserving bisimulations. Vice versa given a weak history preserving bisimulation between the denotations of two processes, one obtains a relation between runs of the two processes by composing with the run-bisimulations of Lemma A.9. The relation on causal π agents, which relates end points of related runs is a weak causal bisimulation.

□

In [6] it is argued that, because of the dependencies due to the binding of names, processes like (νy)(\overline{x}y.\overline{y}z) and (νy)(\overline{x}y|\overline{y}z) should be indistinguishable by an external observer. Nonetheless causal bisimulation distinguishes them, as it only tracks the dependencies due to the structure of processes – in the example, one output is prefixing the other in the first process but not in the second. The paper leaves open the possibility of a further refinement of the treatment of causes in the operational semantics to identify the above two processes.

Their remark has been tackled in [30], where a domain model of π-terms based on Kahn networks is presented. There the induced equivalence equates the two processes, but it seems to us that the equivalence is anyway a traced-based rather than a bisimulation based one. In [18], the authors use the combination of different partial orders to achieve the effect of equating the two processes above. In this paper we instead refined the way the causal order of events in a run is determined. This has led to the notion of name-dependency aware history preserving bisimulation defined above. It is easy to verify that name-dependency aware history preserving bisimilarity is a coarser relation than history preserving bisimilarity and that the former equates the two example processes:

Proposition 5.10 If two asynchronous transition systems are history preserving bisimilar than they are name-dependency aware history preserving bisimilar.

Proposition 5.11 The denotations of the process terms (νy)(\overline{x}y.\overline{y}z) and (νy)(\overline{x}y|\overline{y}z) are namedependency aware history preserving bisimilar but not history preserving bisimilar.

6 Relating N -LTSs and N -LATSs

We continue now the abstract study, initiated in the second part of Section 3, of the structures defined in this paper. We begin by defining, for name-sets I, categories N -LATS_{I} of N -LATSs. We then establish some categorical properties of N -LATS_{I} and, analogously to the case of N -LTSs, define a category N -LATS which cofibres over N – the fibres being the categories N -LATS_{I}. Finally we conclude by showing the existence of adjunctions relating N -LTS_{I} and (a full subcategory of) N -LATS_{I}, and how these can be glued together to provide a (fibred) adjunction between N -LTS and (a full subcategory of) N -LATS.

Definition 6.1 Define a morphism T_{1} → T_{2} between N -LATSs with initial name-set I to consist of a pair ⟨α, η⟩ where

• α : S_{1} ⟹ S_{2} is a natural transformation

• η: E_{1} → E_{2} is a function

such that

1. αi_{1} = i_{2}

2. s⟶_{e}^{ℓ}s′ implies αs⟶_{ηe}^{ℓ}αs′

3. eI_{1}e′ implies ηeI_{2}ηe′.

Define N -LATS_{I} to be the category of N -LATSs with initial name-set I and these morphisms.

Because of restrictions imposed by the axioms which governs the independence relation between events of a N -LATS, the category N -LATS_{I} does not enjoy all the completeness and cocompleteness properties of N -LTS_{I}, still it has enough colimits to allow for a denotational semantics of recursively defined processes.

Theorem 6.2 For every name set I, the category N -LATS_{I} has small coproducts and colimits of filtered diagrams.^{2} It also has limits of every non-empty diagram.

Proof: The constructions are extensions of those seen in the proof of Theorem 3.13 for N -LTSs. We outline some.

• The initial object is ⟨N (I, −), ∅, ⟨I, 1_{I}⟩, ∅, ∅⟩.

• The coproduct of a family (T_{k} = ⟨S_{k}, ⟶_{k}, ⟨I, i_{k}⟩, E_{k}, I_{k}⟩)_{k∈K} of N -LATSs is given by ⟨S, ⟶, ⟨I, i⟩, E, I⟩, where S and the initial state ⟨I, i⟩ are obtained as in the analogous construction in the proof of Theorem 3.13; E = ∐_{k∈K} E_{k}, while I = ∐_{k∈K} I_{k}.

If (in_{k}^{S} : S_{k} → S)_{k∈K} and (in_{k}^{E} : E_{k} → E)_{k∈K} are the cones of injections, then define s⟶_{e}^{ℓ}t

if there exist k ∈ K, s̄, t̄ ∈ S_{k} and ē ∈ E_{k}, such that s̄⟶_{ē}^{ℓ}_{k}t̄ and such that in_{k}^{S}s̄ = s,

in_{k}^{S}t̄ = t and ∈_{k}^{E} (ē) = e.

• If 𝔻 is a filtered category and Δ : 𝔻 → N -LATS_{I} is a functor, then a colimiting cone

(⟨α_{D}, η_{D}⟩: Δ(D) → T)_{D∈|𝔻|}

can be built as follows:

– (α_{D}: S_{D} → S)_{D∈|𝔻|} is the colimit of 𝔻 →^{Δ} N -LATS_{I} →^{p^{S}} Set^{N}, where p^{S} is the obvious projection functor.

– Similarly (η_{D}: E_{D} → E)_{D∈|𝔻|} is the colimit in Set of 𝔻 →^{Δ} N -LATS_{I} →^{p^{E}} Set.

– eIe′ if there exist d ∈ |𝔻| and ē, ē′ ∈ E_{D} such that ēI_{D}ē′ and η_{D}(ē) = e and η_{D}(ē′) = e′.

– s⟶_{e}^{ℓ}t if there exist d ∈ |𝔻|, ē ∈ E_{D} and s̄, t̄ ∈ S_{D} such that s̄⟶_{e}^{ℓ}_{D}t̄ and α_{D}(s̄) = s

and α_{D}(t̄) = t.

– ⟨I, i⟩ = ⟨I, (α_{D})_{I}(i_{D})⟩, for some D (by filteredness, all the initial states are mapped to the same state of S(I))

2A filtered diagram is a diagram obtained from a filtered category (see [36] for the definition of this notion).

It is straightforward to verify that T is a N -LATS and that the cone is colimiting.

Turning to limits it suffices to show that N -LATS_{I} has equalisers and small (but non-empty) products. Again these are defined by simple extensions of the analogous constructions in N -LTS_{I}. We leave the reader to work out such details.

□

In particular we can see that N -LATS_{I} does not have terminal object (the limit of the empty diagram) and in general it does not have coequalisers – to exist, these would require the possibility of “autoconcurrent” events. It is worth remarking that the situation here is quite similar to that of standard LTSs and Asynchronous Transition Systems or Event Structures [58]. Again it is easy to see how every reindexing function f : A → B induces a functor R(f) : N -LATS_{A} → N -LATS_{B} and thus that all the categories N -LATS_{I} can be “glued” together with the Grothendieck construction to provide a cofibration N -LATS → N.

An adjunction The category N -LTS_{I} is a full subcategory of N -LATS_{I}. Moreover the embedding functor, L_{I}, has a right inverse R_{I}. The functor L_{I} can be defined as follows:

\underline{On objects} L_{I}⟨S, ⟶, i⟩ = ⟨S, ⟶′, i, E, I⟩. The set of events E is the set of equivalence classes of transitions of the equivalence relation ⌢ generated by the following reflexive and transitive relation: (A ⊢ s ⟶^{ℓ} t ⊣ B) ⌢^{∘} (A′ ⊢ s′ ⟶^{ℓ′} t′ ⊣ B′) if there exist f : A →_{inj} A′ and g: B \A → B′ such that s′ = fs, t′ = [ιf, g]t and ℓ′ = [ιf, g]ℓ, where ι : A′ ↪ B′ is the inclusion function. The independence relation I is the empty relation. The transition relation is defined as follows:

A ⊢ s⟶′_{e}^{ℓ}t ⊣ B if e = [A ⊢ s ⟶^{ℓ} t ⊣ B]_{⌢}.

\underline{On arrows} L_{I}(α) = ⟨α, η⟩, where η([A ⊢ s ⟶^{ℓ} t ⊣ B]_{⌢}) = [A ⊢ α_{A}s ⟶^{ℓ} α_{B}t ⊣ B]_{⌢}.

The functor R_{I} is defined by simply forgetting the extra structure, i.e. the set of events and the independence relation, which distinguishes N -LATSs from N -LTSs. From a categorical perspective it would be nice if the pair of functors ⟨L_{I}, R_{I}⟩ was an adjoint pair. This might help in providing a formal understanding of the relationship between the constructions used for the semantics of π-terms in either categories. Unfortunately, as also noted in [58] for the case of “standard” LATS and LTS, this is not the case: in an (Indexed) LATS, one can have several transitions carrying the same label between two states. This is something clearly not possible for an (Indexed) LTS. This mismatching leads to the impossibility of defining a natural transformation LR ⟹ Id which can act as the counit of the adjunction. A solution out of this problem is that of imposing an extra extensionality axiom on (Indexed) LATS. It is worth noticing that this axiom also appeared in [25] where a similar formal relationship was sought between LATS and Winskel and Nielsen’s Transition System with Independence (a transition system analogue of Petri nets).

Theorem 6.3 The pair of functors ⟨L_{I}, R_{I}⟩ forms an adjoint pair, with L_{I} left adjoint and R_{I} right adjoint, if we restrict to consider N -LATS such that for every events e, e′ ∈ E,

s⟶_{e}^{ℓ}t and s⟶_{e′}^{ℓ′}t implies ℓ ≠ ℓ′ .

Proof: From the definition of adjunction [36], to show that L_{I} ⊣ R_{I}, one has to provide natural transformations η: Id ⇒ R_{I}L_{I} and ε: L_{I}R_{I} ⇒ Id such that

ε_{L_{I}} (L_{I}η) = Id_{L_{I}}  and  (R_{I}ε)η_{R_{I}} = Id_{R_{I}} .

As we said R_{I} is right inverse to L_{I}, thus η is naturally defined to be the identity natural transformation. Now, if T = ⟨S, ⟶, i, E, I⟩ is a N -LATS, define ε_{T} : L_{I}R_{I}T → T to be ε_{T} = ⟨1_{S}, σ⟩, where for every event [A ⊢ s ⟶^{ℓ} t ⊣ B]_{⌢} of L_{I}R_{I}T, σ([A ⊢ s ⟶^{ℓ} t ⊣ B]_{⌢}) = e with e the unique event of E, such that A ⊢ s⟶_{e}^{ℓ}t ⊣ B in T.

It should be clear the importance of the extensionality axiom in making ε_{T} well-defined. It is now immediately clear that, if T is an N -LTS, then ε_{L_{I}T} is the identity arrow and thus

ε_{L_{I}T} (L_{I}η_{T}) = 1_{L_{I}T}.

On the other hand, for every N -LATS T, R_{I}ε_{T} is clearly the identity on R_{I}T, thus it is also the case that (R_{I}ε_{T})η_{R_{I}T} = 1_{R_{I}T}.

□

Notice that for any π-term P with free names in I, the corresponding Indexed LATS [[P]]_{I}^{c} satisfies the condition of the Theorem above. Moreover, under the hypothesis of Theorem 6.3, the adjoint functors L_{I} ⊣ R_{I} induce a (fibred) adjunction L ⊣ R: N -LATS → N -LTS.

7 Alternative indexing structure

In this paper we considered transition systems with an indexed sets of states. The indexing structure (the category N) that we have chosen is not the only possible one. Other possibilities might reasonably be conceived. In this last section we examine those which have occurred to us and we discuss trade-offs briefly.

Sets and injections Instead of indexing by the category N one can index by N_{inj}, the subcategory of N with all objects but only injective functions as arrows. This gives a simpler structure, in which the transitions of a reindexed state fs are always determined by those of s. Specifically, define an N_{inj}-LTS to be a structure T = ⟨S: N_{inj} → Set, ⟶, i⟩ where i ∈ S and ⟶⊆ S × Lab × S, satisfying axioms 1, 3a, 3b, 4 of Section 3. To make input prefix definable, however, the denotation of a process with n free names must be a function from n-tuples of names to N_{inj}-LTSs, not simply an N -LTS – to define [[xy.P]] one would need (at least) [[{^{z}/_{y}}P]] for all z ∈ fn(P), w. Moreover, we doubt whether an analogue of the input axioms 2a,2b could be stated. Alternatively, one might consider the half-way house of an N_{inj+}-LTS – an N_{inj}- LTS with additional data (and appropriate axioms) specifying how the initial state (but no other state) is affected by non-injective renamings. This is less mathematically natural, but has enough structure to support definitions of input prefixing, and of the bisimulation congruence ∼ obtained by closing ˙∼ under arbitrary renamings.

Building restriction into the indexing It is arguable that, as restriction is a fundamental π-calculus concept, one should take models with more data than our N -LTSs, specifying how the transitions of states change when names are restricted. This leads to more complex axioms, though clearly also to a simpler definition of the restriction operator. In more detail, define N_{ν} to be the category with objects finite subsets of N and arrows pairs ⟨f, R_{f}⟩: A → B where f : A ⇀ B is a partial function and R_{f} ⊆ (A \ dom(f)) × (A \ dom(f)) is an equivalence relation. If A ⊢ s then the re-indexing of s along ⟨f, R_{f}⟩ should be thought of as the state in which names in A \ dom(f) have been restricted, after being quotiented by R_{f}, and other names have been substituted as specified by f. Define composition of arrows by ⟨g, R_{g}⟩ ∘ ⟨f, R_{f}⟩ = ⟨g ∘ f, R_{g∘f}⟩ where R_{g∘f} = R_{f} ∪ { (a, a′) | f(a) R_{g} f(a′) }. Preliminary investigation suggests that with this structure it may be possible to relate parallel composition to the categorical product, as in [58]. Moreover, from the categorical point of view, the explicit restriction reindexings, makes the resulting cofibrations N -LTS → N_{ν} and N -LATS → N_{ν} bifibrations, i.e. fibrations as well as cofibrations.

Choosing new names In our definition, for a state s above A, all names w ∉ A are treated symmetrically – corresponding to the operational fact that (if x ∈ A) there is a transition A ⊢ (νz)\overline{x}z ⟶^{\overline{x}w} 0 for any w ∉ A. One can instead take a chosen new – a function ν: P_{fin}(N) → N such that ∀A . νA ∉ A. This leads to an endofunctor δ: N → N defined by δ A = A ∪ {νA} and δ(f) = f ∪ {νA ↦ νB}; the axioms can be restated in terms of δ. In this paper we have not taken a chosen new in order to keep the tight correspondence with the operational semantics, and for notational simplicity. The obvious advantage of taking such an approach would be that of drastically restricting the degree of branching of the transition systems. The drawback is in the extra complications occurring in the axiomatisation having to do with the renaming of newly generated and communicated channels.

The chosen-new version of N_{inj} is essentially the indexing structure used in [56, 20, 24, 12].

8 Future work and applications

We conclude by hinting at several possible applications and extensions.

Syntax-free Metatheory

Firstly, N -LTSs provide a setting in which some of the π-calculus early metatheory can be developed in a syntax-free style, independently of the exact choice of calculus. In particular, one could show congruence results for operational equivalences with respect to the N -LTS operations defined in Section 4, perhaps developing the open-map approach of [31, 13, 14], and could prove characterisation results relating operational equivalences with classes of formulae of suitable modal logics.

Model Checking

We believe our structures may form a useful basis for π-calculus interleaving and partial-order model checking, via notions of finitely presentable N -LTS and N -LATS. The π labelled transition relation is (for non-trivial processes) infinite-branching, but when checking (eg) bisimulation of processes it is often intuitively clear that only a finite number of transitions are ‘important’. Several authors have worked on finitary characterisations using a refined symbolic operational semantics [35, 45, 5]. It may be fruitful to consider the alternative approach of model-checking algorithms that work directly over finite presentations, thereby again decoupling the algorithm design from the exact choice of calculus. Depending on what equivalence (or modal properties) one wishes to check, it may be appropriate to work not with N -LTSs but with the N_{inj}-LTSs or N_{inj+}-LTSs of Section 7. For illustration we sketch a notion of finite presentation of an N_{inj}-LTS. We expect there to be interesting relationships with the HD-automata of [43], which provide a notion of minimal realization.

Definition 8.1 A finite presentation T_{0} of an N_{inj}-LTS consists of data ⟨S_{0}, ⟶_{0}, i⟩, where

1. S_{0} is function from |N_{inj}| to finite sets which is empty almost everywhere. We then define a functor S: N_{inj} → Set by

S(B) =^{def} { ⟨s, f⟩ | ∃A . s ∈ S_{0}(A) ∧ f : A →_{inj} B }
S(g)(⟨s, f⟩) =^{def} ⟨s, g ∘ f⟩  for g: B →_{inj} C and ⟨s, f⟩ ∈ S(B)

As before we write S for the set ∐_{A∈|N |} S(A), and also write S_{0} for ∐_{A∈|N |} S_{0}(A).

2. ⟶_{0}⊆ S_{0} × Lab × S is a finite relation.

3. i ∈ S.

satisfying the axiom

1. (Naming) ⟨A, s⟩ ⟶^{ℓ}_{0} ⟨B, ⟨t, f⟩⟩ ⟹ chan(ℓ) ⊆ A ∧ B = A ∪ fn(ℓ) (here s ∈ S_{0}(A),

t ∈ S_{0}(C), and f : C →_{inj} B).

A more sophisticated notion would include also a finite number of equalities between elements of S. One could now relate the finitely-presentable N_{inj}-LTSs to those denotable by finite-control process terms, and consider model-checking algorithms over the finite presentations.

Adding Values

In this paper we addressed only monadic π-calculus, for notational simplicity. Extension to calculi with polyadic or tuple communication is straightforward. Some applications – notably those involving cryptography – require a further extension to allow communication of values of datatypes that are specified with equations or rewrite rules. This should also be straightforward (though one may wish to exclude equations that discard variables, to obtain an unambiguous notion of the new names in a value). An operational development with equational datatypes has been given by Abadi and Fournet [1].

Synchronisation Algebras

More speculatively, one can ask whether synchronisation algebras [58] can be generalised to cover a useful variety of name-passing calculi, thereby supporting uniform definitions of N -LTS and N -LATS. A good test-case here is the synchronisations of the box-π calculus [53, 54], which has an early LTS that is interestingly different from that of the π-calculus. One might also begin a study of early rule formats.

Security Protocols

An analogue of N -LTS, extended to allow communication of tuples and encrypted values, may provide a useful basis for proofs and model-checking of cryptographic protocols. There are two points here. Firstly, many security properties are stated using a quantification over all possible ‘attacker’ processes. Quantifying over all elements of the model, not merely over syntacticallydenotable elements, therefore gives stronger security properties that are less dependent on the precise expressiveness of the calculus used.

Secondly, the model allows alternative styles of definition of system behaviours. For example, in the work of Paulson (see e.g. [44]) systems are described by disjunctions of predicates specifying when a given trace can be extended by a particular label. One can characterise the well-formed such predicates (loosely, those that are preserved by new-name substitutions), that define N_{inj}-LTSs (with state-sets simply the set of all traces). These can then be composed by parallel and restriction operators. One may thereby obtain a tight connection between this work and process-calculus modeling of protocols, e.g. [2].

Out \overline{A ⊢ C:\overline{x}v ⟶^{\overline{x}v}_{C} 0}  In \overline{A ⊢ xp.P ⟶^{xv}_{C} C •\{^{v}/_{p}\}P}

Par \frac{A ⊢ P ⟶^{ℓ}_{C} P′}{A ⊢ P | Q ⟶^{ℓ}_{C} P′ | Q}  Comm \frac{A ⊢ P ⟶^{\overline{x}v}_{C} P′ A ⊢ Q ⟶^{xv}_{C} Q′}{A ⊢ P | Q ⟶^{τ}_{∅} ν(\{v\} \ A)(P′ | Q′)}

Res \frac{A, x ⊢ P ⟶^{ℓ}_{C} P′ x ∉ fn(ℓ)}{A ⊢ νxP ⟶^{ℓ}_{C} νxP′} Open \frac{A, x ⊢ P ⟶^{\overline{y}x}_{C} P′}{A ⊢ νxP ⟶^{\overline{y}x}_{C} P′}

In all rules with conclusion of the form A ⊢ P ⟶^{ℓ}_{C} Q there is an implicit side condition fn(P) ⊆ A. Symmetric versions of (Par) and (Comm) are elided.

Figure 4: Coloured π operational semantics

Relating to Coloured Semantics

Lastly, we observe that the model-theoretic view would enhance work on secure encapsulation [53, 54]. As above, quantifying over elements of the model, rather than over syntactic processes, would allow stronger security properties to be stated. Further, that work introduced an adhoc coloured operational semantics, to provide a tractable approximate notion of causality for the box-π calculus used there. We state conjectures relating the (π fragment of the) coloured semantics to N -LATS, as a step towards understanding exactly what approximation is involved.

The coloured semantics takes a fixed set col of colours (or initial causes, or principals – we use the terms interchangeably) disjoint from N. Let C, D, K range over subsets of col. We define a coloured box-π calculus by annotating all outputs with sets of colours:

P, Q ::= 0 | P | Q | C:\overline{x}v | xp.P | νxP

If P is a coloured term we write |P | for the term of the original syntax obtained by erasing all annotations. Conversely, for a term P of the original syntax C ∘ P denotes the term with every particle coloured by C. In the coloured output C:\overline{x}v think of C as recording the causal history of the output particle – C is the set (possibly empty) of principals p ∈ C that have affected the particle in the past. In an initial state all outputs might typically be coloured by singleton sets giving their actual principals. The coloured labelled transition relation has the form

A ⊢ P ⟶^{ℓ}_{C} Q

where A is a finite set of names, fn(P) ⊆ A, and ℓ is a label as before; it should be read as ‘in a state where the names A may be known to P and its environment, process P can do ℓ, coloured C, to become Q’. Here C records causal history, giving all the principals which have directly or indirectly contributed to this action. The relation is defined as the smallest relation satisfying the rules in Figure 4.

Consider a coloured trace t and a run r

A_{0} ⊢ ∅ ∘ P ⟶^{ℓ_{1}}_{C_{1}} R_{1} ⟶^{ℓ_{2}}_{C_{2}} R_{2} … ⟶^{ℓ_{n}}_{C_{n}} R_{n}, A_{0} ⊢ s_{0}⟶_{e_{1}}^{ℓ_{1}}s_{1}⟶_{e_{2}}^{ℓ_{2}}s_{2} ⋯ ⟶_{e_{n}}^{ℓ_{n}}s_{n}

Given a run r and an arbitrary equivalence relation ≃ on the set { e_{i} | ∃x, v . ℓ_{i} = xv } and col the equivalence classes, define a coloured trace r/ ≃ (without the process parts) with labels ℓ_{1} … ℓ_{n}, with inputs ℓ_{j} coloured [e_{j}]_{≃}, outputs ℓ_{j} coloured by ⋃{ [e_{i}]_{≃} | i an input and i ⊴_{I}^{r} j } and taus coloured ∅. We conjecture that given r and an arbitrary equivalence relation ≃ there is a coloured trace r/ ≃, and that given t there exists a run r and an equivalence relation ≃ such that t = r/ ≃.

A Proof of Theorem 5.6

In this appendix we provide all the necessary auxiliary results for and the proof of Theorem 5.6 whose text, we recall, is the following:

Let P and Q be two terms of the π-calculus with free names in I and let [[P]]_{I}^{c} and [[Q]]_{I}^{c} be their interpretations as N -LATS’s. Then [[P]]_{I}^{c} is history preserving bisimilar to [[Q]]_{I}^{c} if and only if P is strongly causal bisimilar to Q.

Notation: Throughout this appendix we write P, Q for generic π-terms, regarded as causal π-terms and C (possibly indexed) for generic causal π-terms.

We then begin with some auxiliary definitions and lemmas.

Definition A.1 If P is a π-term with free names in I, define Run(P)_{I} to be the set of runs of

P with initial name set I. Given a causal run r = I ⊢ P ⟶_{K_{1};k_{1}}^{ℓ_{1}}C_{1} ⟶_{K_{2};k_{2}}^{ℓ_{2}}C_{2}⟶ ⋯ ⟶_{K_{n};k_{n}}^{ℓ_{n}}C_{n} define

1. end(r) =^{def} C_{n}

2. label(r) =^{def} {ℓ_{j} | 1 ≤ j ≤ n}

3. names(r) =^{def} I ∪ ⋃_{ℓ∈label(r)} fn(ℓ)

4. po(r)_{I} to be the following labelled partial order: ([n], ≤_{c}, l), where l(i) = ℓ_{i} and i ≤_{c} j if k_{i} ∈ K_{j} ∪ {k_{j}}.

5. for any set of causes K ⊆ K(C_{n}), the cause-closure of K with respect to r, \overline{K} =^{def} K ∪ ⋃_{k_{j}∈K} K_{j}

To prove that the relation ≤_{c} is a partial order it suffices to prove the following theorem:

Theorem A.2 Given a causal-π run, I ⊢ P ⟶_{K_{1};k_{1}}^{ℓ_{1}}C_{1} ⟶_{K_{2};k_{2}}^{ℓ_{2}}C_{2}⟶ ⋯ ⟶_{K_{n};k_{n}}^{ℓ_{n}}C_{n}, for every i < n, if

k_{i} ∈ K_{n}, then K_{i} ⊆ K_{n}.

The proof requires a new definition and a lemma.

Definition A.3 For every causal-π term, C and cause k, define k ↓ C to be the set of sets of causes inductively defined as follows:

k ↓ 0 = ∅  k ↓ μ.C = k ↓ C
k ↓ (νx)C = k ↓ C  k ↓ (C_{1} + C_{2}) = (k ↓ C_{1}) ∪ (k ↓ C_{2})
k ↓ (C_{1} | C_{2}) = (k ↓ C_{1}) ∪ (k ↓ C_{2})  k ↓ K :: C = \{ \begin{matrix}\{K ∪ K′ | K′ ∈ k ↓ C\} & if k ∉ K \\ \{K ∪ K′ | K′ ∈ k ↓ C\} ∪ \{K\} & otherwise, \end{matrix}

where μ is any output, input or τ prefix.

The set k ↓ C aims at syntactically identify the sets of causes which precede (occurrences of) k in the partial order. A few useful properties can be proved to hold:

Lemma A.4 If, for every set X and Y, we write [x ⇝ Y]X, for the set (X \ {x}) ∪ Y if x ∈ X and X if x ∉ X, then k ↓ [k ⇝ K]C = {[k ⇝ K]X | X ∈ k ↓ C}, for any causal π-term C, cause k and cause set K with k ∈ K.

Proof: The proof is a straightforward structural induction.

□

Lemma A.5 For any causal π-transition A ⊢ C⟶_{K;k}^{ℓ}C′ the following facts hold:

1. k ↓ C′ = {K ∪ {k}}

2. for all k̂ ∈ K, there exists K̂ ∈ k̂ ↓ C such that K̂ ⊆ K

3. for all k̂ ≠ k and for all all K′ ∈ k̂ ↓ C′, there exists K̂ ∈ k̂ ↓ C such that K̂ ⊆ K′ Proof: The proof is an easy rule induction. Point (1) requires point (A.4) to resolve the case of the rule COM.

□

Equipped with the Lemma A.5 it is now easy to prove the Theorem A.2. Proof:[of Theorem A.2] The proof is by induction on the length of the run. The base case, i.e. the length is 0, is obviously trivial. For the inductive step, suppose k_{i} ∈ K_{n} (with n > 0), then by Lemma A.5(2) there exists K̂ ∈ k_{i} ↓ C_{n−1} such that K̂ ⊆ K_{n}. By induction on (n − 1 − i) it is now easy to show that K_{i} ⊆ K̂ and thus that K_{i} ⊆ K_{n}. In fact, if n − 1 − i = 0 then K̂ = K_{i} ∪ {k_{i}}, by Lemma A.5(1), otherwise, by Lemma A.5(3), there exists ˆ K̂ ∈ k_{i} ↓ C_{n−2} such that ˆ K̂ ⊆ K̂ and by inductive hypothesis K_{i} ⊆ ˆ K̂.

□

We define now the notion of run-bisimulation, relating the behaviour of causal π-processes and N -LATSs. Notation: If r is a causal run and names(r) ⊢ end(r)⟶_{K;k}^{ℓ}C′ is a transition, we write r⟶_{K;k}^{ℓ}C′ for the run which extends r with that transition. If r and r′ are runs, we write r⟶_{K;k}^{ℓ}r′ if r′ extends r with the transition names(r) ⊢ end(r)⟶_{K;k}^{ℓ}end(r′).

Definition A.6 A relation R ⊆ Run(P) × Run(T) between causal runs of a π-term P with free names in I and runs of an N -LATS T with initial name-set I is a run-bisimulation if

1. (I ⊢ P, I ⊢ i) ∈ R

2. (r, ρ) ∈ R implies po(r)_{I} = po(ρ)_{I}

3. (r, ρ) ∈ R and r⟶_{K;k}^{ℓ}r′ implies that there exists an e ∈ E such that ρ⟶_{e}^{ℓ}ρ′ and (r′, ρ′) ∈ R

4. (r, ρ) ∈ R and ρ⟶_{e}^{ℓ}ρ′, implies that there exist K and k such that r⟶_{K;k}^{ℓ}r′ and (r′, ρ′) ∈ R .

Causal bisimulations in π, gives rise to relations between runs of processes:

Definition A.7 If B is a causal bisimulation, such that P BQ, define

Run(B) ⊆ Run(P) × Run(Q)

to be the following relation between causal runs of P and Q respectively:

if r = I ⊢ P ⟶_{K_{1};k_{1}}^{ℓ_{1}}C_{1} ⟶_{K_{2};k_{2}}^{ℓ_{2}}C_{2}⟶ ⋯ ⟶_{K_{n};k_{n}}^{ℓ_{n}}C_{n} and s = I ⊢ Q ⟶_{K_{1};k_{1}}^{ℓ_{1}}D_{1} ⟶_{K_{2};k_{2}}^{ℓ_{2}}D_{2}⟶ ⋯ ⟶_{K_{n};k_{n}}^{ℓ_{n}}D_{n} are

causal runs (notice the coincidence of initial name-set, labels and causes), then r Run(B) s if for all i ≤ n it is the case that C_{i}BD_{i}.

Run-bisimulations and causal bisimulations originate history-preserving bisimulations between N -LATSs, while run-bisimulations and history preserving bisimulations originate causal bisimulations.

Lemma A.8 Let R ⊆ Run(P) × Run(T) and S ⊆ Run(Q) × Run(U) be two run-bisimulations. Then the following two facts hold:

1. If B is a causal bisimulation relating P and Q, then S ∘ Run(B) ∘ R^{∘}, where R^{∘} is the relation opposite of R, is an history-preserving bisimulation.

2. If B ⊆ Run(T)×Run(U) is an history preserving bisimulation, then the symmetric closure of the relation

{(C, D) | ∃r, r′. r (S^{∘} ∘ B ∘ R) r′ ∧ end(r) = C ∧ end(r′) = D}

is a causal bisimulation, which obviously relates P and Q.

Proof: Straightforward.

□

In order to prove Theorem 5.6, we then show that for every process term P, with free names in I, there is a run-bisimulation between Run(P)_{I} and Run([[P]]_{I}^{c}). Combining this with Lemma A.8 will then give us a proof of the Theorem.

Lemma A.9 Let P be a π-term with free names in I, then there exists a run-bisimulation R^{P} ⊆ Run(P)_{I} × Run([[P]]_{I}^{c}).

Proof:The proof is by induction on the size of P, where the size of the process is defined as its number of process constructors. The base case is trivially provided by the unique process of size one, namely the nil process. One then shows how to build run bisimulations for compound process terms out of run bisimulation of processes of smaller size.

Most cases are straightforward, we consider here only the two delicate ones, i.e. when a term of size greater than 1 is either a restriction or a parallel composition of terms.

Restriction Suppose P = (νx)Q and assume, by inductive hypothesis, the existence for each x̂ ∈ N \ I of a run-bisimulation R^{{x̂/x}Q} ⊆ Run({x̂/x}Q)_{I,x̂} × Run([[{x̂/x}Q]]_{I,x̂}^{c}). Let also [[{x̂/x}Q]]_{I,x̂}^{c} be the tuple ⟨Sx̂, ⟶x̂, ix̂, Ex̂, Ix̂⟩. Define R to be the smallest set of 4-tuples

⟨r, ρ, r̂, ρ̂⟩ ∈ ⋃_{x̂∈N \I}(Run({x̂/x}Q)_{I,x̂} × Run([[{x̂/x}Q]]_{I,x̂}^{c})) × Run(P)_{I} × Run([[P]]_{I}^{c})

such that:

• ⟨(I, x̂) ⊢ {x̂/x}Q, (I, x̂) ⊢ ix̂, I ⊢ P, I ⊢ r[ix̂]_{↔_{I}} ⟩ ∈ R, for each x̂ ∈ N \ I • if ⟨r, ρ, r̂, ρ̂⟩ ∈ R then the following two conditions are satisfied for every label ℓ, cause set

K, cause k, event e, causal-π agent C and state s:

1. if ⟨r⟶_{K;k}^{ℓ}C, ρ⟶x̂_{e}^{ℓ}s⟩ ∈ R^{{x̂/x}Q}, and if for every ℓ′ ∈ label(r) ∪ {ℓ}, x̂ ∉ fn(ℓ′) then

⟨r⟶_{K;k}^{ℓ}C, ρ⟶x̂_{e}^{ℓ}s , r̂⟶_{K;k}^{ℓ}(νx̂)C, ρ̂⟶_{e}^{ℓ}r[s]_{↔_{A}}⟩ ∈ R ,

where A = names(r) ∪ fn(ℓ).

2. if ⟨r⟶_{K;k}^{ℓ}C, ρ⟶x̂_{e}^{ℓ}s⟩ ∈ R^{\{x̂/x\}Q}, and if there exists ℓ′ ∈ label(r)∪\{ℓ\} such that ℓ′ = \overline{y}x̂,

for some y ∈ N then

⟨r⟶_{K;k}^{ℓ}C, ρ⟶x̂_{e}^{ℓ}s, r̂⟶_{K;k}^{ℓ}C, ρ̂⟶_{e}^{ℓ}ls⟩ ∈ R

Define now R^{P} =^{def} {⟨r̂, ρ̂⟩ | ∃ r, ρ. ⟨r, ρ, r̂, ρ̂⟩ ∈ R}. It is not difficult to verify that R^{P} is a run-bisimulation.

Parallel composition Suppose P = P_{1} | P_{2} and that R^{P_{1}} and R^{P_{2}} are run-bisimulations. Define R to be the smallest set of 7-tuples ⟨Z, r_{1}, ρ_{1}, r_{2}, ρ_{2}, r, ρ⟩ in

P_{fin}(N) × Run(P_{1})_{I} × Run([[P_{1}]]_{I}^{c}) × Run(P_{2})_{I} × Run([[P_{2}]]_{I}^{c}) × Run(P)_{I} × Run([[P]]_{I}^{c})

such that

• ⟨∅, I ⊢ P_{1}, I ⊢ i_{1}, I ⊢ P_{2}, I ⊢ i_{2}, I ⊢ P, I ⊢ i_{1} |_{I} i_{2}⟩ ∈ R

• if ⟨Z, r_{1}, ρ_{1}, r_{2}, ρ_{2}, r, ρ⟩ ∈ R then the following five conditions and their obvious symmetric counterparts hold for any (possibly subscripted) label ℓ, cause set K, cause k, event e, causal-π agent C, state s and names x, y ∈ N:

1. if ⟨r_{1}⟶_{K;k}^{ℓ}C, ρ_{1}⟶_{e}^{ℓ}s⟩ ∈ R^{P_{1}} and k ∉ K(end(r)) and chan(ℓ) ∩ Z = ∅ and val(ℓ) ∩ (Z ∪

names(r_{2}) \ names(r_{1})) = ∅ then

⟨Z, r_{1}⟶_{K;k}^{ℓ}C, ρ⟶_{e}^{ℓ}s, r_{2}, ρ_{2}, r⟶_{\overline{K};k}^{ℓ}(νZ )(C | end(r_{2})), ρ⟶_{⟨e,∗⟩}^{ℓ}(ȷ_{1}s |_{A} ȷ_{2}end(ρ_{2}))⟩ ∈ R ,

where names(r_{1}) ∪ val(ℓ) ↪^{ȷ_{1}} names(r_{1}) ∪ val(ℓ) ∪ names(r_{2}) ↩^{ȷ_{2}} names(r_{2}) and A = names(r) ∪ val(ℓ).

2. if ⟨r_{1}⟶_{K;k}^{xy}C, ρ⟶_{e}^{xy}s⟩ ∈ R^{P_{1}} and k ∉ K(end(r)) and x ∉ Z and y ∈ (names(r_{2}) \

names(r_{1})) then

⟨Z, r_{1}⟶_{K;k}^{xy}C, ρ⟶_{e}^{xy}s, r_{2}, ρ_{2}, r⟶_{\overline{K};k}^{xy}(νZ )(C | end(r_{2})), ρ⟶_{⟨e,∗⟩}^{xy}(ȷ_{1}s |_{A} ȷ_{2}end(ρ_{2}))⟩ ∈ R ,

where names(r_{1}) ∪ {y} ↪^{ȷ_{1}} names(r_{1}) ∪ names(r_{2}) ↩^{ȷ_{2}} names(r_{2}) and A = names(r).

3. if ⟨r_{1}⟶_{K;k}^{\overline{x}y}C, ρ_{1}⟶_{e}^{\overline{x}y}s⟩ ∈ R^{P_{1}} and k ∉ K(end(r)) and x ∉ Z and y ∈ Z then

⟨Z \ \{y\}, r_{1}⟶_{K;k}^{\overline{x}y}C, ρ⟶_{e}^{\overline{x}y}s, r_{2}, ρ_{2}, r⟶_{\overline{K};k}^{\overline{x}y}(ν(Z \ \{y\}))(C | end(r_{2})), ρ⟶_{⟨e,∗⟩}^{xy}(ȷ_{1}s |_{A} ȷ_{2}end(ρ_{2}))⟩ ∈ R ,

where names(r_{1}) ↪^{ȷ_{1}} names(r_{1}) ∪ names(r_{2}) ↩^{ȷ_{2}} names(r_{2}) and A = (names(r), y).

4. if ⟨r_{1}⟶_{K_{1};k}^{\overline{x}y}C_{1}, ρ_{1}⟶_{e_{1}}^{\overline{x}y}s_{1}⟩ ∈ R^{P_{1}} and ⟨r_{2}⟶_{K_{2};k}^{xy}C_{2}, ρ_{2}⟶_{e_{2}}^{xy}s_{2}⟩ ∈ R^{P_{2}} and y ∉ names(r_{1}) ∪

names(r_{2}) then

⟨(Z, y), r_{1} ⟶_{K_{1};k}^{\overline{x}y}C_{1}, ρ_{1}⟶_{e_{1}}^{\overline{x}y}s_{1}, r_{2} ⟶_{K_{2};k}^{xy}C_{2}, ρ_{2}⟶_{e_{2}}^{xy}s_{2}, r ⟶_{\overline{K_{1}∪K_{2}};k}^{τ}(ν(Z , y))(C_{1} | C_{2}), ρ ⟶_{⟨e_{1},e_{2}⟩}^{τ}(ȷ_{1}s_{1} |_{A} ȷ_{2}s_{2})⟩ ∈ R ,

where A = names(r) and

names(s_{1}) = names(r_{1})∪{y} ↪^{ȷ_{1}} names(r_{1})∪{y}∪names(r_{2}) ↩^{ȷ_{2}} names(r_{2})∪{y} = names(s_{2}) .

5. if ⟨r_{1}⟶_{K_{1};k}^{\overline{x}y}C_{1}, ρ_{1}⟶_{e_{1}}^{\overline{x}y}s_{1}⟩ ∈ R^{P_{1}} and ⟨r_{2}⟶_{K_{2};k}^{xy}C_{2}, ρ_{2}⟶_{e_{2}}^{xy}s_{2}⟩ ∈ R^{P_{2}} and y ∈ (names(r_{1}) \

names(r_{2})) ∪ Z then

⟨Z, r_{1} ⟶_{K_{1};k}^{\overline{x}y}C_{1}, ρ_{1}⟶_{e_{1}}^{\overline{x}y}s_{1}, r_{2} ⟶_{K_{2};k}^{xy}C_{2}, ρ_{2}⟶_{e_{2}}^{xy}s_{2}, r ⟶_{\overline{K_{1}∪K_{2}};k}^{τ}(νZ )(C_{1} | C_{2}), ρ ⟶_{⟨e_{1},e_{2}⟩}^{τ}(ȷ_{1}s_{1} |_{A} ȷ_{2}s_{2})⟩ ∈ R ,

where A = names(r) and

names(s_{1}) = names(r_{1}) ↪^{ȷ_{1}} names(r_{1}) ∪ names(r_{2}) ↩^{ȷ_{2}} names(r_{2}) = names(s_{2}) .

Define now

R^{P} = {⟨r, ρ⟩ | ∃ ⟨Z, r_{1}, ρ_{1}, r_{2}, ρ_{2}, r, ρ⟩ ∈ R} .

The five conditions (and their symmetric counterparts) cover all possible cases of how transitions in the components of a (restricted) parallel composition induce transition in the (restricted) parallel composition process itself. Condition 1 considers all possible kind of transitions in one of the components. The restriction on val(ℓ) is to ensure that no names from the set Z are communicated as outputs and that the outputs or inputs of new names, with respect to one component only are also outputs or inputs of a new name in the compound process. Condition 2 and 3 supplement Condition 1: Condition 2 by considering what happens in the cases of the input of a name which is new with respect to one component but not the other; Condition 3 by handling the case of the output of a name in Z. Condition 4 and 5 analyse the possibility of an internal communication between the two components which might lead to the extrusion of the scope of some restricted name.

It is slightly more laborious, compared to the case of restriction, to verify that R^{P} is a run bisimulation as the equality between the partial orders induced by related runs is not transparently clear but need to be proved by induction on the length of the (related) runs. We leave to the reader to work out the necessary details.

□

We are finally ready to put all this together and prove Theorem 5.6:

Proof:[of Theorem 5.6] Let P and Q be two π-terms with free names in I. By Lemma A.9, there exist run-bisimulations R^{P} ⊆ Run(P)_{I} × Run([[P]]_{I}^{c}) and R^{Q} ⊆ Run(Q)_{I} × Run([[Q]]_{I}^{c}). Thus is P is causal bisimilar to Q, by Lemma A.8 (1), Run([[P]]_{I}^{c}) is history preserving bisimilar to Run([[Q]]_{I}^{c}). Vice versa if Run([[P]]_{I}^{c}) is history preserving bisimilar to Run([[Q]]_{I}^{c}), by Lemma A.8 (2), P is causal bisimilar to Q.

□

References

[1] M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In Proceedings of POPL 2001, Jan. 2001. To appear.

[2] M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. In Proceedings of the Fourth ACM Conference on Computer and Communications Security, Zürich, pages 36–47. ACM Press, Apr. 1997.

[3] M. Bednarczyk. Categories of Asynchronous Systems. PhD thesis, University of Sussex, 1988.

[4] M. Boreale and R. De Nicola. Testing equivalences for mobile processes. Information and Computation, 120:279–303, 1995.

[5] M. Boreale and R. De Nicola. A symbolic semantics for the π-calculus. Information and Computation, 126(1):34–52, 1996.

[6] M. Boreale and D. Sangiorgi. A fully abstract semantics for causality in the π-calculus. Acta Informatica, 35:353–400, 1998.

[7] G. Boudol. Asynchrony and the π-calculus. Technical Report 1702, INRIA, Sophia Antipolis, 1992.

[8] G. Boudol and I. Castellani. Permutation of transitions: an event structure semantics for CCS and SCCS. In Proc. of REX School/Workshop, volume 354 of Lecture Notes in Computer Science, pages 411–427, 1988.

[9] N. Busi and R. Gorrieri. A petri net semantics for π-calculus. In I. Lee and S. A. Smolk, editors, Proceedings of the 6th International Conference on Concurrency Theory, CONCUR ’95, volume 962 of Lecture Notes in Computer Science, pages 145–159. Springer-Verlag, 1995.

[10] G. L. Cattani. Presheaf Models for Concurrency. PhD thesis, University of Aarhus, 1999.

[11] G. L. Cattani and P. Sewell. Models for name-passing processes: Interleaving and causal (extended abstract). In LICS 2000, Proceedings of the Fifteenth Annual IEEE Symposium on Logic in Computer Science, pages 322–333. IEEE Computer Society Press, 2000.

[12] G. L. Cattani, I. Stark, and G. Winskel. Presheaf models for the π-calculus. In Proceedings of the 7th International Conference on Category Theory and Computer Science, CTCS ’97, number 1290 in Lecture Notes in Computer Science, pages 106–126. Springer-Verlag, 1997.

[13] G. L. Cattani and G. Winskel. Presheaf models for concurrency. In D. van Dalen and M. Bezem, editors, Computer Science Logic. 10th International Workshop, CSL ’96, Annual Conference of the European Association for Computer Science Logic. Selected Papers, volume 1258 of Lecture Notes in Computer Science, pages 58–75. Springer-Verlag, 1997.

[14] G. L. Cattani and G. Winskel. Presheaf models for CCS-like languages. Technical Report 477, Cambridge University Computer Laboratory, 1999. Submitted for publication.

[15] P. Darondeau and P. Degano. Causal trees. In G. Ausiello, M. Dezani-Ciancaglini, and S. R. D. Rocca, editors, ICALP ’89, Sixteenth Colloquium on Automata, Languages and Programming, volume 372 of Lecture Notes in Computer Science, pages 234–248. Springer-Verlag, 1989.

[16] P. Degano, R. De Nicola, and U. Montanari. On the consistency of “truly concurrent” operational and denotational semantics (extended abstract). In LICS ’88, Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science, pages 133–141. IEEE Computer Society Press, 1988.

[17] P. Degano, R. De Nicola, and U. Montanari. Partial orderings descriptions and observations of nondeterministic concurrent processes. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, number 354 in Lecture Notes in Computer Science, pages 438–496, 1988.

[18] P. Degano and C. Priami. Non-interleaving semantics for mobile processes. Theoretical Computer Science, 216(1-2):237–270, 1999.

[19] M. P. Fiore, G. L. Cattani, and G. Winskel. Weak bisimulation and open maps (extended abstract). In LICS ’99 [34], pages 67–76.

[20] M. P. Fiore, E. Moggi, and D. Sangiorgi. A fully-abstract model for the π-calculus (extended abstract). In LICS ’96 [33], pages 43–54.

[21] M. P. Fiore, G. D. Plotkin, and D. Turi. Abstract syntax and variable binding. In LICS ’99 [34], pages 193–202.

[22] M. Gabbay and A. Pitts. A new approach to abstract syntax involving binders. In LICS ’99 [34], pages 214–224.

[23] R. v. Glabbeek and U. Goltz. Equivalence notions for concurrent systems and refinement of actions. In Mathematical Foundations of Computer Science 1989, number 379 in Lecture Notes in Computer Science, pages 237–248. Springer-Verlag, 1989.

[24] M. Hennessy. A fully abstract denotational semantics for the π-calculus. Technical Report 96:04, School of Cognitive and Computing Sciences, University of Sussex, 1996. To appear in Theoretical Computer Science.

[25] T. T. Hildebrandt and V. Sassone. Comparing transition systems with independence and asynchronous transition systems. In U. Montanari and V. Sassone, editors, CONCUR’96, Proceedings of the 7th International Conference on Concurrency Theory, volume 1119 of Lecture Notes in Computer Science, pages 84–97. Springer-Verlag, 1996.

[26] M. Hofmann. Semantical analysis of higher-order abstract syntax. In LICS ’99 [34], pages 204–213.

[27] K. Honda. Behavioural subtyping in name passing synchronisation trees. Available at

http://www.dcs.qmw.ac.uk/∼kohei/, 1999.

[28] K. Honda and M. Tokoro. An object calculus for asynchronous communication. In Proceedings of ECOOP’91 European Conference on Object-Oriented Programming, volume 512 of Lecture Notes in Computer Science, pages 133–147, 1991.

[29] B. Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam, 1999.

[30] L. J. Jagadeesan and R. Jagadeesan. Causality and true concurrency: A data-flow analysis of the pi-calculus (extended abstract). In Proceedings of AMAST ’95, Lecture Notes in Computer Science, pages 277–291. Springer-Verlag, 1995.

[31] A. Joyal, M. Nielsen, and G. Winskel. Bisimulation from open maps. Information and Computation, 127(2):164–185, 1996.

[32] A. Kiehn. Comparing locality and causality based equivalences. Acta Informatica, 31:697–718, 1994.

[33] LICS ’96, Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1996.

[34] LICS ’99, Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1999.

[35] H. Lin. Symbolic bisimulations and proof systems for the pi-calculus. Technical Report 1994:07, COGS, University of Sussex, 1994.

[36] S. Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, 1971.

[37] S. Mac Lane and I. Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer-Verlag, 1992.

[38] A. W. Mazurkievicz and J. Winkowski, editors. Proceedings of the 8th International Conference on Concurrency Theory, CONCUR ’97, volume 1243 of Lecture Notes in Computer Science. Springer-Verlag, 1997.

[39] R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.

[40] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes. II. Information and Computation, 100(1):41–77, 1992.

[41] R. Milner, J. Parrow, and D. Walker. Modal logics for mobile processes. Theoretical Computer Science, 114(1):149–171, 1993.

[42] U. Montanari and M. Pistore. Concurrent semantics for the π-calculus. In MFPS XI, Mathematical Foundations of Programming Semantics, Eleventh Annual Conference, volume 1 of ENTCS, pages 337–356. Elsevier, 1995.

[43] U. Montanari and M. Pistore. π-calculus, structured coalgebras and minimal HD-automata. In M. Nielsen and B. Rovan, editors, Mathematical Foundations of Computer Science 2000, volume 1893 of Lecture Notes in Computer Science. Springer, 2000.

[44] L. C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6:85–128, 1998.

[45] P. Quaglia. On the finitary characterization of π-congruences. Technical Report RS-97-52, BRICS, Aarhus University, 1997.

[46] A. Rabinovitch and B. Traktenbrot. Behaviour structures and nets. Fundamenta Informatica, 11(4):357–404, 1988.

[47] D. Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, University of Edinburgh, 1992.

[48] D. Sangiorgi. π-calculus, internal mobility, and agent-passing calculi. Theoretical Computer Science, 167(2):235–274, 1996.

[49] V. Sassone, M. Nielsen, and G. Winskel. Models for concurrency: towards a classification. Theoretical Computer Science, 170(1-2):297–348, 1996.

[50] P. Selinger. First order axioms for asynchrony. In Mazurkievicz and Winkowski [38], pages 376–390.

[51] P. Sewell. On implementations and semantics of a concurrent programming language. In Mazurkievicz and Winkowski [38], pages 391–405.

[52] P. Sewell. Pi calculi. In H. Bowman and J. Derrick, editors, Formal Methods for Distributed Processing, An Object Oriented Approach. CUP, 2000. To appear. Extended version as University of Cambridge TR 498, 2000.

[53] P. Sewell and J. Vitek. Secure composition of insecure components. In Proceedings of the 12th IEEE Computer Security Foundations Workshop. Mordano, Italy, pages 136–150. IEEE Computer Society, June 1999. Extended version as University of Cambridge TR 463, 1999.

[54] P. Sewell and J. Vitek. Secure composition of untrusted code: Wrappers and causality types. In Proceedings of CSFW 00: The 13th IEEE Computer Security Foundations Workshop., pages 269– 284. IEEE Computer Society, July 2000. Extended version as University of Cambridge TR 478, 1999.

[55] M. W. Shields. Concurrent machines. Theoretical Computer Science, 28:449–465, 1985.

[56] I. Stark. A fully abstract domain model for the π-calculus. In LICS ’96 [33], pages 36–42.

[57] W. Vogler. Generalized OM-bisimulation. Information and Computation, 118(1):38–47, 1995.

[58] G. Winskel and M. Nielsen. Models for concurrency. In Handbook of logic in computer science, Vol. 4, Oxford Sci. Publ., pages 1–148. Oxford Univ. Press, 1995.