On Hierarchical Communication Topologies in
the π-calculus
Emanuele D’Osualdo1 and C.-H. Luke Ong2

arXiv:1601.01725v2 [] 19 Apr 2016

1

TU Kaiserslautern dosualdo@cs.uni-kl.de
2
University of Oxford lo@cs.ox.ac.uk

Abstract. This paper is concerned with the shape invariants satisfied
by the communication topology of π-terms, and the automatic inference
of these invariants. A π-term P is hierarchical if there is a finite forest
T such that the communication topology of every term reachable from
P satisfies a T-shaped invariant. We design a static analysis to prove a
term hierarchical by means of a novel type system that enjoys decidable
inference. The soundness proof of the type system employs a non-standard
view of π-calculus reactions. The coverability problem for hierarchical
terms is decidable. This is proved by showing that every hierarchical term
is depth-bounded, an undecidable property known in the literature. We
thus obtain an expressive static fragment of the π-calculus with decidable
safety verification problems.

1

Introduction

Concurrency is pervasive in computing. A standard approach is to organise concurrent software systems as a dynamic collection of processes that communicate
by message passing. Because processes may be destroyed or created, the number
of processes in the system changes in the course of the computation, and may
be unbounded. Moreover the messages that are exchanged may contain process
addresses. Consequently the communication topology of the system—the hypergraph [19, 18] connecting processes that can communicate directly—evolves over
time. In particular, the connectivity of a process (i.e. its neighbourhood in this
hypergraph) can change dynamically. The design and analysis of these systems
is difficult: the dynamic reconfigurability alone renders verification problems
undecidable. This paper is concerned with hierarchical systems, a new subclass of
concurrent message-passing systems that enjoys decidability of safety verification
problems, thanks to a shape constraint on the communication topology.
The π-calculus of Milner, Parrow and Walker [19] is a process calculus designed
to model systems with a dynamic communication topology. In the π-calculus,
processes can be spawned dynamically, and they communicate by exchanging
messages along synchronous channels. Furthermore channel names can themselves
be created dynamically, and passed as messages, a salient feature known as
mobility, as this enables processes to modify their neighbourhood at runtime.
It is well known that the π-calculus is a Turing-complete model of computation.
Verification problems on π-terms are therefore undecidable in general. There are

2

E. D’Osualdo and C.-H. L. Ong

however useful fragments of the calculus that support automatic verification. The
most expressive such fragment known to date is the depth-bounded π-calculus of
Meyer [12]. Depth boundedness is a constraint on the shape of communication
topologies. A π-term is depth-bounded if there is a number k such that every
simple path3 in the communication topology of every reachable π-term has length
bounded by k. Meyer [14] proved that termination and coverability (a class of
safety properties) are decidable for depth-bounded terms.
Unfortunately depth boundedness itself is an undecidable property [14], which
is a serious impediment to the practical application of the depth-bounded fragment to verification. This paper offers a two-step approach to this problem.
First we identify a (still undecidable) subclass of depth-bounded systems, called
hierarchical, by a shape constraint on communication topologies (as opposed to
numeric, as in the case of depth-boundedness). Secondly, by exploiting this richer
structure, we define a type system, which in turn gives a static characterisation of
an expressive and practically relevant fragment of the depth-bounded π-calculus.
Example 1 (Client-server pattern). To illustrate our approach, consider a simple
system implementing a client-server pattern. A server S is a process listening on
a channel s which acts as its address. A client C knows the address of a server
and has a private channel c that represents its identity. When the client wants
to communicate with the server, it asynchronously sends c along the channel s.
Upon receipt of the message, the server acquires knowledge of (the address of)
the requesting client; and spawns a process A to answer the client’s request R
asynchronously; the answer consists of a new piece of data, represented by a new
name d, sent along the channel c. Then the server forgets the identity of the
client and reverts to listening for new requests. Since only the requesting client
knows c at this point, the server’s answer can only be received by the correct
client. Figure 1a shows the communication topology of a server and a client, in
the three phases of the protocol.
The overall system is composed of an unbounded number of servers and
clients, constructed according to the above protocol. The topology of a reachable
configuration is depicted in Fig. 1b. While in general the topology of a mobile
system can become arbitrarily complex, for such common patterns as client-server,
the programmer often has a clear idea of the desired shape of the communication
topology: there will be a number of servers, each with its cluster of clients; each
client may in turn be waiting to receive a number of private replies. This suggests
a hierarchical relationship between the names representing servers, clients and
data, although the communication topology itself does not form a tree.
T-compatibility and hierarchical terms Recall that in the π-calculus there
is an important relation between terms, ≡, called structural congruence, which
equates terms that differ only in irrelevant presentation details, but not in
behaviour. For instance, the structural congruence laws for restriction tell us that
the order of restrictions is irrelevant—νx.νy.P ≡ νy.νx.P —and that the scope
3

a simple path is a path with no repeating edges.

On Hierarchical Communication Topologies in the π-calculus

S

s

C

d

c

s

C

cc
c

cc c
c

C
C
C

R

→
S

s

S
C

c

d
d

→
S

3

A

(a) the protocol

d

c

C
C
C

s

A

c

···

C d ··· d

C
C
C
R
R
R

s

A
A
A

A

C d ··· d
A

A

c
cc

(b) a reachable configuration

(c) forest representation

Fig. 1. Evolution of the communication topology of a server interacting with a client.
R represents a client’s pending request and A a server’s pending answer.

of a restriction can be extended to processes that do not refer to the restricted
name—i.e., (νx.P ) k Q ≡ νx.(P k Q) when x does not occur free in Q—without
altering the meaning of the term. The former law is called exchange, the latter is
called scope extrusion.
Our first contribution is a formalisation in the π-calculus of the intuitive
notion of hierarchy illustrated in Example 1. We shall often speak of the forest
representation of a π-term P , forest(P ), which is a version of the abstract syntax
tree of P that captures the nesting relationship between the active restrictions
of the term. (A restriction of a π-term is active if it is not in the scope of a
prefix.) Thus the internal nodes of a forest representation are labelled with
(active) restriction names, and its leaf nodes are labelled with the sequential
subterms. Given a π-term P , we are interested in not just forest(P ), but also
forest(P 0 ) where P 0 ranges over the structural congruents of P , because these
are all behaviourally equivalent representations. See Fig. 4 for an example of
the respective forest representations of the structural congruents of a term. In
our setting a hierarchy T is a finite forest of what we call base types. Given
a finite forest T , we say that a term P is T-compatible if there is a term P 0 ,
which is structurally congruent to P , such that the parent relation of forest(P 0 )
is consistent with the partial order of T .
In Example 1 we would introduce base types srv, cl and data associated with
the restrictions νs, νc and νd respectively, and we would like the system to be
compatible to the hierarchy T = srv  cl  data, where  is the is-parent-of
relation. That is, we must be able to represent a configuration with a forest that,
for instance, does not place a server name below a client name nor a client name
below another client name. Such a representation is shown in Fig. 1c.
In the Example, we want every reachable configuration of the system to be
compatible with the hierarchy. We say that a π-term P is hierarchical if there is
a hierarchy T such that every term reachable from P is T-compatible. Thus the
hierarchy T is a shape invariant of the communication topology under reduction.

4

E. D’Osualdo and C.-H. L. Ong
a
b

S

a
b

≡
R

S

a
b

→
R

S0

R0

Fig. 2. Standard view of π-calculus reactions

It is instructive to express depth boundedness as a constraint on forest
representation: a term P is depth-bounded if there is a constant k such that
every term reachable from P has a structurally congruent P 0 whereby forest(P 0 )
has height bounded by k. It is straightforward to see that hierarchical terms are
depth-bounded; the converse is however not true.
A type system for hierarchical terms While membership of the hierarchical
fragment is undecidable, by exploiting the forest structure, we have devised
a novel type system that guarantees the invariance of T-compatibility under
reduction. Furthermore type inference is decidable, so that the type system can
be used to infer a hierarchy T with respect to which the input term is hierarchical.
To the best of our knowledge, our type system is the first that can infer a shape
invariant of the communication topology of a system.
The typing rules that ensure invariance of T-compatibility under reduction
arise from a new perspective of the π-calculus reaction, one that allows compatibility to a given hierarchy to be tracked more readily. Suppose we are presented
with a T-compatible term P = C[S, R] where C[-, -] is the reaction context, and
the two processes S = ahbi.S 0 and R = a(x).R0 are ready to communicate over
a channel a. After sending the message b, S continues as the process S 0 , while
upon receipt of b, R binds x to b and continues as R00 = R0 [ b/x ]. Schematically,
the traditional understanding of this transaction is: first extrude the scope of b
to include R, then let them react, as shown in Fig. 2.
Instead, we seek to implement the reaction without scope extrusion: after the
message is transmitted, the sender continues in-place as S 0 , while R00 is split in
0
0
two parts Rmig
k R¬mig
, one that uses the message (the migratable part) and one
0
that does not. As shown in Fig. 3, the migratable part of R00 , Rmig
, is “installed”
under b so that it can make use of the acquired name, while the non-migratable
0
one, R¬mig
, can simply continue in-place.
Crucially, the reaction context, C[-, -], is left unchanged. This means that if the
starting term is T-compatible, the reaction context of the reactum is T-compatible
as well. We can then focus on imposing constraints on the use of names of R0
0
so that the migration does not result in Rmig
escaping the scope of previously
bound names.
By using these ideas, our type system is able to statically accept π-calculus
encodings of such system as that discussed in Example 1. The type system can
be used, not just to check that a given T is respected by the behaviour of a
term, but also to infer a suitable T when it exists. Once typability of a term

On Hierarchical Communication Topologies in the π-calculus
a

a

→

b

S

5

R

b
R0
S 0 mig

R0
¬mig

Fig. 3. T-compatibility preserving reaction

is established, safety properties such as unreachability of error states, mutual
exclusion or bounds on mailboxes, can be verified algorithmically. For instance, in
Example 1, a coverability check can prove that each client can have at most one
reply pending in its mailbox. To prove such a property, one needs to construct an
argument that reasons about dynamically created names with a high degree of
precision. This is something that counter abstraction and uniform abstractions
based methods have great difficulty attaining.
Our type system is (necessarily) incomplete in that there are depth-bounded,
or even hierarchical, systems that cannot be typed. The class of π-terms that
can be typed is non-trivial, and includes terms which generate an unbounded
number of names and exhibit mobility.
Outline. In Section 2 we review the π-calculus, depth-bounded terms, and
related technical preliminaries. In Section 3 we introduce T-compatibility and the
hierarchical terms. We present our type system in Section 4. Section 5 discusses
soundness of the type system. In Section 6 we give a type inference algorithm;
and in Section 7 we present results on expressivity and discuss applications. We
conclude with related and future work in Sections 8 and 9. All missing definitions
and proofs can be found in Appendix.

2
2.1

The π-calculus and the depth-bounded fragment
Syntax and semantics

We use a π-calculus with guarded replication to express recursion [16]. Fix a
universe N of names representing channels and messages. The syntax is defined
by the grammar:
P 3 P, Q ::= 0 | νx.P | P1 k P2 | M | !M
M ::= M + M | π.P

π ::= a(x) | ahbi | τ

process
choice
prefix

Definition 1. Structural congruence, ≡, is the least relation that respects αconversion of bound names, and is associative and commutative with respect to +

6

E. D’Osualdo and C.-H. L. Ong

(choice) and k (parallel composition) with 0 as the neutral element, and satisfies
laws for restriction: νa.0 ≡ 0 and νa.νb.P ≡ νb.νa.P , and
!P ≡ P k !P

P k νa.Q ≡ νa.(P k Q)

Replication
(if a 6∈ fn(P ))

Scope Extrusion

In P = π.Q, we call Q the continuation of P and will often omit Q altogether
when Q = 0. In a term νx.P we will occasionally refer to P as the scope of x. The
name x is bound in both νx.P , and in a(x).P . We will write fn(P ), bn(P ) and
bnν (P ) for the set of free, bound and restriction-bound names in P , respectively.
A sub-term is active if it is not under a prefix. A name is active when it is bound
by an active restriction. We write actν (P ) for the set of active names of P . Terms
of the form M and !M are called sequential. We write S for the set of sequential
terms, actS (P ) for the set of active sequential processes of P , and P i for the
parallel composition of i copies of P .
Intuitively, a sequential process acts like a thread running finite-control
sequential code. A term τ .(P k Q) is the equivalent of spawning a process
Q and continuing as P —although in this context the rôles of P and Q are
interchangeable. Interaction is by synchronous communication over channels.
An input prefix a(x) is a blocking receive on the channel a binding the variable
x to the message. An output prefix ahbi is a blocking send of the message b
along the channel a; here b is itself the name of a channel that can be used
subsequently for further communication: an essential feature for mobility. A
non-blocking send can be simulated by spawning a new process doing a blocking
send. Restrictions are used to make a channel name private. A replication !(π.P )
can be understood as having a server that can spawn a new copy of P whenever
a process tries to communicate with it. In other words it behaves like an infinite
parallel composition (π.P k π.P k · · · ).
For conciseness, we assume channels are unary (the extension to the polyadic
case is straightforward). In contrast to process calculi without mobility, replication
and systems of tail recursive equations are equivalent methods of defining recursive
processes in the π-calculus [17, Section 3.1].
We rely on the following mild assumption, that the choice of names is unambiguous, especially when selecting a representative for a congruence class:
Name Uniqueness Assumption. Each name in P is bound at most once and
fn(P ) ∩ bn(P ) = ∅.
Normal Form. The notion of hierarchy, which is central to this paper, and
the associated type system depend heavily on structural congruence. These are
criteria that, given a structure on names, require the existence of a specific
representative of the structural congruence class exhibiting certain properties.
However, we cannot assume the input term is presented as that representative;
even worse, when the structure on names is not fixed (for example, when inferring
types) we cannot fix a representative and be sure that it will witness the desired
properties. Thus, in both the semantics and the type system, we manipulate

On Hierarchical Communication Topologies in the π-calculus

7

a neutral type of representative called normal form, which is a variant of the
standard form [19]. In this way we are not distracted by the particular syntactic
representation we are presented with.
We say that a term P is in normal form (P ∈ Pnf ) if it is in standard form
and each of its inactive subterms is also in normal form. Formally, normal forms
are defined by the grammar
Pnf 3 N ::= νx1 . · · · νxn .(A1 k · · · k Am )

A ::= π1 .N1 + · · · + πn .Nn | !(π1 .N1 + · · · + πn .Nn )

where the sequences x1 . . . xn and A1 . . . Am may be empty; when they are both
empty the normal form is the term 0. We further assume w.l.o.g. that normal
forms Q
satisfy Name Uniqueness. Given a finite set of indexes I = {i1 , P
. . . , in } we
write i∈I Ai for (Ai1 k · · · k Ain ), which is 0 when I is empty; and i∈I πi .Ni
for (πi1 .Ni1 + · · · + πin .Nin ). This notation is justified by commutativity and
associativity of the parallel and choice operators. Thanks to the structural laws
of restriction, we also write νX.P where X = {x1 , . . . , xn }, or νx1 x2 · · · xn .P ,
for νx1 . · · · νxn .P ; or just P when X is empty. When X and Y are disjoint sets
of names, we use juxtaposition for union.
Every process P ∈ P is structurally congruent to a process in normal form. The
function nf : P → Pnf , defined in Appendix, extracts, from a term, a structurally
congruent normal form.
Q
Given a process P with normal form νX. i∈I Ai , the communication topology 4
of P , written GJP K, is defined as the labelled hypergraph with X as hyperedges
and I as nodes, each labelled with the corresponding Ai . An hyperedge x ∈ X is
connected with i just if x ∈ fn(Ai ).
Semantics. We are interested in the reduction semantics of a π-term, which can
be described using the following rule.
Definition 2 (Semantics of π-calculus). The operational semantics of a term
P0 ∈ P is defined by the (pointed) transition system (P, →, P0 ) on π-terms, where
P0 is the initial term, and the transition relation, → ⊆ P 2 , is defined by P → Q
if either (i) to (iv) hold, or (v) and (vi) hold, where
(i)
(ii)
(iii)
(iv)

P ≡ νW.(S k R k C) ∈ Pnf ,
S = (ahbi.νYs .S 0 ) + Ms ,
R = (a(x).νYr .R0 ) + Mr ,
Q ≡ νW Ys Yr .(S 0 k R0 [ b/x ] k C),

(v) P ≡ νW.(τ .νY.P 0 k C) ∈ Pnf ,
(vi) Q ≡ νW Y.(P 0 k C).

We define the set of reachable terms from P as Reach(P ) := { Q | P →∗ Q },
writing →∗ to mean the reflexive, transitive closure of →. We refer to the
restrictions, νYs , νYr and νY , as the restrictions activated by the transition
P → Q.
Notice that the use of structural congruence in the definition of → takes unfolding
replication into account.
4

This definition arises from the “flow graphs” of [19]; see e.g. [14, p. 175] for a formal
definition.

8

E. D’Osualdo and C.-H. L. Ong

Example 2 (Client-server). We can model a variation of the client-server pattern
sketched in the introduction, with the term νs c.P where P = !S k !C k !M ,
S = s(x).νd.xhdi, C = c(m).(shmi k m(y).chmi) and M = τ .νm.chmi. The term
!S represents a server listening to a port s for a client’s requests. A request is a
channel x that the client sends to the server for exchanging the response. After
receiving x the server creates a new name d and sends it over x. The term !M
creates unboundedly many clients, each with its own private mailbox m. A client
on a mailbox m repeatedly sends requests to the server and concurrently waits
for the answer on the mailbox before recursing.
In the following examples, we use CCS-style nullary channels, which can be
understood as a shorthand: c.P := c(x).P and c.P := νx.chxi.P where x 6∈ fn(P ).
Example 3 (Resettable counter). A counter with reset is a process reacting to
messages on three channels inc, dec and rst. An inc message increases the value
of the counter, a dec message decreases it or causes a deadlock if the counter is
zero, and a rst message resets the counter to zero. This behaviour is exhibited

by the process Ci = ! pi (t). inc i .(t k pi hti) + dec i .(t.pi hti) + rst i .(νt0i .pi ht0i i) .
Here, the number of processes t in parallel with pi hti represents the current
 value
of the counter i. A system νp1 t1 .(C1 k p1 ht1 i) k νp2 t2 .(C2 k p2 ht2 i) can for
instance simulate a two-counter machine when put in parallel with a finite control
process sending signals along the channels inc i , dec i and rst i .
Example 4 (Unbounded ring). Let R = νm.νs0 .(M k mhs0 i k s0 ), S = !(s.n)
and M = ! m(n).s0 .νs.(S k mhsi k s) . The term R implements an unboundedly
growing ring. It initialises the ring with a single “master” node pointing at
itself (s0 ) as the next in the ring. The term M , implementing the master node’s
behaviour, waits on s0 and reacts to a signal by creating a new slave with address
s connected with the previous next slave n. A slave S simply propagates the
signals on its channel to the next in the ring.
2.2

Forest representation of terms

In the technical developement of our ideas, we will manipulate the structure of
terms in non-trivial ways. When reasoning about these manipulations, a term is
best viewed as a forest representing (the relevant part of) its abstract syntax tree.
Since we only aim to capture the active portion of the term, the active sequential
subterms are the leaves of its forest view. Parallel composition corresponds to
(unordered) branching, and names introduced by restriction are represented by
internal (non-leaf) nodes.
A forest is a simple, acyclic, directed graph, f = (Nf , f ), where the edge
relation n1 f n2 means “n1 is the parent of n2 ”. We write ≤f and <f for
the reflexive transitive and the transitive closure of f respectively. A path is a
sequence of nodes, n1 . . . nk , such that for each i < k, ni f ni+1 . Henceforth
we drop the subscript f from f , ≤f and <f (as there is no risk of confusion),
and assume that all forests are finite. Thus every node has a unique path to a
root (and that root is unique).

On Hierarchical Communication Topologies in the π-calculus
1

2

a

3

c
a

b
c

A1

A1 A2 A3 A4

b

A3

A2 A4

a

4

A1

b

A1

A2

c

A4

a

c

b

A3

A2 A4

5
A2

9

b

c

a

A3

A1 A4

A3

Fig. 4. Examples of forests in FJP K where P = νa b c.(A1 k A2 k A3 k A4 ), A1 = a(x),
A2 = b(x), A3 = c(x) and A4 = ahbi.

An L-labelled forest is a pair ϕ = (fϕ , `ϕ ) where fϕ is a forest and `ϕ : Nϕ → L
is a labelling function on nodes. Given a path n1 . . . nk of fϕ , its trace is the
induced sequence `ϕ (n1 ) . . . `ϕ (nk ). By abuse of language, a trace is an element
of L∗ which is the trace of some path in the forest.
We define L-labelled forests inductively from the empty forest (∅, ∅). We write
ϕ1 ] ϕ2 for the disjoint union of forests ϕ1 and ϕ2 , and l[ϕ] for the forest with a
single root, which is labelled with l ∈ L, and whose children are the respective
roots of the forest ϕ. Since the choice of the set of nodes is irrelevant, we will
always interpret equality between forests up to isomorphism (i.e. a bijection on
nodes respecting parent and labeling).
Definition 3 (Forest representation). We represent the structural congruence class of a term P ∈ P with the set of labelled forests FJP K := {forest(Q) |
Q ≡ P } with labels in actν (P ) ] actS (P ) where forest(Q) is defined as

(∅, ∅)



Q[(∅, ∅)]
forest(Q) :=

x[forest(Q0 )]



forest(Q1 ) ] forest(Q2 )

if
if
if
if

Q=0
Q is sequential
Q = νx.Q0
Q = Q1 k Q2

Note that leaves (and only leaves) are labelled with sequential processes.
The restriction height, heightν (forest(P )), is the length of the longest path
formed of nodes labelled with names in forest(P ).
In Fig. 4 we show some of the possible forest representations of an example term.
2.3

Depth-bounded terms

Definition 4 (Depth-bounded term [12]). The nesting of restrictions of a
term is given by the function
nestν (M ) := nestν (!M ) := nestν (0) := 0
nestν (νx.P ) := 1 + nestν (P )
nestν (P k Q) := max(nestν (P ), nestν (Q)).

10

E. D’Osualdo and C.-H. L. Ong

The depth of a term is defined as the minimal nesting of restrictions in its
congruence class, depth(P ) := min {nestν (Q) | P ≡ Q}. A term P ∈ P is depthbounded if there exists k ∈ N such that for each Q ∈ Reach(P ), depth(Q) ≤ k.
We write Pdb for the set of terms with bounded depth.
Notice that nestν is not an invariant of structural congruence, whereas depth
and depth-boundedness are.
Example 5. Consider the congruent terms P and Q


P = νa.νb.νc. a(x) k bhci k c(y) ≡ νa.a(x) k νc. (νb.bhci) k c(y) = Q
We have nestν (P ) = 3 and nestν (Q) = 2; but depth(P ) = depth(Q) = 2.
It is straightforward to see that the nesting of restrictions of a term coincides
with the height of its forest representation, i.e., for every P ∈ P, nestν (P ) =
heightν (forest(P )).
Example 6 (Depth-bounded term). The term in Example 2 is depth-bounded: all
the reachable terms are congruent to terms of the form

Qijk = νs c. P k N i k Req j k Ans k
for some i, j, k ∈ N where N = νm.chmi, Req = νm.(shmi k m(y).chmi) and
Ans = νm.(νd.mhdi k m(y).chmi). For any i, j, k, nestν (Qijk ) ≤ 4.
Example 7 (Depth-unbounded term). Consider the term in Example 4 and the
following run:
R →∗ νm s0 .(M k νs1 .(!(s1 .s0 ) k mhs1 i k s1 ))

→∗ νm s0 .(M k νs1 .(!(s1 .s0 ) k νs2 .(!(s2 .s1 ) k mhs2 i k s2 ))) →∗ . . .

The scopes of s0 , s1 , s2 and the rest of the instantiations of νs are inextricably
nested, thus R has unbounded depth: for each n ≥ 1, a term with depth n is
reachable.
Depth boundedness is a semantic notion. Because the definition is a universal
quantification over reachable terms, analysis of depth boundedness is difficult.
Indeed the membership problem is undecidable [14]. In the communication
topology interpretation, depth has a tight relationship with the maximum length
of the simple paths. A path v1 e1 v2 . . . vn en vn+1 in GJP K is simple if it does not
repeat hyper-edges, i.e., ei =
6 ej for all i 6= j. A term is depth-bounded if and only
if there exists a bound on the length of the simple paths of the communication
topology of each reachable term [12]. This allows terms to grow unboundedly in
breadth, i.e., the degree of hyper-edges in the communication topology.
Q
A term P is Q
embeddable in a term Q, written P  Q, if P ≡ νX. i∈I Ai ∈ Pnf
and Q ≡ νXY.( i∈I Ai k R) ∈ Pnf for some term R. In [12] the term embedding
ordering, , is shown to be both a simulation relation on π-terms, and an effective
well-quasi ordering on depth-bounded terms. This makes the transition system
(Reach(P )/≡ , →/≡ , P ) a well-structured transition system (WSTS) [7, 1] under
the term embedding ordering. Consequently a number of verification problems
are decidable for terms in Pdb .

On Hierarchical Communication Topologies in the π-calculus

11

Theorem 1 (Decidability of termination [12]). The termination problem
for depth-bounded terms, which asks, given a term P0 ∈ Pdb , if there is an infinite
sequence P0 → P1 → . . ., is decidable.
Theorem 2 (Decidability of coverability [12, 24]). The coverability problem for depth-bounded terms, which asks, given a term P ∈ Pdb and a query
Q ∈ P, if there exists P 0 ∈ Reach(P ) such that Q  P 0 , is decidable.

3

T-compatibility and hierarchical terms

A hierarchy is specified by a finite forest (T , ). In order to formally relate active
restrictions in a term to nodes of the hierarchy T , we annotate restrictions with
types. For the moment we view types abstractly as elements of a set T, equipped
with a map base : T → T . An annotated restriction ν(x : τ ) where τ ∈ T will be
associated with the node base(τ ) in the hierarchy T . Elements of T are called
types, and those of T are called base types. In the simplest case and, especially for
Section 3, we may assume T = T and base(t) = t. In Section 4 we will consider a
set T of types generated from T , and a non-trivial base map.
Definition 5 (Annotated term). A T-annotated π-term (or simply annotated
π-term) P ∈ P T has the same syntax as ordinary π-terms except that restrictions
take the form ν(x : τ ) where τ ∈ T. In the abbreviated form νX, X is a set of
annotated names (x : τ ).
Structural congruence, ≡, of annotated terms, is defined by Definition 1, with
the proviso that the type annotations are invariant under α-conversion and
replication. For example, ! π.ν(x : τ ).P ≡ π.ν(x : τ ).P k ! π.ν(x : τ ).P and
ν(x : τ ).P ≡ ν(y : τ ).P [ y/x ]; observe that the annotated restrictions that occur
in a replication unfolding are necessarily inactive.
The forest representation of an annotated π-term is obtained from Definition 3
by replacing the case of Q = ν(x : τ ).Q0 by
forest(ν(x : τ ).Q0 ) := (x, t)[forest(Q0 )]
where base(τ ) = t. Thus the forests in FJP K have labels in (actν (P )×T )]actS (P ).
We write FT for the set of forests with labels in (N × T ) ] S. We write PnfT for
the set of T-annotated π-terms in normal form.
The definition of the transition relation of annotated terms, P → Q, is
obtained from Definition 2, where W, Ys , Yr and Y are now sets of annotated
names, by replacing clauses (iv) and (vi) by
(iv’) Q ≡ νW Ys0 Yr0 .(S 0 k R0 [ b/x ] k C)

(vi’) Q ≡ νW Y 0 .(P 0 k C)

respectively, such that Ys  N = Ys0  N , Yr  N = Yr0  N , and Y  N = Y  N ,
where X  N := {x ∈ N | ∃τ.(x : τ ) ∈ X}. I.e. the type annotation of the names
that are activated by the transition (i.e. those from Ys , Yr and Y ) are not required
to be preserved in Q. (By contrast, the annotation of every active restriction in
P is preserved by the transition.) While in this context inactive annotations can

12

E. D’Osualdo and C.-H. L. Ong

be ignored by the transitions, they will be used by the type system in Section 4,
to establish invariance of T-compatible.
Now we are ready to explain what it means for an annotated term P to be
T-compatible: there is a forest in FJP K such that every trace of it projects to a
chain in the partial order T .
Definition 6 (T-compatibility). Let P ∈ P T be an annotated π-term. A forest
ϕ ∈ FJP K is T-compatible if for every trace ((x1 , t1 ) . . . (xk , tk ) A) in ϕ it holds
that t1 < t2 < . . . < tk . The π-term P is T-compatible if FJP K contains a
T-compatible forest. A term is T-shaped if each of its subterms is T-compatible.
As a property of annotated terms, T-compatibility is by definition invariant
under structural congruence.
A term P 0 ∈ P T is a type annotation (or simply annotation) of P ∈ P if its
type-erasure, written pP q, coincides with P . (We omit the obvious definition
of type-erasure.) A consistent annotation of a transition of terms, P → Q, is a
choice function that, given an annotation P 0 of P , returns an annotation Q0 of Q
such that P 0 → Q0 . Note that it follows from the definition that the annotation of
every active restriction in P 0 is preserved in Q0 . The effect of the choice function
is therefore to pick a possibly new annotation for each restriction in Q0 that is
activated by the transition. Thus, given a semantics (P, →, P ) of a term P , and
an annotation P 0 of P , and a consistent annotation for every transition of the
semantics, there is a well-defined pointed transition system (P T , →0 , P 0 ) such
that every transition sequence of the former lifts to a transition sequence of the
latter. We call (P T , →0 , P 0 ) a consistent annotation of the semantics (P, →, P ).
Definition 7 (Hierarchical term). A term P ∈ P is hierarchical if there exist
a finite forest T = T and a consistent annotation (P T , →0 , P 0 ) of the semantics
(P, →, P ) of P , such that all terms reachable from P 0 are T-compatible.
Example 8. The term in Examples 2 and 6 is hierarchical: take the hierarchy
T = s  c  m  d and annotate each name in Qijk as follows: s : s, c : c, m : m
and d : d. The annotation is consistent, and forest(Qijk ) is T-compatible for all
i,j and k.
Example 4 gives an example of a term that is not hierarchical. The forest
representation of the reachable terms shown in Example 7 does not have a
bounded height, which means that if T has n base types, there is a reachable
term with a representation of height bigger than n, which implies that there will
be a path repeating a base type.
Let us now study this fragment. First it is easy to see that invariance of
T-compatibility under reduction →, for some finite T , puts a bound |T | on the
height of the T-compatible reachable forests, and consequently a bound on depth.
Theorem 3. Every hierarchical term is depth-bounded. The converse is false.
Thanks to Theorem 2, an immediate corollary of Theorem 3 is that coverability
and termination are decidable for hierarchical terms.

On Hierarchical Communication Topologies in the π-calculus

13

Unfortunately, like the depth-bounded fragment, membership of the hierarchical fragment is undecidable. The proof is by adapting the argument for the
undecidability of depth boundedness [14].
Lemma 1. Every terminating π-term is hierarchical.
Proof. Since the transition system of a term, quotiented by structural congruence,
is finitely branching, by König’s lemma the computation tree of a terminating
term is finite, so it contains finitely many reachable processes and therefore
finitely many names. Take the set of all (disambiguated) active names of the
reachable terms and fix an arbitrary total order T on them. The consistent
annotation with (x : x) for each name will prove the term hierarchical.
Theorem 4. Determining whether an arbitrary π-term is hierarchical, is undecidable.
Proof. The π-calculus is Turing-complete, so termination is undecidable. Suppose
we had an algorithm to decide if a term is hierarchical. Then we could decide
termination of an arbitrary π-term by first checking if the term is hierarchical; if
the answer is yes, we can decide termination for it by Theorem 1, otherwise we
know that it is not terminating by Lemma 1.
Theorem 4—and the corresponding version for depth-bounded terms—is a
serious impediment to any practical application of hierarchical terms to verifcation:
when presented with a term to verify, one has to prove that it belongs to one of
the two fragments, manually, before one can apply the relevant algorithms.
While the two fragments have a lot in common, hierarchical systems have a
richer structure, which we will exploit to define a type system that can prove a
term hierarchical, in a feasible, sound but incomplete way. Thanks to the notion
of hierarchy, we are thus able to statically capture an expressive fragment of the
π-calculus that enjoys decidable coverability.

4

A type system for hierarchical topologies

The purpose of this section is to devise a static check to determine if a term is
hierarchical. To do so, we define a type system, parametrised over a forest T ,
which satisfies subject reduction. Furthermore we prove that if a term is typable
then T-shapedness is preserved by reduction of the term. Typability together
with T-shapedness of the initial term would then prove the term hierarchical.
As we have seen in the introduction, the typing rules make use of a new
perspective on π-calculus reactions. Take the term
P = νa.(νb.ahbi.S k νc.a(x).R) = C[ahbi.S, a(x).R]
where C[−1 , −2 ] = νa.(νb.[−1 ] k νc.[−2 ]) is the reaction context. Standardly the
synchronisation of the two sequential processes over a is preceded by an extrusion

14

E. D’Osualdo and C.-H. L. Ong

of the scope of b to include νc.a(x).R, followed by the actual reaction:


νa. νb.(ahbi.S) k νc.a(x).R ≡ νa.νb. ahbi.S k νc.a(x).R

→ νa.νb. S k νc.(R[ b/x ])
This dynamic reshuffling of scopes is problematic for establishing invariance
of T-compatibility under reduction: notice how νc is brought into the scope of
νb, possibly disrupting T-compatibility. (For example, the preceding reduction
would break T-compatibility of the forest representations if the tree T is either
a  c  b or b  a  c.) We therefore adopt a different view. After the message is
transmitted, the sender continues in-place as S, while R is split into two parts
Rmig k R¬mig , one that uses the message (the migratable one) and one that does
not. The migratable portion Rmig is “installed” under νb so that it can make use
of the acquired name, while the non-migratable one can simply continue in-place:


νa. νb.(ahbi.S) k νc.a(x).R → νa. νb.(S k Rmig [ b/x ]) k νc.R¬mig
|
{z
}
|
{z
}
C[ahbi.S, a(x).R]

C[SkRmig [ b/x ], R¬mig ]

Crucially, the reaction context C is unchanged. This means that if the starting
term is T-compatible, the context of the reactum is T-compatible as well. Naturally,
this only makes sense if Rmig does not use c. Thus our typing rules impose
constraints on the use of names of R so that the migration does not result in
Rmig escaping the scope of bound names such as c.
The formal definition of “migratable” is subtle. Consider the term

νf.a(x).νc d e. xhci k chdi k ahei.ehf i
Upon synchronisation with νb.ahbi, surely xhci will need to be put under the scope
of νb after substituting b for x, hence the first component of the continuation,
xhci, is migratable. However this implies that the scope of νc will need to be
placed under νb, which in turn implies that chdi needs to be considered migratable
as well. On the other hand, νe.ahei.ehf i must be placed in the scope of f , which
may not be known by the sender, so it is not considered migratable.The following
definition makes these observations precise.
Definition
8 (Linked to, tied to, migratable). Given a normal form P =
Q
νX. i∈I Ai we say that Ai is linked to Aj in P , written i ↔P j, if fn(Ai )∩fn(Aj )∩
X=
6 ∅. We define the tied-to relation as the transitive closure of ↔P . I.e. Ai is
tied to Aj , written i aP j, if ∃k1 , . . . , kn ∈ I. i ↔P k1 ↔P k2 . . . ↔P kn ↔P j,
for some n ≥ 0. Furthermore, we say that a name y is tied to Ai in P , written
y /P i, if ∃j ∈ I. y ∈ Q
fn(Aj ) ∧ j aP i. Given an input-prefixed normal form
a(y).P where P = νX. i∈I Ai , we say that Ai is migratable in a(y).P , written
Miga(y).P (i), if y /P i.
These definitions have an intuitive meaning with respect to the communication
topology of a normal form P : two sequential subterms are linked if they are
connected by an hyperedge in the communication topology of P , and are tied to
each other if there exists a path between them.

On Hierarchical Communication Topologies in the π-calculus

15

The following lemma indicates how the tied-to relation fundamentally constrains the possible shape of the forest of a term.
Q
Lemma 2. Let P = νX. i∈I Ai ∈ Pnf , if i aP j then if a forest ϕ ∈ FJP K has
leaves labelled with Ai and Aj respectively, they belong to the same tree in ϕ (i.e.,
have a common ancestor in ϕ).
Example 9. Take the normal form P = νa b c.(A1 k A2 k A3 k A4 ) where
A1 = a(x), A2 = b(x), A3 = c(x) and A4 = ahbi. We have 1 ↔P 4, 2 ↔P 4,
therefore 1 aP 2 aP 4 and a /P 2. In Fig. 4 we show some of the forests in FJP K.
Forest 1 represents forest(P ). The fact that A1 , A2 and A4 are tied is reflected
by the fact that none of the forests place them in disjoint trees. Now suppose we
select only the forests in FJP K that respect the hierarchy a  b: in all the forests
in this set, the nodes labelled with A1 , A2 and A4 have a as common ancestor
(as in forests 1, 2, 3 and 4). In particular, in these forests A2 is necessarily a
descendent of a even if a is not one of its free names.
In Section 3 we introduced annotations in a rather abstract way by means
of a generic domain of types T. In Definition 7 we ask for the existence of an
annotation for the semantics of a term. Specifically, one can decide an arbitrary
annotation for each active name. A type system however will examine the term
statically, which means that it needs to know what could be a possible annotation
for a variable, i.e., the name bound in an input action. This information is directly
related to the notion of data-flow, that is the set of names that are bound to a
variable during runtime. Since a static method cannot capture this information
precisely, we make use of sorts [17], also known as simple types, to approximate
it. The annotation of a restriction will carry not only which base type should
be associated with its instances, but also instructions on how to annotate the
messages received or sent through those instances. Concretely, we define
T 3 τ ::= t | t[τ ]
where t ∈ T is a base type.
A name with type t cannot be used as a channel but can be used as a message;
a name with type t[τ ] can be used to transmit a name of type τ . We will write
base(τ ) for t when τ = t[τ 0 ] or τ = t. By abuse of notation we write, for a set of
types X, base(X) for the set of base types of the types in X.
As is standard, we keep track of the types of free names by means of a typing
environment. An environment Γ is a partial map from names to types, which
we will write as a set of type assignments, x : τ . Given a set of names X and
an environment Γ , we write Γ (X) for the set {Γ (x) | x ∈ X ∩ dom(Γ )}. Given
two environments Γ and Γ 0 with dom(Γ ) ∩ dom(Γ 0 ) = ∅, we write Γ Γ 0 for their
union. For a type environment Γ we define
minT (Γ ) := {(x : τ ) ∈ Γ | ∀(y : τ 0 ) ∈ Γ. base(τ 0 ) 6< base(τ )}.
A judgement Γ `T P means that P ∈ PnfT can be typed under assumptions
Γ , over the hierarchy T ; we say that P is typable if Γ `T P is provable for some

16

E. D’Osualdo and C.-H. L. Ong

∀i ∈ I. Γ, X `T Ai
∀i ∈ I. ∀x : τx ∈ X. x /P i =⇒ base(Γ (fn(Ai ))) < base(τx )
Par
Q
Γ `T νX. i∈I Ai
∀i ∈ I. Γ `T πi .Pi
Choice
P
Γ `T
i∈I πi .Pi
a : ta [τb ] ∈ Γ

Γ `T A

Γ `T !A
b : τb ∈ Γ

Γ `T ahbi.Q

Repl
Γ `T Q

Γ `T P

Γ `T τ .P

Tau

Out

Q
a : ta [τx ] ∈ Γ
Γ, x : τx `T νX. i∈I Ai

base(τx ) < ta ∨ ∀i ∈ I. Miga(x).P (i) =⇒ base(Γ (fn(Ai ) \ {a})) < ta
In
Q
Γ `T a(x).νX. i∈I Ai
Fig. 5. A type system for hierarchical terms. The term P stands for νX.

Q

i∈I Ai .

Γ and T . An arbitrary term P ∈ P T is said to be typable if its normal form is.
The typing rules are presented in Fig. 5.
The type system presents several non-standard features. First, it is defined on
normal forms as opposed to general π-terms. This choice is motivated by the fact
that different syntactic presentations of the same term may be misleading when
trying to analyse the relation between the structure of the term and T . The rules
need to guarantee that a reduction will not break T-compatibility, which is a
property of the congruence class of the term. As justified by Lemma 2, the scope
of names in a congruence class may vary, but the tied-to relation puts constraints
on the structure that must be obeyed by all members of the class. Therefore
the type system is designed around this basic concept, rather than the specific
scoping of any representative of the structural congruence class. Second, no type
information is associated with the typed term, only restricted names hold type
annotations. Third, while the rules are compositional, the constraints on base
types have a global flavour due to the fact that they involve the structure of T
which is a global parameter of typing proofs.
Let us illustrate intuitively how the constraints enforced by the rules guarantee
preservation of T-compatibility. Consider the term



P = νe a. νb. ahbi.A0 k νd. a(x).Q
with Q = νc.(A1 k A2 k A3 ), A0 = b(y), A1 = xhci, A2 = c(z).ahei and A3 = ahdi.
Let T be the forest with te  ta  tb  tc and ta  td , where tx is the base type of
the (omitted) annotation of the restriction νx, for x ∈ {a, b, c, d, e}. The reader
can check that forest(P ) is T-compatible.
In the traditional understanding of mobility, we would interpret the commu
nication of b over a as an application of scope extrusion to include νd. a(x).Q
in the scope of b and then syncronisation over a with the application of the

On Hierarchical Communication Topologies in the π-calculus

17

substitution [ b/x ] to Q; note that the substitution is only valid because the
scope of b has been extended to include the receiver.
Our key observation is that we can instead interpret this communication as a
migration of the subcomponents of Q that do get their scopes changed by the
reduction, from the scope of the receiver to the scope of the sender. For this
operation to be sound, the subcomponents of Q migrating to the sender’s scope
cannot use the names that are in the scope of the receiver but not of the sender.
In our specific example, after the synchronisation between the prefixes ahbi and
a(x), b is substituted to x in A1 resulting in the term A01 = bhci and A0 , A01 , A2
and A3 become active. The scope of A0 can remain unchanged as it cannot know
more names than before as a result of the communication. By contrast, A1 now
knows b as a result of the substitution [ b/x ]: A1 needs to migrate under the
scope of b. Since A1 uses c as well, the scope of c needs to be moved under b;
however A2 uses c so it needs to migrate under b with the scope of c. A3 instead
does not use neither b nor c so it can avoid migration and its scope remains
unaltered.
This information can be formalised using the tied-to relation: on one hand, A1
and A2 need to be moved together because 1 aQ 2 and they need to be moved
because x /Q 1, 2. On the other hand, A3 is not tied to neither A1 nor A2 in Q
and does not know x, thus it is not migratable. After reduction, our view of the
reactum is the term



νa. νb. A0 k νc.(A01 k A2 ) k νd.A3
the forest of which is T-compatible. Rule Par, applied to A1 and A2 , ensures
that c has a base type that can be nested under the one of b. Rule In does not
impose constraints on the base types of A3 because A3 is not migratable. It does
however check that the base type of e is an ancestor of the one of a, thus ensuring
that both receiver and sender are already in the scope of e. The base type of a
does not need to be further constrained since the fact that the synchronisation
happened on it implies that both the receiver and the sender were already under
its scope; this implies, by T-compatibility of P , that c can be nested under a.
We now describe the purpose of the rules of the type system in more detail.
Most of the rules just drive the derivation through the structure of the term. The
crucial constraints are checked by Par, In and Out.
The Out rule. The main purpose of rule Out is enforcing types to be consistent
with the dataflow of the process: the type of the argument of a channel a must
agree with the types of all the names that may be sent over a. This is a very
coarse sound over-approximation of the dataflow; if necessary it could be refined
using well-known techniques from the literature but a simple approach is sufficient
here to type interesting processes.
The Par rule. Rule Par is best understood imagining the normal form to be
typed, P , as the continuation of a prefix π.P . In this context a reduction exposes
each of the active sequential subterms of P which need to have a place in a

18

E. D’Osualdo and C.-H. L. Ong

T-compatible forest for the reactum. The constraint in Par can be read as follows.
A “new” leaf Ai may refer to names already present in the forests of the reaction
context; these names are the ones mentioned in both fn(Ai ) and Γ . Then we
must be able to insert Ai so that we can find these names in its path. However,
Ai must belong to a tree containing all the names in X that are tied to it in
P . So by requiring every name tied to Ai to have a base type greater than any
name in the context that Ai may refer to, we make sure that we can insert the
continuation in the forest of the context without violating T-compatibility. Note
that Γ (fn(Ai )) contains only types that annotate names both in Γ and fn(Ai ),
that is, names which are not restricted by X and are referenced by Ai (and
therefore come from the context).
The In rule. Rule In serves two purposes: on the one hand it requires the type
of the messages that can be sent through a to be consistent with the use of the
variable x which will be bound to the messages; on the other hand, it constrains
the base types of a and x so that synchronisation can be performed without
breaking T-compatibility.
The second purpose is achieved by distinguishing two cases, represented by
the two disjuncts of the condition on base types of the rule. In the first case, the
base type of the message is an ancestor of the base type of a in T . This implies
that in any T-compatible forest representing a(x).P , the name b sent as message
over a is already in the scope of P . Under this circumstance, there is no real
mobility, P does not know new names by the effect of the substitution [ b/x ],
and the T-compatibility constraints to be satisfied are in essence unaltered.
The second case is more complicated as it involves genuine mobility. This case
also requires a slightly non-standard feature: not only do the premises predicate
on the direct subcomponents of an input prefixed term, but also on the direct
subcomponents of the continuation. This is needed to be able to separate the
continuation in two parts: the one requiring migration and the one that does
not. The situation during execution is depicted in Fig. 6. The non migratable
sequential terms behave exactly as the case of the first disjunct: their scope is
unaltered. The migratable ones instead are intended to be inserted as descendents
of the node representing the message b in the forest of the reaction context.
For this to be valid without rearrangement of the forest of the context, we
need all the names in the context that are referenced in the migratable terms, to
be also in the scope at b; we make sure this is the case by requiring the free names
of any migratable Ai that are from the context (i.e. in Γ ) to have base types
smaller than the base type of a. The set base(Γ (fn(Ai ) \ {a})) indeed represents
the base types of the names in the reaction context referenced in a migratable
continuation Ai . In fact a is a name that needs to be in the scope of both the
sender and the receiver at the same time, so it needs to be a common ancestor of
sender and receiver in any T-compatible forest. Any name in the reaction context
and in the continuation of the receiver, with a base type smaller than the one of
a, will be an ancestor of a—and hence of the sender, the receiver and the node
representing the message—in any T-compatible forest. Clearly, remembering a

On Hierarchical Communication Topologies in the π-calculus

a

a

→

b

ahbi

19

a(x).P

b

P
mig

P
¬mig

Fig. 6. Explanation of constraints imposed by rule In. The dashed lines represent
references to names restricted in the reduction context.

is not harmful as it must be already in the scope of receiver and sender, so we
exclude it from the constraint.
Example 10. Take the normal form in Example 2. Let us fix T to be the forest
s  c  m  d and annotate the normal form with the following types: s : τs = s[τm ],
c : τc = c[τm ], m : τm = m[d] and d : d. We want to prove ∅ `T νs c.P . We can
apply rule Par: in this case there are no conditions on types because, being
the environment empty, we have base(∅(fn(A))) = ∅ for every active sequential
term A of P . Let Γ = {(s : τs ), (c : τc )}. The rule requires Γ `T !S, Γ `T !C and
Γ `T !M , which can be proved by proving typability of S, C and M under Γ by
rule Repl.
To prove Γ `T S we apply rule In; we have s : s[τm ] ∈ Γ and we need to prove
that Γ, x : τm `T νd.xhdi. No constraints on base types are generated at this step
since the migratable sequential term νd.xhdi does not contain free variables typed
by Γ making Γ (fn(νd.xhdi) \ {a}) = Γ ({x}) empty. Next, Γ, x : τm `T νd.xhdi
can be proved by applying rule Par which amounts to checking Γ, x : τm , d : d `T
xhdi.0 (by a simple application of Out and the axiom Γ, x : τm , d : d `T 0) and
verifying the condition—true in T —base(τm ) < base(τd ): in fact d is tied to xhdi
and, for Γ 0 = Γ ∪ {x : τm }, base(Γ 0 (fn(xhdi))) = base(Γ 0 ({x, d})) = base({τm }).
The proof for Γ `T M is similar and requires c < m which is true in T .
Finally, we can prove Γ `T C using rule In; both the two continuations A1 =
shmi and A2 = m(y).chmi are migratable in C and since base(τm ) < base(τc )
is false we need the other disjunct of the condition to be true. This amounts
to checking that base(Γ (fn(A1 ) \ {c})) = base(Γ ({s, m})) = base({τs }) = s < c
(note m 6∈ dom(Γ )) and base(Γ (fn(Aa ) \ {c})) = base(Γ (∅)) < c (that holds
trivially).
To complete the typing we need to show Γ, m : τm `T A1 and Γ, m : τm `T A2 .
The former can be proved by a simple application of Out which does not impose
further constraints on T . The latter is proved by applying In which requires
base(τc ) < m, which holds in T .
Note how, at every step, there is only one rule that applies to each subproof.
Example 11. The term Example 4 is not typable under any T . To see why,
one can build the proof tree without assumptions on T by assuming that each

20

E. D’Osualdo and C.-H. L. Ong

restriction νx has base type tx . When typing mhsi we deduce that ts = tn , which
is in contradiction with the constraint that tn < ts required by rule Par when
typing νs.(S k mhsi k s).

5

Soundness of the type system

We now establish the soundness of the type system. Theorem 5 will show how
typability is preserved by reduction. Theorem 6 establishes the main property
of the type system: if a term is typable then T-shapedness is invariant under
reduction. This allows us to conclude that if a term is T-shaped and typable,
then every term reachable from it will be T-shaped.
The subtitution lemma states that substituting names without altering the
types preserves typability.
Lemma 3 (Substitution). Let P ∈ PnfT and Γ be a typing environment such
that Γ (a) = Γ (b). Then it holds that if Γ `T P then Γ `T P [ b/a ].

Before we state the main theorem, we define the notion of P -safe type
environment, which is a simple restriction on the types that can be assigned to
names that are free at the top-level of a term.
Definition 9 (P -safe environment). A type environment Γ is said to be P safe if for each x ∈ fn(P ) and (y : τ ) ∈ bnν (P ), base(Γ (x)) < base(τ ).
Theorem 5 (Subject Reduction). Let P and Q be two terms in PnfT and Γ
be a P -safe type environment. If Γ `T P and P → Q, then Γ `T Q.
The proof is by careful analysis of how the typing proof for P can be adapted
to derive a proof for Q. The only difficulty comes from the fact that some of the
subterms of P will appear in Q with a substitution applied. However, typability
of P ensures that we are only substituting names for names with the same type,
thus allowing us to apply Lemma 3.
To establish that T-shapedness is invariant under reduction for typable terms,
we will need to show that starting from a typable T-shaped term P , any step will
reduce it to a (typable) T-shaped term. The hypothesis of T-compatibility of P
can be used to extract a T-compatible forest ϕ from FJP K. While many forests in
FJP K can be witnesses of the T-compatibility of P , we want to characterise the
shape of a witness that must exist if P is T-compatible. The proof of invariance
relies on selecting a ϕ that does not impose unnecessary hierarchical dependencies
among names. Such forest is identified by ΦT (nf(P )): it is the shallowest among
all the T-compatible forests in FJP K.
Definition 10 (ΦT ). The function ΦT : PnfT → FT is defined inductively as
]
Q
ΦT ( i∈I Ai ) :=
{Ai []}
i∈I

o
Q
(x, base(τ ))[ΦT (νYx . j∈Ix Aj )] (x : τ ) ∈ minT (X)
Q
] ΦT (νZ. r∈R Ar )

ΦT (P ) :=

]n

On Hierarchical Communication Topologies in the π-calculus

21

Q
where X 6= ∅, P = νX. i∈I Ai Ix = {i ∈ I | x /P i} and
Yx = {(y : τ ) ∈ X | ∃i ∈ Ix . y ∈ fn(Ai )} \ minT (X)

S
Z = X\ (x : τ )∈minT (X) Yx ∪ {x : τ }

S
R = I\ (x : τ )∈minT (X) Ix
Forest 4 of Fig. 4 is ΦT (P ) when every restriction νx has base type x (for
x ∈ {a, b, c}) and T is the forest with nodes a, b and c and a single edge a  b.
Lemma 4. Let P ∈ PnfT . Then:
a) ΦT (P ) is a T-compatible forest;
b) ΦT (P ) ∈ FJP K if and only if P is T-compatible;
c) if P ≡ Q ∈ P T then ΦT (P ) ∈ FJQK if and only if Q is T-compatible.
Theorem 6 (Invariance of T-shapedness). Let P and Q be terms in PnfT
such that P → Q and Γ be a P -safe environment such that Γ `T P . Then, if P
is T-shaped then Q is T-shaped.
The key of the proof is a) the use of ΦT (P ) to extract a specific T-compatible
forest, b) the definition of a way to insert the subtrees of the continuations of
the reacting processes in the forest of reaction context, in a way that preserves
T-compatibility. Thanks to the constraints of the typing rules, we will always
be able to find a valid place in the reaction context where to attach the trees
representing the reactum.

6

Type inference

In this section we will show that it is possible to take any non-annotated normal
form P and derive a forest T and an annotated version of P that can be typed
under T .
Inference for simple types has already been proved decidable in [8, 23]. In our
case, since our types are not recursive, the algorithm concerned purely with the
constraints imposed by the type system of the form τx = t[τy ] is even simpler.
The main difficulty is inferring the structure of T .
Let us first be more specific on assigning simple types. The number of ways
a term P can be annotated with types are infinite, simply from the fact that
types allow an arbitrary nesting as in t, t[t], t[t[t]] and so on. We observe that,
however, there is no use annotating a restriction with a type with nesting deeper
than the size of the program: the type system cannot inspect more deeply nested
types. Thanks to this observation we can restrict ourselves to annotations with
bounded nesting in the type’s structure. This also gives a bound on the number
of base types that need to appear in the annotated term. Therefore, there are
only finitely many possible annotations and possible forests under which P can
be proved typably hierarchical. A naı̈ve inference algorithm can then enumerate
all of them and type check each.

22

E. D’Osualdo and C.-H. L. Ong

Theorem 7 (Decidability of inference). Given a normal form P ∈ Pnf , it is
decidable if there exists a finite forest T , a T-annotated version P 0 ∈ P T of P
and a P 0 -safe environment Γ such that P 0 is T-shaped and Γ `T P 0 .
While enumerating all the relevant forests, annotations and environments is
impractical, more clever strategies for inference exist.
We start by annotating the term with type variables: each name x gets typed
with a type variable tx . Then we start the type derivation, collecting all the
constraints on types along the way. If we can find a T and type expressions to
associate to each type variable, so that these constraints are satisfied, the process
can be typed under T .
By inspecting rules Par and In we observe that all the “tied-to” and “migratable” predicates do not depend on T so for any given P , the type constraints
can be expressed simply by conjuctions and disjuctions of two kinds of basic
predicates:
1. data-flow constraints of the form tx = tx [ty ] where tx is a base type variable;
2. base type constraints of the form base(tx ) < base(ty ) which correspond to
constraints over the corresponding base type variables, e.g. tx < ty .
Note that the P -safety condition on Γ translates to constraints of the second
kind. The first kind of constraint can be solved using unification in linear time.
If no solution exists, the process cannot be typed. This is the case of processes
that cannot be simply typed. If unification is successful we get a set of equations
over base type variables. Any assignment of those variables to nodes in a suitable
forest that satisfies the constraints of the second kind would be a witness of
typability. An example of the type inference in action can be found in Appendix.
First we note that if there exists a T which makes P typable and T-compatible,
then there exists a T 0 which does the same but is a linear chain of base types (i.e.
a single tree with no branching). To see how, simply take T 0 to be any topological
sort of T .
Now, suppose we are presented with a set C of constraints of the form t < t0
(no disjuctions). One approach for solving them could be based on reductions to
SAT or CLP(FD). We instead outline a direct algorithm. If the constraints are
acyclic, i.e. it is not possible to derive t < t by transitivity, then there exists a
finite forest satisfying the constraints, having as nodes the base type variables. To
construct such forest, we can first represent the constraints as a graph with the
base type variables as vertices and an edge between t and t0 just when t < t0 ∈ C.
Then we can check the graph for acyclicity. If the test fails, the constraints are
unsatisfiable. Otherwise, any topological sort of the graph will represent a forest
satisfying C.
We can modify this simple procedure to support constraints including disjuctions by using backtracking on the disjuncts. Every time we arrive at an acyclic
assigment, we can check for T-shapedness (which takes linear time) and in case
the check fails we can backtrack again.
To speed up the backtracking algorithm, one can merge the acyclicity test
with the T-compatibility check. Acyclicity can be checked by constructing a

On Hierarchical Communication Topologies in the π-calculus

23

topological sort of the constraints graph. Every time we produce the next node
in the sorting, we take a step in the construction of Φ(P ) using the fact that the
currently produced node is the minimal base type among the remaining ones. We
can then backtrack as soon as a choice contradicts T-compatibility.
The complexity of the type checking problem is easily seen to be linear in
the size of the program. This proves, in conjuction with the finiteness of the
candidate guesses for T and annotations, that the type inference problem is in
NP. We conjecture that inference is also NP-hard.
We implemented the above algorithm in a tool called ‘James Bound’ (jb),
available at http://github.com/bordaigorl/jamesbound.

7
7.1

Expressivity and verification
Expressivity

Typably hierarchical terms form a rather expressive fragment. Apart from including common patterns as the client-server one, they generalise powerful models of
computation with decidable properties.
Relations with variants of CCS are the easiest to establish: CCS can be seen
as a syntactic subset of π-calculus when including 0-arity channels, which are
very easily dealt with by straightforward specialisations of the typing rules for
actions. One very expressive, yet not Turing-powerful, variant is CCS! [9] which
can be seen as our π-calculus without mobility. Indeed, every CCS! process is
typably hierarchical [4, Section 11.4].
Reset nets can be simulated by using resettable counters as defined in Example 3. The full encoding can be found in Appendix. The encoding preserves
coverability but not reachability.
CCS! was recently proven to have decidable reachability [9] so it is reasonable
to ask whether reachability is decidable for typably hierarchical terms.
We show this is not the case by introducing a weak encoding of Minsky
machines (in Appendix). The encoding is weak in the sense that not all of the
runs represent real runs of the encoded Minsky machine; however with reachability
one can distinguish between the reachable terms that are encodings of reachable
configurations and those which are not. We therefore reduce reachability of
Minsky machines to reachability of typably hierarchical terms.
Theorem 8. The reachability problem is undecidable for (typably) hierarchical
terms.
Theorem 8 can be used to clearly separate the (typably) hierarchical fragment
from other models of concurrent computation as Petri Nets, which have decidable
reachability and are thus less expressive.
7.2

Applications

Although reachability is not decidable, coverability is often quite enough to prove
non-trivial safety properties. To illustrate this point, let us consider Example 2

24

E. D’Osualdo and C.-H. L. Ong

again. In our example, each client waits for a reply reaching its mailbox before
issuing another request; moreover the server replies to each request with a single
message. Together, these observations suggest that the mailboxes of each client will
contain at most one message at all times. To automatically verify this property we
could use a coverability algorithm for depth-bounded systems: since the example is
typable, it is depth-bounded and such algorithm is guaranteed to terminate with a
correct answer. To formulate the property as a coverability problem, we can ask for
coverability of the following query: νs m.(!S k m(y).chmi k νd.mhdi k νd0 .mhd0 i).
This is equivalent to asking whether a term is reachable that embeds a server
connected with a client with a mailbox containing two messages. The query is
not coverable and therefore we proved our property.5
Other examples of coverability properties are variants of secrecy properties.
For instance, the coverability query νs m m0 .(!S k m(y).chmi k m0 (y).chm0 i k
νd.(mhdi k m0 hdi)) encodes the property “can two different clients receive the
same message?”, which cannot happen in our example.
It is worth noting that this level of accuracy for proving such properties
automatically is uncommon. Many approaches based on counter abstraction [22, 6]
or CFA-style abstractions [5] would collapse the identities of clients by not
distinguishing between different mailbox addresses. Instead a single counter is
typically used to record the number of processes in the same control state and of
messages. In our case, abstracting the mailbox addresses away has the effect of
making the bounds on the clients’ mailboxes unprovable in the abstract model.
A natural question at this point is: how can we go about verifying terms
which cannot be typed, as the ring example? Coverability algorithms can be
applied to untypable terms and they yield sound results when they terminate. But
termination is not guaranteed, as the term in question may be depth-unbounded.
However, even a failed typing attempt may reveal interesting information
about the structure of a term. For instance, in Example 11 one may easily see that
the cyclic dependencies in the constraints are caused by the names representing
the “next” process identities. In the general case heuristics can be employed
to automatically identify a minimal set of problematic restrictions. Once such
restrictions are found, a counter abstraction could be applied to those restrictions
only yielding a term that simulates the original one but introducing some spurious
behaviour. Type inference can be run again on the the abstracted term; on failure,
the process can be repeated, until a hierarchical abstraction is obtained. This
abstract model can then be model checked instead of the original term, yielding
sound but possibly imprecise results.

8

Related work

Depth boundedness in the π-calculus was first proposed in [12] where it is proved
that depth-bounded systems are well-structured transition systems. In [24] it
is further proved that (forward) coverability is decidable even when the depth
5

To fully prove a bound on the mailbox capacity one may need to also ask another
coverability question for the case where the two messages bear the same data-value d.

On Hierarchical Communication Topologies in the π-calculus

25

bound k is not known a priori. In [25] an approximate algorithm for computing
the cover set—an over-approximation of the set of reachable terms—of a system
of depth bounded by k is presented. All these analyses rely on the assumption
of depth boundedness and may even require a known bound on the depth to
terminate.
Several other interesting fragments of the π-calculus have been proposed in
the literature, such as name bounded [10], mixed bounded [15], and structurally
stationary [13]. Typically defined by a non-trivial condition on the set of reachable
terms – a semantic property, membership becomes undecidable. Links with Petri
nets via encodings of proper subsets of depth-bounded systems have been explored
in [15]. Our type system can prove depth boundedness for processes that are
breadth and name unbounded, and which cannot be simulated by Petri nets. In [2],
Amadio and Meyssonnier consider fragments of the asynchronous π-calculus and
show that coverability is decidable for the fragment with no mobility and bounded
number of active sequential processes, via an encoding to Petri nets. Typably
hierarchical systems can be seen as an extension of the result for a synchronous
π-calculus with unbounded sequential processes and a restricted form of mobility.
Recently Hüchting et al. [11] proved several relative classification results
between fragments of π-calculus. Using Karp-Miller trees, they presented an
algorithm to decide if an arbitrary π-term is bounded in depth by a given k. The
construction is based on an (accelerated) exploration of the state space of the
π-term, with non primitive recursive complexity, which makes it impractical. By
contrast, our type system uses a very different technique leading to a quicker
algorithm, at the expense of precision. Our forest-structured types can also act
as specifications, offering more intensional information to the user than just a
bound k.
Our types are based on Milner’s sorts for the π-calculus [17, 8], later refined
into I/O types [20] and their variants [21]. Based on these types is a system for
termination of π-terms [3] that uses a notion of levels, enabling the definition
of a lexicographical ordering. Our type system can also be used to determine
termination of π-terms in an approximate but conservative way, by using it in
conjuction with Theorem 1. Because the respective orderings between types of the
two approaches are different in conception, we expect the terminating fragments
isolated by the respective systems to be incomparable.

9

Future directions

The type system we presented in Section 4 is conservative: the use of simple types,
for example, renders the analysis context-insensitive. Although we have kept the
system simple so as to focus on the novel aspects, a number of improvements are
possible. First, the extension to the polyadic case is straightforward. Second, the
type system can be made more precise by using subtyping and polymorphism to
refine the analysis of control and data flow. Third, the typing rule for replication
introduces a very heavy approximation: when typing a subterm, we have no
information about which other parts of the term (crucially, which restrictions)

26

E. D’Osualdo and C.-H. L. Ong

may be replicated. By incorporating some information about which names can
be instantiated unboundedly in the types, the precision of the analysis can be
greatly improved. The formalisation and validation of these extensions is a topic
of ongoing research.
Another direction worth exploring is the application of this machinery to
heap manipulating programs and security protocols verification.
Acknowledgement. We would like to thank Damien Zufferey for helpful discussions
on the nature of depth boundedness, and Roland Meyer for insightful feedback
on a previous version of this paper.

Bibliography

[1] P. A. Abdulla, K. Cerans, B. Jonsson, and Y. Tsay. General decidability
theorems for infinite-state systems. In Symposium on Logic in Computer
Science, pages 313–321. IEEE Computer Society, 1996.
[2] R. M. Amadio and C. Meyssonnier. On decidability of the control reachability
problem in the asynchronous π-calculus. Nordic Journal of Computing, 9
(2):70–101, 2002.
[3] Y. Deng and D. Sangiorgi. Ensuring termination by typability. Information
and Computation, 204(7):1045–1082, 2006.
[4] E. D’Osualdo. Verification of Message Passing Concurrent Systems. PhD
thesis, University of Oxford, 2015. URL http://ora.ox.ac.uk/objects/
uuid:f669b95b-f760-4de9-a62a-374d41172879.
[5] E. D’Osualdo, J. Kochems, and C.-H. L. Ong. Automatic verification of
erlang-style concurrency. In F. Logozzo and M. Fähndrich, editors, Static
Analysis Symposium (SAS), volume 7935 of Lecture Notes in Computer
Science, pages 454–476. Springer, 2013.
[6] E. A. Emerson and R. J. Trefler. From asymmetry to full symmetry: New
techniques for symmetry reduction in model checking. In L. Pierre and
T. Kropf, editors, Correct Hardware Design and Verification Methods, volume
1703 of Lecture Notes in Computer Science, pages 142–156. Springer, 1999.
[7] A. Finkel and P. Schnoebelen. Well-structured transition systems everywhere!
Theoretical Computer Science, 256(1-2):63–92, 2001.
[8] S. J. Gay. A sort inference algorithm for the polyadic π-calculus. In M. S. V.
Deusen and B. Lang, editors, Principles of Programming Languages (POPL),
pages 429–438. ACM Press, 1993.
[9] C. He. The decidability of the reachability problem for CCS! . In Concurrency
Theory (CONCUR), volume 6901 of Lecture Notes in Computer Science,
pages 373–388. Springer, 2011.
[10] R. Hüchting, R. Majumdar, and R. Meyer. A theory of name boundedness.
In Concurrency Theory (CONCUR), 2013.
[11] R. Hüchting, R. Majumdar, and R. Meyer. Bounds on mobility. In Concurrency Theory (CONCUR), pages 357–371, 2014.
[12] R. Meyer. On boundedness in depth in the π-calculus. In IFIP International
Conference on Theoretical Computer Science, IFIP TCS, pages 477–489,
2008.
[13] R. Meyer. A theory of structural stationarity in the π-calculus. Acta
Informatica, 46(2):87–137, 2009.
[14] R. Meyer. Structural stationarity in the π-calculus. PhD thesis, University
of Oldenburg, 2009.
[15] R. Meyer and R. Gorrieri. On the relationship between π-calculus and
finite place/transition Petri nets. In Concurrency Theory (CONCUR), pages
463–480, 2009.

28

E. D’Osualdo and C.-H. L. Ong

[16] R. Milner. Functions as processes. Mathematical Structures in Computer
Science, 2(02):119–141, 1992.
[17] R. Milner. The polyadic pi-calculus: a tutorial. Springer-Verlag, 1993.
[18] R. Milner. Communicating and Mobile Systems: the π-Calculus. Cambridge
University Press, 1999.
[19] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, I, II.
Information and Computation, 100(1):1–77, 1992.
[20] B. C. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes.
In Symposium on Logic in Computer Science, pages 376–385, 1993.
[21] B. C. Pierce and D. Sangiorgi. Behavioral equivalence in the polymorphic
pi-calculus. Journal of the ACM, 47(3):531–584, 2000.
[22] A. Pnueli, J. Xu, and L. D. Zuck. Liveness with (0, 1, ∞)-counter abstraction.
In E. Brinksma and K. G. Larsen, editors, Computer Aided Verification
(CAV), volume 2404 of Lecture Notes in Computer Science, pages 107–122.
Springer, 2002.
[23] V. T. Vasconcelos and K. Honda. Principal typing schemes in a polyadic
π-calculus. In E. Best, editor, Concurrency Theory (CONCUR), volume 715
of Lecture Notes in Computer Science, pages 524–538. Springer, 1993.
[24] T. Wies, D. Zufferey, and T. Henzinger. Forward analysis of depth-bounded
processes. In Foundations of Software Science and Computation Structures
(FoSSaCS), pages 94–108, 2010.
[25] D. Zufferey, T. Wies, and T. Henzinger. Ideal abstractions for well-structured
transition systems. In Verification, Model Checking, and Abstract Interpretation (VMCAI), pages 445–460, 2012.

Appendix
A

Supplementary Material for Section 2

A.1

Definition and properties of nf

The function nf : P → Pnf , defined in Definition 11, extracts, from a term, a
normal form structurally equivalent to it.
Definition 11 (nf(P )). We define the function nf : P → Pnf as follows:
nf(0) := 0

nf(π.P ) := π. nf(P )

nf(M + M 0 ) := nf(M ) + nf(M 0 )

nf(P )



nf(Q)
nf(P k Q) :=

νXP XQ .(NP k NQ )




nf(νx.P ) := νx. nf(P )
nf(!M ) := !(nf(M ))

if nf(Q) = 0 6= nf(P )
if nf(P ) = 0
if nf(Q) = νXQ .NQ , nf(P ) = νXP .NP
and actν (NP ) = actν (NQ ) = ∅

Lemma 5. For each P ∈ P, P ≡ nf(P )
Proof. A straightforward induction on P .
Lemma 6. Let ϕ be a forest with labels in N ] S. Then ϕ = forest(Q) with
Q ≡ Qϕ where
Q
Qϕ := νXϕ . (n,A)∈I A
Xϕ := {`ϕ (n) ∈ N | n ∈ Nϕ }
I := {(n, A) | `ϕ (n) = A ∈ S}
provided
i) ∀n ∈ Nϕ , if `ϕ (n) ∈ S then n has no children in ϕ, and
ii) ∀n, n0 ∈ Nϕ , if `ϕ (n) = `ϕ (n0 ) ∈ N then n = n0 , and
iii) ∀n ∈ Nϕ , if `ϕ (n) = A ∈ S then for each x ∈ Xϕ ∩ fn(A) there exists n0 <ϕ n

such that `ϕ (n0 ) = x.

Proof. We proceed by induction on the structure of ϕ. The base case is when
ϕ = (∅, ∅), for which we have Qϕ = 0 and ϕ = forest(0).
When ϕ = ϕ0 ] ϕ1 we have that if conditions 8.i, 8.ii and 8.iii hold for ϕ, they
must hold for ϕ0 and ϕ1 as well, hence we can apply the induction hypothesis to
them obtaining ϕi forest(Qi ) with Qi ≡ Qϕi (i ∈ {0, 1}). We have ϕ = forest(Q0 k
Q1 ) by definition of forest, and we want to prove that Q0 k Q1 ≡ Qϕ . By condition
8.ii on ϕ, Xϕ0 and Xϕ1 must be disjoint; furthermore, by condition 8.iii on both

30

E. D’Osualdo and C.-H. L. Ong

ϕ0 and ϕ1 we can conclude that fn(Qϕi ) ∩ Xϕ1−i = ∅. We can therefore apply
scope extrusion: Q0 k Q1 ≡ Qϕ0 k Qϕ1 ≡ νXϕ0 Xϕ1 .(Pϕ0 k Pϕ1 ) = Qϕ .
The last case is when ϕ = l[ϕ0 ]. Suppose conditions 8.i, 8.ii and 8.iii hold for ϕ.
We distinguish two cases. If l = A ∈ S, by 8.i we have ϕ0 = (∅, ∅), ϕ = forest(A)
and A = Qϕ . If l = x ∈ N then we observe that conditions 8.i, 8.ii and 8.iii hold
for ϕ0 under the assumption that they hold for ϕ. Therefore ϕ0 = forest(Q0 ) with
Q0 ≡ Qϕ0 , and, by definition of forest, ϕ = forest(νx.Q0 ). By condition 8.ii we
have x 6∈ Xϕ0 so νx.Q0 ≡ νx.Qϕ0 ≡ ν(X ∪ {x}).Pϕ0 = Qϕ .

B
B.1

Supplementary Material for Section 3
Proof of Theorem 3

First, it is immediate to see that every hierarchical term is depth-bounded. Any
T-compatible forest cannot repeat a type in a path, which means that the number
of base types in T bounds the height of T-compatible forests. This automatically
gives a bound on the depth of any T-compatible term.
We show the converse is not true by presenting a depth-bounded process
which is not hierarchical. Take P = (!A k !B k !(C1 + C2 )) where
A = τ .ν(a : a).phai

C1 = p(x).!(q(y).D)

B = τ .ν(b : b).qhbi

C2 = q(x).!(p(y).D)

D = xhyi

then P is depth-bounded. However we can show there is no choice for consistent
annotations and T that can prove it hierarchical. Let h be the height of T .
From P we can reach, by reducing the τ actions of A and B, any of the terms
Qi,j = P k (νa.phai)i k (νb.qhbi)j (omitting annotations) for i, j ∈ N. The choice
for annotations can potentially assign a different type in T to each νa and νb.
Let n, m ∈ N be naturals strictly greater than 2h and consider the reachable
term Qn,nm ; from this term we can reach a term
 

m
 n
ab
Q = P k νa. νb.D[ a/x, b/y ] k ! q(y).D[ a/x ]
by never selecting C2 as part of a redex. Each occurrence of a and b will have an
annotation: we assume type tia is assigned to each occurrence i ≤ n of νa in Qab
i
ab
and a type ti,j
b is assigned to each occurrence j of νb under ν(a : ta ) in Q . Each
ab
occurrence of νa in Q has in its scope more than h occurrences of νb. We cannot
extrude more than h occurrences of νb because we would necessarily violate
T-compatibility by obtaining a path of length greater than h in the forest of the
i,h+1
extruded term. Therefore, w.l.o.g., we can assume that the types ti,1
b , . . . , tb
i
are all descendants of ta , for each i ≤ n. Pictorially, the parent relation in T
entails the relations in Fig. 7 where the edges represent <T .
The type associations of the restrictions in Qab are already fixed in Qn,nm .
From Qn,nm we can however also reach any of the terms



n

Qib = P k · · · k ν(b : ti,1
).
νa.D[
a/x,
b/y
]
k
!
p(y).D[
b/x
]
b

On Hierarchical Communication Topologies in the π-calculus
t1a

31

tn
a

t2a
···

t1,1
b

t1,2
b

· · · t1,h+1
t2,1
b
b

t2,2
b

· · · t2,h+1
b

tn,1
b

tbn,2

· · · tn,h+1
b

Fig. 7. Structure of T in the counterexample.

for i ≤ m, by making C2 and ν(b : ti,1
b ).qhbi react and then repeatedly making
!q(y).D react with each ν(a : tja ).phai. Let us consider Q1b . As before, we cannot
extrude more than h occurrences of a or we would break T-compatibility. We
must however extrude (a : t1a ) to get T-compatibility since t1a <T t1,1
b . From these
two facts we can infer that there must be a type associated to one of the a, let
it be t2a , such that t1a <T t1,1
<T t2a . We can apply the same argument to Q2b
b
2,1
obtaining t1a <T t2a <T tb <T t3a . Since m > 2h we can repeat this h + 1 times
and get t1a <T t2a <T . . . <T th+1
which contradicts the assumption that the
a
height of T is h.
The reason why the counterexample presented in the proof above fails to
be hierarchical is that (unboundedly many) names are used in fundamentally
different ways in different branches of the execution.

C
C.1

Supplementary Material for Section 4
Proof of Lemma 2

We show that the claim holds in the case where Ai is linked to Aj in P . From this,
a simple induction over the length of linked-to steps required to prove i aP j,
can prove the lemma.
Suppose i ↔P j. Let Y = fn(Ai ) ∩ fn(Aj ) ∩ {x | (x : τ ) ∈ X}, we have Y =
6 ∅.
Both Ai and Aj are in the scope of each of the restrictions bounding names
y ∈ Y in any of the processes Q in the congruence class of P , hence, by definition
of forest, the nodes labelled with Ai and Aj generated by forest(Q) will have
nodes labelled with (y, base(X(y))) as common ancestors.
C.2

Some auxiliary lemmas

Lemma 7. If forest(P ) is T-compatible then for any term Q which is an αrenaming of P , forest(Q) is T-compatible.
Proof. Straightforward from the fact that T-compatibility depends only on the
type annotations.
Q
Lemma 8. Let P = νX.
i∈I Ai be a T-compatible normal form, Y ⊆ X and
Q
J ⊆ I. Then P 0 = νY. j∈J Aj is T-compatible.

32

E. D’Osualdo and C.-H. L. Ong

Proof. Take a T-compatible forest ϕ ∈ FJP K. By Lemma 7 we can assume without
loss of generality that ϕ = forest(Q) where proving Q ≡ P does not require
α-renaming. Clearly, removing the leaves that do not correspond to sequential
terms indexed by Y does not affect the T-compatibility of ϕ. Similarly, if a
restriction (x : τ ) ∈ X is not in Y , we can remove the node of ϕ labelled with
(x, base(τ )) by making its parent the new parent of its children. This operation
is unambiguous under Name Uniqueness and does not affect T-compatibility, by
transitivity of <. We then obtain a forest ϕ0 which is T-compatible and that, by
Lemma 6, is the forest of a term congruent to the desired normal form P 0 .

D
D.1

Supplementary Material for Section 5
Some Elementary Properties of the Type System

Lemma 9. Let P ∈ PnfT and Γ , Γ 0 be type environments.
a) if Γ `T P then fn(P ) ⊆ dom(Γ );
b) if dom(Γ 0 ) ∩ bn(P ) = ∅ and fn(P ) ⊆ dom(Γ ),
then Γ `T P if and only if Γ Γ 0 `T P ;
c) if P ≡ P 0 ∈ PnfT then, Γ `T P if and only if Γ `T P 0 .
D.2

Proof of Lemma 4

Item a) is an easy induction on the cardinality of X.
Item b) requires more work. By item a) Φ(P ) is T-compatible so Φ(P ) ∈ FJP K
proves that P is T-compatible.
Q
To prove the ⇐-direction we assume that P = νX. i∈I Ai is T-compatible
and proceed by induction on the cardinality
of X U
to show that Φ(P ) ∈ Q
FJP K. The
Q
base case is when X = ∅: Φ(P ) = Φ( i∈I Ai ) = i∈I {Ai []} = forest( i∈I Ai ) =
forest(P ) ∈ FJP K. For the induction step, we observe that X 6= ∅ implies
minT (X) 6= ∅ so, Z ⊂ X and for each (x : τ ) ∈ minT (X), Yx ⊂ X since
x 6∈ Yx . This, together with Lemma
8, allows us to Q
apply the induction hyQ
potesis on the terms Px = νYx . j∈Ix Aj and PR = νZ. r∈R Ar , obtaining that
there exist terms Qx ≡ Px and QR ≡ PR such that forest(Qx ) = Φ(Px ) and
forest(QR ) = Φ(PRQ
) where all the forests forest(Qx ) and forest(QR ) are T-com{ν(x : τ ).Qx | (x : τ ) ∈ minT (X)} k QR , then forest(Q) =
patible. Let Q =
Φ(P
).
To
prove
the
Q
Q claim we only need to show that Q ≡ P . We have Q ≡
{ν(x : τ ).νYx . j∈Ix Aj | (x : τ ) ∈ minT (X)} k PR and we want to apply extru
Q
U
sion to get Q ≡ νYU
{Ix | (x : τ ) ∈ minT (X)},
min .
i∈Imin Ai k PR for Imin =
Ymin = minT (X) ] {Yx | (x : τ ) ∈ minT (X)} which adds an obligation to prove
that
i) Ix are all pairwise disjoint so that Imin is well-defined,
ii) Yx are all pairwise disjoint and all disjoint from minT (X) so that Ymin is
well-defined,

On Hierarchical Communication Topologies in the π-calculus

33

iii) Yx ∩fn(Aj ) = ∅ for every j ∈ Iz with z =
6 x so that we can apply the extrusion
rule.
To prove condition i), assume by contradiction that there exists an i ∈ I
and names x, y ∈ minT (X) with x 6= y, such that both x and y are tied to
Ai in P . By transitivity of the tied-to relation, we have Ix = Iy . By Lemma 2
all the Aj with j ∈ Ix need to be in the same tree in any forest ϕ ∈ FJP K.
Since P is T-compatible there exist such a ϕ which is T-compatible and has
every Aj as label of leaves of the same tree. This tree will include a node nx
labelled with (x, base(X(x))) and a node ny labelled with (y, base(X(y))). By
T-compatibility of ϕ and the existence of a path between nx and ny we infer
base(X(x)) < base(X(y)) or base(X(y)) < base(X(x)) which contradicts the
assumption that x, y ∈ minT (X).
Condition ii) follows from condition i): suppose there exists a (z : τ ) ∈ X ∩
Yx ∩ Yy for x 6= y, then we would have that z ∈ fn(Ai ) ∩ fn(Aj ) for some i ∈ Ix
and j ∈ Iy , but then i aP j, meaning that i ∈ Iy and j ∈ Ix violating condition i).
The fact that Yx ∩ minT (X) = ∅ follows from the definition of Yx . The same
reasoning proves condition iii).Q

Q
Now we have Q ≡ νYmin . i∈IQ
Ai k νZ. r∈R Ar and we want to apply
min
extrusion again to get Q ≡ νYmin Z. {Ai | i ∈ (Imin ] R)} which is sound under
the following conditions:
iv) Ymin ∩ Z = ∅,
v) Imin ∩ R = ∅,
vi) Z ∩ fn(Ai ) = ∅ for all i 6∈ R

of which the first two hold trivially by construction, while the last follows from
condition viii) below, as a name in the intersection of Z and a fn(Ai ) would need
to be in X but not in Ymin . To be able to conclude that Q ≡ P it remains to
prove that
vii) I = Imin ] R and
viii) X = Ymin ] Z

which are also trivially valid by inspection of their definitions. This concludes
the proof for item b).
Finally, for every Q ∈ P T such that Q ≡ P , Φ(P ) ∈ FJQK if and only if
Φ(P ) ∈ FJP K by definition of FJ−K; since Φ(P ) is T-compatible we can infer
that Q is T-compatible if and only if Φ(P ) ∈ FJQK, which proves item c).
In light of Lemma 4, we can turn the computation of ΦT (P ) into an algorithm
to check T-compatibility of P : it is sufficient to compute ΦT (P ) and check at each
step that the sets Ix , R form a partition of I and the sets Yx , Z form a partition
of X. If the checks fail ΦT (P ) 6∈ FJP K and P is not T-compatible, otherwise the
obtained forest is a witness of T-compatibility.
D.3

Further Properties of ΦT (P )
Q
Lemma 10. Let P = νX. i∈I Ai ∈ PnfT be a T-compatible normal form. Then
for every trace ((x1 , t1 ) . . . (xk , tk ) Aj ) in the forest Φ(P ), for every i ∈ {1, . . . , k},
we have xi /P j (i.e. xi is tied to Aj in P ).

34

E. D’Osualdo and C.-H. L. Ong

Proof. Straightforward from the definition of Ix in Φ: when a node labelled by
(x, t) is introduced, its subtree is extracted from a recursive call on a term that
contains all and only the sequential terms that are tied to x.
Remark 1. Φ(P ) satisfies conditions 8.i, 8.ii and 8.iii of Lemma 6.
D.4

Proof of Lemma 3

We prove the lemma by induction on the structure of P . The base case is when
P ≡ 0, where the claim trivially holds.Q
P
For the induction step, let P ≡ νX. i∈I Ai with Ai = j∈J πij .Pij , for some
finite sets of indexes I and J. Since the presence of replication does not affect
the typing proof, we can safely ignore that case as it follows the same argument.
Let us assume Γ `T P and prove that Γ `T P [ b/a ].
Let Γ 0 be Γ ∪ X. From Γ `T P we have
Γ, X `T Ai

x /P i =⇒ base(Γ (fn(Ai ))) < base(τx )

(1)
(2)

for each i ∈ I and x : τx ∈ X. To extract from this assumptions a proof for
Γ `T P [ b/a ], we need to prove that (1) and (2) hold after the substitution.
Since the substitution does not apply to names in X and the tied to relation
is only concerned with names in X, the only relevant effect of the substitution is
modifying the set fn(Ai ) to fn(Ai [ b/a ]) = fn(Ai ) \ {a} ∪ {b} when a ∈ fn(Ai );
But since Γ (a) = Γ (b) by hypothesis, we have base(Γ (fn(Ai [ b/a ]))) < base(τx ).
It remains to prove (1) holds after the substitution as well. This amounts to
prove for each j ∈ J that Γ 0 `T πij .Pij =⇒ Γ 0 `T πij .Pij [ b/a ]; we prove this
by cases.
Suppose πij = αhβi for two names α and β, then from Γ 0 `T πij .Pij we know
the following
α : tα [τβ ] ∈ Γ 0
0

β : τβ ∈ Γ 0

Γ `T Pij

(3)
(4)

Condition (3) is preserved after the substitution because it involves only types so,
even if α or β are a, their types will be left untouched after they get substituted
with b from the hypothesis that Γ (a) = Γ (b). Condition (4) implies Γ 0 `T
Pij [ b/a ] by inductive hypothesis.
Q
Suppose now that πij = α(x) and Pij ≡ νY. k∈K A0k for some finite set of
indexes K; by hypothesis we have:
α : tα [τx ] ∈ Γ 0
0

Γ , x : τx `T Pij

base(τx ) < tα ∨ ∀k ∈ K. Migπij .Pij (k) =⇒ base(Γ 0 (fn(A0k ) \ {α})) < tα

(5)
(6)
(7)

Now x and Y are bound names so they are not altered by substitutions. The
substitution [ b/a ] can therefore only be affecting the truth of these conditions

On Hierarchical Communication Topologies in the π-calculus

35

when α = a or when a ∈ fn(A0k ) \ (Y ∪ {x}). Since we know a and b are assigned
the same type by Γ and Γ ⊆ Γ 0 , condition (5) still holds when substituting a for
b. Condition (6) holds by inductive hypotesis. The first disjunct of condition (7)
depends only on types, which are not changed by the substitution, so it holds
after applying it if and only if it holds before the application. To see that the
second disjunct also holds after the substitution we observe that the migratable
condition depends on x and fn(A0k ) ∩ Y which are preserved by the substitution;
moreover, if a ∈ fn(A0k ) \ {α} then Γ 0 (fn(A0k ) \ {α}) = Γ 0 (fn(A0k [ b/a ]) \ {α}).
This shows that the premises needed to derive Γ 0 , x : τx0 `T πij .Pij [ b/a ] are
implied by our hypothesis, which completes the proof.
D.5

Proof of Theorem 5

We will only prove the result for the case when P → Q is caused by a synchronising
send and receive action since the τ action case is similar and simpler. From
P → Q we know that P ≡ νW.(S k R k C) ∈ PnfT with S ≡ (ahbi.νYs .S 0 )+Ms and
R ≡ (a(x).νYr .R0 ) + Mr the synchronising sender and receiver respectively;
Q Q≡
k C). In what follows, let W 0 = W Ys Yr , C = h∈H Ch ,
νW YsQ
Yr .(S 0 k R0 [ b/x ] Q
S 0 = i∈I Si0 and R0 = j∈J Rj0 , all normal forms.
For annotated terms, the type system is syntax directed: there can be only
one proof derivation for each typable term. By Lemma 9.c, from the hypothesis
Γ `T P we can deduce Γ `T νW.(S k R k C). The proof derivation for this
typing judgment can only be of the following shape:
Γ W `T S

Γ W `T R ∀h ∈ H. Γ W `T Ch
Γ `T νW.(S k R k C)

Ψ

(8)

where Ψ represents the rest of the conditions of the Par rule.6 The fact that P
is typable implies that each of these premises must be provable. The derivation
proving Γ, W `T S must be of the form
a : ta [τb ] ∈ Γ W b : τb ∈ Γ W Γ W `T νYs .S 0
Γ W `T ahbi.νYs .S 0
Γ `T ahbi.νYs .S 0 + Ms

ΨMs

(9)

where Γ W `T νYs .S 0 is proved by an inference of the shape
∀i ∈ I. Γ W Ys `T Si0

∀i ∈ I. ΨSi0

Γ W `T νYs .S 0

(10)

Analogously, Γ W `T R must be proved by an inference with the following
shape
a : ta [τx ] ∈ Γ W Γ W, x : τx `T νYr .R0 ΨR0
Γ W `T a(x).νYr .R0
ΨMr
(11)
0
Γ W `T a(x).νYr .R + Mr
6

Note that Ψ is trivially true by P -safety of Γ .

36

E. D’Osualdo and C.-H. L. Ong

and to prove Γ W, x : τx `T νYr .R0
∀j ∈ J. Γ W, x : τx , Yr `T Rj0

Γ W, x : τx `T νYr .R0

∀j ∈ J. ΨRj0

(12)

We have to show that from this hypothesis we can infer that Γ `T Q or,
equivalently (by Lemma 9.c), that Γ `T Q0 where Q0 = νW Ys Yr .(S 0 k R0 [ b/x ] k
C). The derivation of this judgment can only end with an application of Par:
∀i ∈ I. Γ W 0 `T Si0

∀j ∈ J. Γ W 0 `T Rj0 [ b/x ] ∀h ∈ H. Γ W 0 `T Ch

Ψ0

Γ `T νW 0 .(S 0 k R0 [ b/x ] k C)

In what follows we show how we can infer these premises are provable as a
consequence of the provability of the premises of the proof of Γ `T νW.(S k R k
C).
From Lemma 9.b and Name Uniqueness, Γ W Ys `T Si0 from (10) implies
Γ W 0 `T Si0 for each i ∈ I.
Let Γr = Γ W, x : τx . We observe that by (9) and (11), τx = τb . From (11)
we know that Γr Yr `T Rj0 which, by Lemma 3, implies Γr Yr `T Rj0 [ b/x ]. By
Lemma 9.b we can infer Γr Yr Ys `T Rj0 [ b/x ] and by applying the same lemma
again using fn(Rj0 [ b/x ]) ⊆ dom(Γ W Yr Ys ) and Name Uniqueness we obtain
Γ W 0 `T Rj0 [ b/x ].
Again applying Lemma 9.b and Name Uniqueness, we have that Γ W `T Ch
implies Γ W 0 `T Ch for each h ∈ H.
To complete the proof we only need to prove that for each A ∈ {Si0 |
i ∈ I} ∪ {Rj0 | j ∈ J} ∪ {Ch | h ∈ H}, Ψ 0 = ∀(x : τx ) ∈ W 0 . x tied to A in Q0 =⇒
base(Γ (fn(A))) < base(τx ) holds. This is trivially true by the hypothesis that Γ
is P -safe.
D.6

Proof of Theorem 6

We will consider the input output synchronisation case as the τ action one is
similar and simpler. We will further assume that the sending action ahbi is such
that ν(a : τa ) and ν(b : τb ) are both active restrictions of P , i.e. (a : τa ) ∈ W ,
(b : τb ) ∈ W with P ≡ νW.(S k R k C). The case when any of these two names is
a free name of P can be easily handled with the aid of the assumption that Γ is
P -safe.
As in the proof of Theorem 5, the derivation of Γ `T P must follow the shape
of (8).
From T-shapedness of P we can conclude that both νYs .S 0 and νYr .R0 are
T-shaped. We note that substitutions do not affect T-compatibility since they
do not alter the set of bound names and their type annotations. Therefore,
we can infer that νYr .R0 [ b/a ] is T-shaped. By Lemma 4 we know that ϕ =
Φ(νW.(S k R k C)) ∈ FJP K, ϕr = Φ(νYr .R0 [ b/a ]) ∈ FJνYr .R0 [ b/x ]K and
ϕs = Φ(νYs .S 0 ) ∈ FJνYs .S 0 K. Let ϕr = ϕmig ] ϕ¬mig where only ϕmig contains
a leaf labelled with a term with b as a free name. These leaves will correspond

On Hierarchical Communication Topologies in the π-calculus

37

to the continuations Rj0 that migrate in a(x).νYr .R0 , after the application of the
substitution [ b/x ]. By assumption, inside P both S and R are in the scope of
the restriction bounding a and S must also be in the scope of the restriction
bounding b. Let ta = base(τa ) and tb = base(τb ), ϕ will contain two leaves nS and
nR labelled with S and R respectively, having a common ancestor na labelled
with (a, ta ); nS will have an ancestor nb labelled with (b, tb ). Let pa , pS and
pR be the paths in ϕ leading from a root to na , nS and nR respectively. By
T-compatibility of ϕ, we are left with only two possible cases: either 1) ta < tb
or 2) tb < ta .
Let us consider case 1) first. The tree in ϕ to which the nodes nS and nR
belong, would have the following shape:

na
nb

nS

nR

Now, we want to transform ϕ, by manipulating this tree, into a forest ϕ0 that
is T-compatible by construction and such that there exists a term Q0 ≡ Q with
forest(Q0 ) = ϕ0 , so that we can conclude Q is T-shaped.
To do so, we introduce the following function, taking a labelled forest ϕ, a
path p in ϕ and a labelled forest ρ and returning a labelled forest:
ins(ϕ, p, ρ) := (Nϕ ] Nρ , ϕ ] ρ ] ins , `ϕ ] `ρ )
where n ins n0 if n0 ∈ minρ (Nρ ) and if `ρ (n0 ) = (y, ty ) then
n ∈ max {m ∈ p | `ϕ (m) = (x, tx ), tx < ty }
ϕ

or if `ρ (n0 ) = A then
n ∈ max {m ∈ p | `ϕ (m) = (x, tx ), x ∈ fn(A)}.
ϕ

Note that for each n0 , since p is a path, there can be at most one n such that
n ins n0 .
To obtain the desired ϕ0 , we first need to remove the leaves nS and nR from
ϕ, as they represent the sequential processes which reacted, obtaining a forest
ϕC . We argue that the ϕ0 we need is indeed
ϕ0 = ins(ϕ1 , pS , ϕmig )
ϕ1 = ins(ϕ2 , pR , ϕ¬mig )
ϕ2 = ins(ϕC , pS , ϕs )

38

E. D’Osualdo and C.-H. L. Ong

It is easy to see that, by definition of ins, ϕ0 is T-compatible: ϕC , ϕs , ϕ¬mig and
ϕmig are T-compatible by hypothesis, ins adds parent-edges only when they do
not break T-compatibility.
0
To prove the claim we need to show that
forest of a term congruent
Qϕ is the
0
0
0
to νW Ys Yr .(S k R [ b/x ] k C). Let R = j∈J Rj0 , Jmig = {j ∈ J | x /νYr .R0 j},
J¬mig = J \ Jmig and Yr0 = {(x : τ ) ∈ Yr | x ∈ fn(Rj0 ), j ∈ J¬mig }. We know that
no Rj0 with j ∈ J¬mig can contain x as a free name so Rj0 [ b/x ] = Rj0 . Now
suppose we are able to prove that conditions 8.i, 8.ii and 8.iii of Lemma 6 hold
for ϕC , ϕ1 , ϕ2 and ϕ0 . Then we could use Lemma 6 to prove
a)
b)
c)
d)

ϕC = forest(QC ), QC ≡ QϕC = νW.C,
ϕ2 = forest(Q2 ), Q2 ≡ Qϕ2 = νW Ys .(S 0 k C),Q
ϕ1 = forest(Q1 ), Q1 ≡ Qϕ1 = νW Ys Yr0 .(S 0 k j∈J¬mig Rj0 k C),
ϕ0 = forest(Q0 ), Q0 ≡ Qϕ0 = νW Ys Yr .(S 0 k R0 [ b/x ] k C) ≡ Q

(it is straightforward to check that ϕC , ϕ2 , ϕ1 and ϕ0 have the right sets of nodes
and labels to give rise to the right terms). We then proceed to check for each of
the forests above that they satisfy conditions 8.i, 8.ii and 8.iii, thus proving the
theorem.
Condition 8.i requires that only leafs are labelled with sequential processes,
condition that is easily satisfied by all of the above forests since none of the
operations involved in their definition alters this property and the forests ϕ, ϕs
and ϕr satisfy it by construction.
Similarly, since νW.(S k R k C) is a normal form it satisfies Name Uniqueness,
8.ii is satisfied as we never use the same name more than once.
Condition 8.iii holds on ϕ and hence it holds on ϕC since the latter contains
all the nodes of ϕ labelled with names.
Now consider ϕs : in the proof of Theorem 5 we established that Γ `T P implies
that the premises ΨSi0 from (10) hold, that is base(Γ W (fn(Si0 ))) < base(τx ) holds
for all Si0 for i ∈ I and all (x : τx ) ∈ Ys such that x /νYs .S 0 i. Since fn(Si0 ) ∩ W ⊆
fn(S 0 ) we know that every name (w : τw ) ∈ W such that w ∈ fn(Si0 ) will appear
as a label (w, base(τw )) of a node nw in pS . Therefore, by definition of ins, we
have that for each n ∈ NϕC , nw <ϕ2 n; in other words, in ϕ2 , every leaf in Nϕs
labelled with Si0 is a descendent of a node labelled with (w, base(τw )) for each
(w : τw ) ∈ W with w ∈ fn(Si0 ). This verifies condition 8.iii on ϕ2 .
Similarly, by (12) the following premise must hold: base(Γ W (fn(Rj0 ))) <
base(τx ) for all Rj0 for j ∈ J and all (y : τy ) ∈ Yr such that y /νYr .R0 j. We can
then apply the same argument we applied to ϕ2 to show that condition 8.iii holds
on ϕ1 .
From (11) and the assumption ta < tb , we can conclude that the following
premise must hold: base(Γ W (fn(Rj0 ) \ {a})) < ta for each j ∈ J such that Rj0 is
migratable in a(x).νYr .R0 , i.e j ∈ Jmig . From this we can conclude that for every
name (w : τw ) ∈ W such that w ∈ fn(Rj0 [ b/x ]) with j ∈ Jmig there must be a
node in pa (and hence in pS ) labelled with (w, base(τw )). Now, some of the leaves
in ϕmig will be labelled with terms having b as a free name; we show that in fact
every node in ϕmig labelled with a (y, ty ) is indeed such that ty < tb . From the

On Hierarchical Communication Topologies in the π-calculus

39

proof of Theorem 5 and Lemma 3 we know that from the hypothesis we can infer
that Γ W `T νYr .R0 [ b/x ] and hence that for each j ∈ Jmig and each (y : τy ) ∈ Yr ,
if y is tied to Rj0 [ b/x ] in νYr .R0 [ b/x ] then base(Γ W (Rj0 [ b/x ])) < base(τy ). By
Lemma 10 we know that every root of ϕmig is labelled with a name (y, ty )
which is tied to each of the leaves in its tree. Therefore each such ty satisfies
base(Γ W (Rj0 [ b/x ])) < ty . By construction, there exists at least one j ∈ Jmig
such that x ∈ fn(Rj0 ) and consequently such that b ∈ fn(Rj0 [ b/x ]). From this
and b ∈ W we can conclude tb < ty for ty labelling a root in ϕmig . We can
then conclude that {nb } = maxϕ2 {m ∈ pS | `ϕ (m) = (z, tz ), tz < ty } for each
ty labelling a root of ϕmig , which means that each tree of ϕmig is placed as a
subtree of nb in ϕ0 . This verifies condition 8.iii for ϕ0 completing the proof.
Pictorially, the tree containing nS and nR in ϕ is now transformed in the
following tree in ϕ0 :
na

∈ ϕs
∈ ϕmig
∈ ϕ¬mig

nb

pS

pR

Case 2) — where tb < ta — is simpler as the migrating continuations can be
treated just as the non-migrating ones.
D.7

Role of ϕmig , ϕ¬mig and ins

To illustrate the role of ϕmig , ϕ¬mig and the ins operation in the above proof, we
show an example that would not be typable if we choose a simpler “migration”
transformation.
Consider the normal form P = νa b c.(!A k ahci) where A = a(x).νd.(ahdi k
bhxi). To make types consistent we need annotations satisfying a : ta [t], b : tb [t],
c : t and d : t. Any T satisfying the constraints tb < ta < t would allow us to prove
∅ `T P ; let then T be the forest with b  a  t with ta = a, tb = b and t = t.
Let P 0 = νa b c d.(!A k ahdi k bhci) be the (only) successor of P . The following
picture shows Φ(P ) in the middle, on the left a forest in FJP 0 K extracted by just
putting the continuation of A under the message, on the right the forest obtained
by using ins on the non-migrating continuations of A:
b
a
c
d
bhci ahdi

!A

←

b
a
!A

c
ahci

→

!A

b
a
c

d
bhci ahdi

Clearly, the tree on the left is not T-compatible since c and d have the same base
type t. Instead, the tree on the right can be obtained because ins inserts the
non-migrating continuation as close to the root as possible.

40

E

E. D’Osualdo and C.-H. L. Ong

Supplementary Material for Section 6

E.1

A type inference example

Take the term ! τ .νs c.P of Example 2. We start by annotating each restriction
νa with a fresh type variable ν(a : ta ). Then we perform a type derivation as in
Example 10, obtaining the following data-flow constraints:
ts = ts [tz ]

tc = tc [tx ]

tx = tx [ty ]

tz = tx = tm = tz [td ]

from which we learn that:
- td is unconstrained; we use the base type variable td for base(td );
- ty = td ;
- tx = tz and base(tm ) = tx .
We can therefore completely specify the types just by associating ts , tc , tx and td
to nodes in a forest: all the types would be determined as a consequence of the
data-flow constraints, apart from td to which we can safely assign the type td .
During the type derivation we also collected the following base type constraints:
base(tz ) < base(td )

base(tc ) < base(tm )

base(tc ) < base(tx )

base(tx ) < base(tc ) ∨ base(ts ) < base(tc )
These can be simplified and normalised using the equations on types seen above
obtaining the set
Cνs c.P = {tx < tc ∨ ts < tc , tc < tx , tx < td }
Hence any choice of T ⊇ {tx , tc , ts , td } such that ts <T tc <T tx <T td would
make the typing succeed.

F
F.1

Supplementary Material for Section 7
Encoding of Reset nets

A reset net N with n places is a finite set of transitions of the form (u, R) where
n
u ∈ {−1, 0, +1} is the update vector and R ⊆ {1, . . . , n} is the reset set. A
marking m is a vector in Nn ; a transition (u, R) is said to be enabled at m
if m − u > 0. The semantics of a reset net N with initial marking m0 is the
transition system (Nn , [i, m0 ) where m [i m0 if there exists a transition (u, R) in
N that is enabled in m and such that
(
mi + ui if i 6∈ R
m0i =
0
if i ∈ R

On Hierarchical Communication Topologies in the π-calculus

41

To simulate place i in a reset net we can construct a term that implements a
counter with increment and reset:

Ci = ! pi (t). inc i .(t k pi hti) + dec i .(t.pi hti) + rst i .(νt0i .pi ht0i i)
Here, the number of processes t in parallel with pi hti represent the current
value of the marking in place i. A transition (u, R) is encoded as a process
Tu,R = ! valid .Du .Iu .ZR .valid where Du = dec j1 . · · · .dec jk with {j1 , . . . , jk } =
{j | uj < 0}, Iu = inc i1 . · · · .inc il with {i1 , . . . , il } = {i | ui > 0}, and ZR =
rst r1 . · · · .rst rm with R = {r1 , . . . , rl }.
A marking m is encoded by a process
Q
Q
m 
PN,m = valid k 1≤i≤n pi hti i k Ci k ti i k (u,R)∈N Tu,R
Actions on the name valid act as a global lock: a transition may need many steps
to complete, but by acquiring and releasing valid it can ensure no other transition
will fire in between. If a transition tries to decrement a counter below zero, the
counter would deadlock causing valid to be never released again. Therefore, the
encoding preserves coverability: m is coverable in N from m0 if and only if PN,m
is coverable from PN,m0 . Reachability is not preserved because each reset would
generate some ‘garbage’ term νt.(t k . . . k t) and thus, even when m is reachable,
PN,m might not be reachable alone, but only in parallel with some garbage.
The reader can verify that any encoding P can be typed under the hierarchy
valid < inc 1 < dec 1 < rst 1 < t1 < p1 < · · · <

inc n < dec n < rst n < tn < pn < t01 < · · · < t0n

by annotating each restriction νt0i as ν(t0i : t0i ) and using the P -safe environment
{(x : x) | x ∈ fn(P )}.
F.2

A weak encoding of Minsky machines

A k-counters Minsky machine is a finite list of instructions I1 , . . . , In each of
which can be either an increase or a decrease command. An increase command
inc i j increases counter i and jumps to instruction Ij . A decrease command
dec i j1 j2 decreases counter i jumping to instruction Ij1 if the counter is greater
than zero, or jumps to Ij2 otherwise. We implement a counter i with the process
Ci of Example 3. An increase Im = inc i j is encoded by ! im .inc i .ij . A decrease

Im = dec i j1 j2 is encoded by ! im .(dec i .ij1 + rst i .ij2 ) . A configuration of a
Minsky machine is the vector of values of its registers r1 , . . . , rk and the current
instruction j; its encoding is the term
Q
Q
ri
1≤i≤k νti .(pi hti i k ti ) k ij k
1≤m≤n PIm
where PIm is the encoding of the instruction Im .
When a counter is zero, performing a decrease command on it in the encoding
presents a non-deterministic choice between sending a decrease or a reset signal

42

E. D’Osualdo and C.-H. L. Ong

to the counter. In the branch where the decrease signal is sent, the counter
process will deadlock, ending up in a term that is clearly not an encoding of a
configuration of the Minsky machine. If instead a reset signal is sent, the counter
will refresh the name t with a new name, but the old one would be discarded as
there is no sequential term which knows it.
When a counter is not zero, the branch where the decrease signal is sent
will simply succeed, while the resetting one will generate some ‘garbage’ term
νt.(t k . . . k t) in parallel with the rest of the encoding of the Minsky machine’s
configuration.
A configuration of the machine is thus reachable if and only if its encoding
(without garbage) is reachable from the encoding of the machine. This proves
Theorem 8.

