Models for Name-Passing Processes: Interleaving and Causal (Extended Abstract)

In Proceedings of LICS 2000, \begin{matrix}c \\ ◯ \end{matrix}IEEE Computer Society

Gian Luca Cattani^{∗} and Peter Sewell^{†}

Computer Laboratory, University of Cambridge, England

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

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 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. In each case we relate a denotational semantics to an operational view, for bisimulation and causal bisimulation respectively. This is a first step towards a uniform understanding of the semantics and operations of name-passing calculi.

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 focusses 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 [MPW92], 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 [Bed88, Shi85, WN95]. In each case we give a denotational semantics of a π-calculus; we prove the operational early and causal bisimulations [San93, BS98] coincide with model-theoretic notions. In the full version of this extended abstract [CS00], we also investigate the properties of and relationship between categories of the two models, and give the omitted proofs. This is a first step towards a uniform understanding of the semantics and operations of name-passing calculi.

Interleaving The standard notion of labelled transition system (LTS) for calculi without value-passing is straightforward. For example, given a set N of 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

∗supported by EPSRC grant GR/L62290: Calculi for Interactive Systems: Theory and Experiment

†supported by a Royal Society University Research Fellowship

is inferred in the ‘early’ semantics of [MPW93, San93] 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 namesets 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. Many variant definitions of N -LTS are possible; we discuss the alternatives in Section 4. In Section 5 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 model-checking 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 [WN95]; the second is represented by various annotated operational semantics, e.g. [DDNM88a, BC88, DD89, Kie94, WN95]. The two seem to have been carried out almost independently – to our knowledge, the only works to make precise connections are [DDNM88a, BC88, WN95]. Moreover, only the syntactic approach has been developed to address name-passing, in the annotated operational models of [BS98, DP99]. There is also work that does not fit this categorisation, having both syntactic and model-theoretic aspects, with Petri nets and graph rewriting [BG95, MP95].

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 [Bed88, Shi85, WN95]. This is precisely related to causal bisimulation [BS98].

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 [DP99]. 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 previouslyextruded 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 6 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 5 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 [CS00] an abstract study of the structures defined in this paper is initiated. Categories N -LTS_{I} of Indexed LTS and N -LATS_{I} of Indexed LATS (each for initial nameset I) are defined. Their properties and mutual relationship are studied, as the first step towards an abstract understanding of the equivalences and constructions involved in the semantics of π-like process languages. Space limitations prevent us from presenting such results here.

Further Motivation, Future Directions and Related Work Viewing models categorically has proven useful in study of the interleaving/non-interleaving and lineartime/branching-time distinctions [SNW96]. Moreover, the categorical study of process calculi gives the possibility of obtaining general congruence results: in [WN95] categorical models of CCS-like processes are axiomatised and in [JNW96] an abstract model-theoretic notion of bisimulation is introduced (via open maps); in [CW97, CW99] 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 [CS00].

Among earlier models of π-processes, the name passing synchronisation trees of [Hon99] and presheaves of [CSW97] are the closest to our N -LTS, though they employ a slightly different indexing structure (cf. Section 4). In [CSW97] the models are defined using domain theoretical techniques similar to those employed in [Sta96, FMS96], 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 which adapt them to closely reflect paradigms such as the asynchronous π-calculus [Bou92, HT91]. In particular it should be quite straightforward to adapt the axioms of [Sel97] to our models. It should also be easy to address the πI-calculus [San96a], 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 and the presheaf model can, as far as we know, only achieve indirectly by means of a saturation construction [FCW99].

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 [Sew97, SV99a, SV99b, Sew00]. Presheaf models exist for both early and late notions [Cat99]. Moreover we should add that, in constrast to [Sta96, FMS96] (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 [Hen96, BDN95]. The precise relationships with these and other models defined in the literature e.g., [MP98, MP95, BG95, JJ95] requires further work.

In [CS00] we begin the study of three applications. Firstly, 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. We define the former precisely. Secondly, N -LTS (extended to allow communication of tuples and encrypted values) may provide a basis for proofs and model-checking of cryptographic protocols. In particular, it would support direct (i.e. not via a process calculus syntax) definitions of behaviours, as in [Pau98], while still allowing composition of these behaviours. Thirdly, developing work on secure encapsulation [SV99a, SV99b], quantifying over elements of the model, rather than over syntactic processes, would allow stronger security properties to be stated. We state conjectures relating the coloured π-calculus semantics – an approximate but simple notion of causality used there to state security properties – to N -LATS. We also wonder what the relationships are with the recent [GP99, FPT99, Hof99], 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. We have begun to consider, with Hyland, 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.

2. Background on the π-Calculus

Many variant π-calculi have been studied in the literature since the original was introduced in [MPW92]. 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; for lack of space also omitting 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 | P | Q | P + Q | τ.P | \overline{a}d.P | ac.P |!P
| (νc)P | [a = b]P | [a ≠ b]P .

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 presentational variant, explicitly-indexed, of the early labelled transition semantics of [San93, MPW93], 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 [Sew97, SV99a, SV99b]. 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 name-set associated with Q is then A∪fn(ℓ). 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 alphaconversion – 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 alphaequivalence 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 nameset – 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.

Out \overline{A ⊢ \overline{x}v.P ⟶^{\overline{x}v} P}  Par \frac{A ⊢ P ⟶^{ℓ} P′}{A ⊢ P | Q ⟶^{ℓ} P′ | Q}  Res \frac{A, x ⊢ P ⟶^{ℓ} P′ x ∉ fn(ℓ)}{A ⊢ (νx)P ⟶^{ℓ} (νx)P′}

In \overline{A ⊢ xp.P ⟶^{xv} \{^{v}/_{p}\}P} Com \frac{A ⊢ P ⟶^{\overline{x}v} P′ A ⊢ Q ⟶^{xv} Q′}{A ⊢ P | Q ⟶^{τ} (ν\{v\} \ A)(P′ | Q′)}  Open \frac{A, x ⊢ P ⟶^{\overline{y}x} P′ y ≠ x}{A ⊢ (νx)P ⟶^{\overline{y}x} P′}

Sum \frac{A ⊢ P ⟶^{ℓ} P′}{A ⊢ P + Q ⟶^{ℓ} 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. The rule for τ.P and symmetric versions of Par , Com and Sum are elided.

Figure 1. π operational semantics

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′ }.

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 the next section.

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

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 a function f : A → B and two names x ∉ A and y ∈ B, write [f, [y/x]] for the obvious copairing 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)⟩.

Definition 3.2 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.3 Define an Indexed Labelled Transition System (N -LTS) to be a structure

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

where ⟨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 (at least) 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 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.

In fact the definition contains some redundancy:

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

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,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 [Mil89]). When 2a,2b are omitted, 3b becomes essential.

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

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

Proposition 3.6 (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.

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

Weakening and Strengthening are immediate consequences of conditions 3a and 4. The converse of Shifting requires 2b, strengthening and 3a.

4. Alternative indexing structure

There are several alternative indexing structures – one simpler, with only injective renaming; one more elaborate, with data for restriction; and variants of all with a chosen new-name function. We discuss the 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. 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 - LTSs, not simply an N -LTS – to define [[xy.P]] one would need [[{^{z}/_{y}}P]] for all z. Moreover, we doubt whether an analogue of the input axioms 2a,2b could be stated. 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′) }. 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 chosen new version of N_{inj} is essentially the indexing structure used in [Sta96, FMS96, Hen96, CSW97].

5. Denotational semantics

We describe now operations on N -LTS that we will use in giving a compositional semantics to the π-calculus. In [CS00] we turn the class of N -LTS with initial name-set I into a category, N -LTS_{I}, in the obvious way. It is then straightforward to turn the operations below into functors, in fact into ω-continuous functors. The category N -LTS_{I} can be easily shown to have colimits of ω-chains, in fact to be cocomplete (and complete). Thus a semantics of recursively defined processes, such as replicated ones, can be obtained using least fixed points of ω-chains in the usual way. Lacking enough space to develop all of the above (or a more concrete definition for replication), we have decided in this extended abstract not to consider recursive processes at all.

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 5.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}.

The equivalence classes of ↔_{A} are analogous to alphaequivalence classes of terms w.r.t. renaming of names not in A. 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}}.

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 (see e.g. [MLM92]) N (I, −) which sends each name-set A to the set of functions (the morphisms in N) from I to A. Given a function g: A → B, N (I, g)(f : I → A) = gf. The new initial state is the identity on I, 1_{I} and each of its reindexings is given by the reindexing function itself. 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 no confusion arises, we will write l : U → U ⊎ V and r : V → U ⊎ V for the obvious left and right injections in their disjoint union. 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, i⟩⟩ and T_{k} = ⟨S_{k}: N → Set, ⟶_{k}, ⟨I, i_{k}⟩⟩ (for k = 1, 2) are N -LTSs. 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} l[t]_{↔_{A,z}}} x ≠ z

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{s ⟶^{ℓ} t}{ls ⟶′^{ℓ} lt} \frac{f : I → A}{⟨A, rf⟩ ⟶′^{\overline{f(x)}f(y)} ⟨A, lS(f)(i)⟩}

Define τ(T) similarly by labelling the transition in the first rule τ rather than \overline{f(x)}f(y).

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 deadlocked N -LTS with free names in I as 0_{I} = ⟨N (I, −), ∅, ⟨I, 1_{I}⟩⟩. Notice that 0_{I} is the initial object of the category N -LTS_{I} (see [CS00]).

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

⟨S + N (I, −) : N → Set, ⟶′, ⟨I, i⟩⟩ ,

where ⟶′ is defined by the following rules:

\frac{f : I → A  ⟨A, S(f)i⟩ ⟶^{ℓ} ⟨B, s⟩  f(x) = f(y)}{⟨A, rf⟩ ⟶′^{ℓ} ⟨B, 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 we assume the N -LTSs to be non-restarting, we can give a more standard definition which (pointwise) glues together the two (sets of) initial states; in this case the sum is the categorical coproduct [CS00].

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 5.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, ⟨i_{1}, 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 easy 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.

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 5.2 Define two N -LTSs T_{1} and T_{2} to be strongly bisimilar if the LTS ⟨S_{1}, ⟶_{1}, ⟨I, i_{1}⟩⟩ and ⟨S_{2}, ⟶_{2}, ⟨I, i_{2}⟩⟩ are bisimilar in the usual sense of Milner [Mil89]. Say that they are strongly equivalent if, for every f : I → A the N -LTSs ⟨S_{1}, ⟶_{1}, ⟨A, S_{1}(f)i_{1}⟩⟩ and ⟨S_{2}, ⟶_{2}, ⟨A, S_{2}(f)i_{2}⟩⟩ are strongly bisimilar.

Weak bisimilarity and equivalence are defined similarly.

Exploiting the indexing structure even more, notice that if a bisimulation is further required to be a relation between S_{1} and S_{2} in the categorical sense, i.e. a subobject of the product S_{1}×S_{2}, one obtains an open bisimulation [San96b].

Compositional semantics to π-terms is given using the operations defined above in the obvious way. For a process term P, with free names in I, we write [[P]]_{I} for the corresponding N -LTS. We conclude this section by stating the result which relates bisimulation in the model with early bisimulation in the operational semantics.

Theorem 5.3 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}.

Proof:[Sketch] First of all observe that the operational semantics naturally induces for every process term P, with free names in I, an N -LTS

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

where π(A) = {Q | Q is a π-term and fn(Q) ⊆ A}, π(f) simply relabels processes according to f, and there is a transition ⟨A, P ⟩ ⟶^{ℓ} ⟨B, Q⟩ if A ⊢ P ⟶^{ℓ} Q (according to the operational semantics) and B = A ∪ fn(ℓ). One can then prove by structural induction that ([P])_{I} is open bisimilar (cf. the remark after Definition 5.2) to [[P]]_{I}. The theorem is now an easy consequence of this last statement.

6. N -LATS

In this section we define a class of causal models by smoothly lifting the notion of labelled asynchronous^{1} transition system [Bed88, Shi85, WN95] (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 6.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

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

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

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

where ⟨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, i⟩⟩ is a transition system

according to Definition 3.3, 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 [Bed88, WN95]). 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 6.3 For every run r

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(r)_{I} = ⟨[n], ⊴_{I}^{r}, l^{r}⟩, where

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

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

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

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

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

Definition 6.4 Let T_{1} and T_{2} be two N -LATSs with initial name-set I and let Run(T_{i}) (for i = 1, 2) be the corresponding sets of runs. A relation B ⊆ Run(T_{1}) × Run(T_{2}) is an history preserving bisimulation (hpb) if it satisfies the following conditions

1. ⟨I ⊢ ⟨I, i_{1}⟩, I ⊢ ⟨I, i_{2}⟩⟩ ∈ B 2. ⟨r_{1}, r_{2}⟩ ∈ B implies

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

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

(b) if r′_{1} extends r_{1} with a transition s_{n}⟶_{1}_{e_{n+1}}^{ℓ_{n+1}}s_{n+1}

then there exists a run r′_{2} which extends r_{2} with a

transition s̄_{n}⟶_{2}_{ē_{n+1}}^{ℓ_{n+1}}s̄_{n+1} such that ⟨r′_{1}, r′_{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(r_{1})_{ID} = po(r_{2})_{ID}.

The constructions of Section 5 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 rules 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 then 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 [BS98]. In particular we present correspondence results relating our hbp semantics to causal bisimulation, and further discuss name-dependency.

In the paper [BS98], no notion of strong bisimulation is defined. The authors in fact defined directly causal bisimulation in the weak, i.e. abstracting away from τ actions, form. 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, and not their effect only, visible. We will in fact do both, ending up with two correspondence results, one for strong and one for weak bisimulation. Due to space constraints we cannot report the definition of causal bisimulation here and therefore refer to loc. cit. for definitions and discussions of the relevance of their approach. We simply mention here, using their notation, what modifications are needed in order to define strong causal bisimulation.

Definition 6.5 An operational semantics for strong causal bisimulation is obtained by modifying the definition of [BS98, table 3, page 365] in the rules which derive silent actions in the following way:

T-pre, T-sum, T-par, T-res, T-cau, T-rep: These are all subsumed in the homologous rules, out, sum, par, res, cau, rep, respectively, which were originally defined for non-τ actions.

com: This is changed as follows (recall that we are dealing with the monadic π-calculus):

\frac{A_{1} ⟶_{K_{1}:k}^{(νz)\overline{x}y}A′_{1} A_{2}⟶_{K_{2}:k}^{xy}A′_{2}}{A_{1} | A_{2} ⟶_{K_{1}∪K_{2}:k}^{τ}(νz)(A′_{1}[k ⇝ (K_{2}, k)] | A′_{2}[k ⇝ (K_{1}, k)])}

with conditions z ∉ fn(A_{2}) and k ∉ K(A_{1}, A_{2}).^{2}

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. We can now state our first noninterleaving correspondence result:

Theorem 6.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.

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

Definition 6.7 Let r be a run in an asynchronous transition system, let n be the length of r and let n^{τ} be the number of transitions in r 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 r has label ℓ_{h} ≠ τ; n_{j+1} is the smallest number h such that the h-th transition of r has label ℓ_{h} ≠ τ and that moreover is strictly bigger than n_{j}.

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

2In [BS98] the notation (νz)\overline{x}y is employed for possibly-bound outputs.

Definition 6.8 Let r be a run of an N -LATS and let po(r)_{I} and po(r)_{ID} be the corresponding partial orders as in Definition 6.3. Define po(r)_{wI} and po(r)_{wID} to be the partial orders ⟨[n^{τ}], ⊴_{wI}, l_{w}^{r}⟩ and ⟨[n^{τ}], ⊴_{wID}, l_{w}^{r}⟩, respectively, where l_{w}^{r}(i) = l^{r}(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 6.4 but where, as usual, “strong” transitions s_{1}⟶_{1}_{e_{1}}^{ℓ}t_{1} are simulated by

“weak” ones s_{2} ⟹_{2}_{e_{2}}^{ℓ̂} t_{2} (and symmetrically) and with con-

dition 2(a) replaced by po(r)_{wI} = po(r′)_{wI} or by po(r)_{wID} = po(r′)_{wID}, for the name-dependency aware case. We can then prove the following result:

Theorem 6.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 [BS98].

In [BS98] 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 [JJ95], 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 [DP99], 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 6.10 If two asynchronous transition systems are history preserving bisimilar than they are namedependency aware history preserving bisimilar.

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

References

[BC88] G. Boudol and I. Castellani. Permutation of transitions: an event structure semantics for CCS and SCCS. In Proceedings of REX School/Workshop, volume 354 of LNCS, pages 411–427, 1988.

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

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

[BG95] N. Busi and R. Gorrieri. A petri net semantics for πcalculus. In Proceedings of CONCUR’95, volume 962 of LNCS, pages 145–159, 1995.

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

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

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

[CS00] G. L. Cattani and P. Sewell. Models for namepassing processes: Interleaving and causal. Technical report, Cambridge University Computer Laboratory, 2000.

[CSW97] G. L. Cattani, I. Stark, and G. Winskel. Presheaf models for the π-calculus. In Proceedings of CTCS’97, volume 1290 of LNCS, pages 106–126, 1997.

[CW97] G. L. Cattani and G. Winskel. Presheaf models for concurrency. In Proceedings of CSL’96, volume 1258 of LNCS, pages 58–75, 1997.

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

[DD89] Ph. Darondeau and P. Degano. Causal trees. In Proceedings of ICALP’89, volume 372 of LNCS, pages 234–248, 1989.

[DDNM88a] P. Degano, R. De Nicola, and U. Montanari. On the consistency of “truly concurrent” operational and denotational semantics (extended abstract). In Proceedings of LICS’88, pages 133–141. IEEE, 1988.

[DDNM88b] P. Degano, R. De Nicola, and U. Montanari. Partial orderings descriptions and observations of nondeterministic concurrent processes. In Proceedings of REX School/Workshop, volume 354 of LNCS, pages 438–496, 1988.

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

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

[FMS96] M. P. Fiore, E. Moggi, and D. Sangiorgi. A fullyabstract model for the π-calculus (extended abstract). In Proceedings of LICS’96, pages 43–54. IEEE, 1996.

[FPT99] M. P. Fiore, G. D. Plotkin, and D. Turi. Abstract syntax and variable binding. In Proceedings of LICS’99, pages 193–202. IEEE, 1999.

[GG89] R. van Glabbeek and U. Goltz. Equivalence notions for concurrent systems and refinement of actions. In Proceedings of MFCS’89, volume 379 of LNCS, pages 237–248, 1989.

[GP99] M. Gabbay and A. Pitts. A new approach to abstract syntax involving binders. In Proceedings of LICS’99, pages 214–224. IEEE, 1999.

[Hen96] 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.

[Hof99] M. Hofmann. Semantical analysis of higher-order abstract syntax. In Proceedings of LICS’99, pages 204–213. IEEE, 1999.

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

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

1999.

[HT91] K. Honda and M. Tokoro. An object calculus for asynchronous communication. In Proceedings of ECOOP’91, volume 512 of LNCS, pages 133–147, 1991.

[JJ95] L. J. Jagadeesan and R. Jagadeesan. Causality and true concurrency: A data-flow analysis of the picalculus (extended abstract). In Proceedings of AMAST’95, volume 936 of LNCS, pages 277–291, 1995.

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

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

[Mil89] R. Milner. Communication and Concurrency. Prentice Hall, 1989.

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

[MP95] U. Montanari and M. Pistore. Concurrent semantics for the π-calculus. In Proceedings of MFPS XI, volume 1 of ENTCS, pages 337–356. Elsevier, 1995.

[MP98] U. Montanari and M. Pistore. An introduction to history dependent automata. In Second Workshop on Higher-Order Operational Techniques in Semantics (HOOTS II), volume 10 of ENTCS. Elsevier, 1998.

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

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

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

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

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

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

[San96b] D. Sangiorgi. A theory of bisimulation for the πcalculus. Acta Informatica, 33(1):69–97, 1996.

[Sel97] P. Selinger. First order axioms for asynchrony. In Proceedings of CONCUR’97, volume 1243 of LNCS, pages 376–390, 1997.

[Sew97] P. Sewell. On implementations and semantics of a concurrent programming language. In Proceedings of CONCUR’97, volume 1243 of LNCS, pages 391– 405, 1997.

[Sew00] P. Sewell. Pi calculi. In H. Bowman and J. Derrick, editors, Formal Methods for Distributed Processing, An Object Oriented Approach. CUP, 2000. To appear.

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

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

[Sta96] I. Stark. A fully abstract domain model for the πcalculus. In Proceedings of LICS’96, pages 36–42. IEEE, 1996.

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

[SV99b] P. Sewell and J. Vitek. Secure composition of untrusted code: Wrappers and causality types. Technical Report 478, Computer Laboratory, University of Cambridge, 1999. To appear in Proceedings of the 13th IEEE Computer Security Foundations Workshop.

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

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