Shape Calculus:
Timed Operational Semantics and Well-formedness

arXiv:1011.2488v1 [cs.PL] 9 Nov 2010

Ezio Bartocci1
Maria Rita Di Berardini1

Diletta Romana Cacciagrano1
Emanuela Merelli1
Luca Tesei1

Abstract
The Shape Calculus is a bio-inspired calculus for describing 3D
shapes moving in a space. A shape forms a 3D process when combined
with a behaviour. Behaviours are specified with a timed CCS-like process algebra using a notion of channel that models naturally binding
sites on the surface of shapes. Processes can represent molecules or
other mobile objects and can be part of networks of processes that
move simultaneously and interact in a given geometrical space. The
calculus embeds collision detection and response, binding of compatible 3D processes and splitting of previously established bonds. In this
work the full formal timed operational semantics of the calculus is provided, together with examples that illustrate the use of the calculus in
a well-known biological scenario. Moreover, a result of well-formedness
about the evolution of a given network of well-formed 3D processes is
proved.

1

Introduction

In a near future, systems biology will profoundly affect health care and
medical science. One aim is to design and test “in-silico” drugs giving rise to
individualized medicines that will take into account physiology and genetic
profiles [14]. The advantages of performing in-silico experiments by simulating a model, instead of arranging expensive in-vivo or in-vitro experiments,
are evident. But of course the models should be as faithful as possible to
the real system.
Towards the improving of the faithfulness of languages and models proposed in literature in the field of systems biology, the Shape Calculus [6, 5, 4]
1

School of Science and Technology, University of Camerino
Via Madonna delle Carceri 9, 62032, Camerino (MC), Italy.
Email: name.surname@unicam.it

1

was proposed as a very rich language to describe mainly, but not only, biological phenomena. The main new characteristics of this calculus are that
it is spatial - with a geometric notion of a 3D space - and it is shape-based,
i.e. entities have geometric simple or complex shapes that are related to
their “functions”, that is to say, in the context of formal calculi, the possible interactions that can occur among the entities (called 3D processes, in
the same context). Note that there are some other approaches that use a
geometric notion of space [2, 16, 3], but they do not fully exploit the potentiality of geometry: they only consider positions that are centers of perception/communication spheres or discretized the space using grids. Moreover,
differently to classical mathematical models for biological systems, the Shape
Calculus is individual-based, that is to say it considers autonomous entities
that interact with others in order to give rise to an emerging behaviour of the
whole system. However, this characteristic is also present in other languages
and models proposed in literature [18, 19, 11, 7, 12]. Parallel to the introduction of the Shape Calculus, a simulation environment called BioShape
[20, 9] has been proposed. This environment embodies all the concepts and
features of the Shape Calculus, plus others, more detailed, characteristics
that are related to the implementation of simulations in different biological
case studies [9, 8, 10]. The Shape Calculus can be considered the formal
core of BioShape. On the Shape Calculus, formal verification techniques
can be applied, while in-silico experiments (simulations) can be performed
in BioShape. These two approaches can be used successfully in an independent way, but they can also be combined to address complex biological
case studies.
In [5], the language of the Shape Calculus was introduced with the main
aim of gently and incrementally present all its features and their relative
semantics. The motivations behind the type and nature of the calculus operators were discussed and a great variety of scenarios in which the calculus
may be used effectively were described. In [4] the timed operational semantics of the calculus was introduced and a well-formedness property of the
dynamics of the calculus was proved.
This paper is an extended version of [4] in which the original concepts
of the calculus are fully recalled and in which further examples are provided in order to explain better the technical details of its timed operational
semantics.
We present the full timed operational semantics of the Shape Calculus
and we explain with proper running examples all the technical points that

2

Figure 1: An example of binding and subsequent weak-split of two 3D processes.
need particular attention and further explanation. Moreover, we define a
concept of well-formedness, starting from shapes and porting it to more
complex calculus objects such as 3D processes and, ultimately, networks
of 3D processes. In the calculus, only well-formed objects are considered.
Well-formedness is a standard concept used to avoid strange and unwanted
situations in which a term can be legally written by syntax rules, but that
semantically corresponds to a contradictory situation, for instance, in our
case, a composed shape whose pieces move in different directions. We prove
that a given well-formed network of 3D processes always evolves into a wellformed network of 3D processes, that is to say, no temporal and spatial
inconsistencies are introduced by the dynamics of the calculus.
The paper is organized as follows. Section 2 recalls the main concepts
of the calculus and focuses on weak and strong split operations whose semantics are slightly more complicated to define than that of other operators.
Section 3 introduces formally 3D shapes, shape composition, movement, collision detection and collision response. Section 4 defines behaviours and 3D
processes giving them full semantics. Section 5 puts all the pieces together
and specifies precisely networks of 3D processes and a general result of dynamic well-formedness is proven. Finally, Section 6 concludes with ongoing
and future work directions. For the sake of readability all the proofs have
been moved in Appendices A, B and C.

3

2

Recall of Main Concepts

In this section we recall the main concepts the calculus introduced in [5] and
we focus in particular to the weak and strong split operations, in order to
make them clear from the beginning and, thus, then smoothly define their
semantics, which requires some particular technical expedients.
The general idea of the Shape Calculus is to consider a 3D space in
which several shapes reside, move and interact. While time flows, shapes
move according to their velocities, that can change over time both due to a
general motion law - for instance as in a gravitational or in an electromagnetic field, or as in Brownian motion - and due to collisions that can occur
between two or more shapes. Collisions can result in a bounce, that is to
say elastic collisions. Instead, as it often happens in biological scenarios,
colliding objects can bind and become a new compound object moving in
a different way and possibly having a different behaviour. In this case we
speak of inelastic collisions since they are treated with the physical law for
that kind of collision.
The Shape Calculus can be used to represent a lot of scenarios at different scales in different fields [5]. However, in this work we use a well-known
biological scenario in order to introduce simple running examples that illustrate the semantics of the calculus operators. We consider biochemical
reactions occurring inside a cell. Every species of involved molecules has a
specific shape and we know from biology that the functions of a molecule
are tightly related to its shape. For instance, in enzymatic reactions the
functional sites that are active in the enzyme structure, at a given time,
determine which substrate (one or two metabolites) can bind the enzyme
and proceed to the catalyzed reaction.
Fig. 1 shows a (2D, for simplicity) possible representation of an enzymatic reaction. The larger object represents an enzyme with a shape S0
and a behaviour B0 ; S0 and B0 together constitute a 3D process S0 [B0 ].
The 3D process S1 [B1 ] represents a metabolite that is close to the given
enzyme. Note that portions of the shape surfaces are highlighted: they are
the channels (an extension of the notion of channels of CCS [17]) that the
corresponding 3D processes exhibit to the environment. Each channel has
a name and an active surface. For instance, ha, Xi is a channel of type a
on the active site X of S0 [B0 ]. The enzyme in Fig. 1 has two channels and
its behaviour can be specified as: B0 = hb, Y i.B00 + ha, Xi.B000 . The plus
operator represents a non-deterministic choice between two possible communications on the channels. This non-determinism is resolved during the
4

Figure 2: An example of complex formation and subsequent strong-split.
evolution of the system depending on which 3D processes will collide with
the enzyme and where.
Following the evolution proposed in the figure, after some time t elapsed
t
(represented by the transition →
− ) and after a detection and resolution of an
inelastic collision (transition →
− i ), we get one compound process represented
by the term S0 [B00 ]hb, W iS1 [B10 ]. The bond is established on the surface of
contact W and the name b records the type of channels that bound. Note
that communication, i.e. binding, can only happen if there is a collision between two 3D processes that expose compatible channels (name and co-name
à la CCS) on their surface of contact. If the channels were not compatible,
the collision would have been treated as elastic and the two 3D processes
would have simply bounced. By letting B10 = hc, Y1 i.B100 we allow the component of shape S1 to open a new channel and to bind with other colling
processes.
The third stage of Fig. 1 represents a possible evolution of an enzyme
binding with a substrate; it can happen that, for some reason, the bond
is loose and the two molecules are free again. To model this kind of behaviour we introduce a special kind of not urgent split operation, called
weak-split operation, that can be delayed of an unspecified time. This is another source of non-determinism in the calculus. Fig. 2 shows what happens
when another substrate – that we represent as the 3D process S2 [B2 ] with a
channel ha, X1 i – binds with the compound process S0 [B00 ]hb, W iS1 [B10 ] on
the common surface W1 . In the terminology of biochemical reactions, a final
complex has been formed. As a consequence, the reaction must proceed and
5

the products must be released. In our calculus, reactions are represented
by strong-split operations. Differently from weak-split operations, this kind
of split operations cannot be delayed and must occur as soon as they are
enabled, i.e. when all the involved components can release all the bonds. In
this example the involved components are S0 [B00 ], S1 [B10 ] and S2 [B20 ]; the
set of bonds to be split is L = {hb, W i, ha, W1 i}.

3

3D Shapes

We start by introducing three dimensional shapes as terms of a suitable
language, allowing simpler shapes to bind and form more complex shapes.
From now on we consider assigned a global coordinate system in a three
dimensional space represented by R3 . Let P, V = R3 be the sets of positions and velocities, respectively, in this coordinate system. Throughout the
paper, we assume relative coordinate systems that will always be w.r.t. a
certain shape S, i.e. the origin of the relative system is the reference point
p of S. We refer to this relative system as the local coordinate system of
shape S. If p ∈ P is a position expressed in global coordinates, and V ⊆ P
is a set of points expressed w.r.t. a local coordinate system whose origin is
p, we define global(V, p) = V + p = {x + p | x ∈ V } to be the set V w.r.t.
the global coordinates. Using local coordinate systems we can express parts
of a given shape, such as faces and vertexes, independently from its actual
global position.
Definition 1 (Basic Shapes) A basic shape σ is a tuple hV, m, p, vi where
V ⊆ P is a convex polyhedron (e.g. a sphere, a cone, a cylinder, etc.)2 that
represents the set of shape points; m ∈ R+ , p ∈ P and v ∈ V are, resp., the
mass, the centre of mass3 and the velocity of σ. All possible basic shapes are
ranged over by σ, σ 0 , · · · . We also define the boundary B(σ) of σ to be the
subset of points of V that are on the surface of σ 4
Note that basic shapes are very simple convex shapes. They can be represented by means of suitable and efficient data structures and are handled by
the most popular algorithms for motion simulation, collision detection and
response [13]. Three dimensional shapes of any form can be approximated
2

From a syntactical representation point of view, we assume that V is finitely represented by a suitable data structure, such as a formula or a set of vertices.
3
We actually need only a reference point. Thus, any other point in V can be chosen.
4
Note that we consider only closed shapes, i.e. they contain their boundary.

6

- with arbitrary precision - by composing basic shapes: the composition of
two shapes corresponds to the construction of a third shape by “gluing the
two components on a common surface. This concept is generalized by the
following definition.
Definition 2 (3D shapes) The set S of the 3D shapes, ranged over by
S, S 0 , · · · , is generated by the grammar:
S ::= σ S hXi S
where σ is a basic shape and X ⊆ P. If S = σ = hV, m, p, vi, we define
P(S) = V , m(S) = m, R(S) = p, v(S) = {v} to be, resp., the set of points,
the mass, the reference point and the velocity of S. If S = S1 hXi S2 is a
compound shape, then: P(S) = P(S1 ) ∪P(S2 ), m(S) = m(S
 1 ) + m(S2 ),
R(S) = m(S1 ) · R(S1 ) + m(S2 ) · R(S2 ) / m(S1 ) + m(S2 ) 5 and v(S) =
v(S1 ) ∪ v(S2 ). Finally, the boundary of S is defined to be the set B(S) =
B(S1 ) ∪ B(S2 ) \ {x ∈ P | x is interior of P(S1 hXi S2 )}, where a point
x ∈ V ⊆ P is said to be interior if there exists an open ball with centre x
which is completely contained in V .
In this paper we only consider shapes that are well-formed according to
the following definition.
Definition 3 (Well-formed shapes) Each basic shape σ is well-formed.
A compound shape S1 hXi S2 is well-formed iff:
1. both S1 and S2 are well-formed;
2. the set X = P(S1 ) ∩ P(S2 ) is non-empty and equal to B(S1 ) ∩ B(S2 );
3. v(S1 hXi S2 ) is a singleton {v}6 where v = v(S1 ) = v(S2 ).
Below we say that two shapes S1 and S2 interpenetrate each other if there
exists a point x that is interior of both P(S1 ) and P(S2 ). In other terms,
they interpenetrate iff the set X = P(S1 ) ∩ P(S2 ) 6= ∅ is not a subset of
B(S1 ) ∩ B(S2 ). If S = S1 hXi S2 is well-formed, X is said to be the surface
of contact between S1 and S2 ; moreover, each x ∈ X is a point of contact.
5
Again for simplicity, we use the centre of mass as the reference point. Any other point
can also be chosen.
6
With abuse of notation, throughout the paper, we write v(S) also to refer to the
element v of the singleton {v} as this is not ambiguous when S is well-formed.

7

Condition (2) guarantees that well-formed compound shapes touch but
do not interpenetrate; the surface of contact X is always on the boundary of
both S1 and S2 . It can be a single point, a segment or a surface, depending
on where the two shapes are touching without interpenetrating. Most of
the time X is a (subset of) a feature of the basic shapes composing the
3D shape, i.e., a face, an edge or a vertex. Condition (3) imposes that all
the shapes forming a compound shape have the same velocity; thus, the
compound shape moves as a unique body.
A compound 3D shape S can be represented in a number of different
ways by rearranging its basic shapes and surfaces of contact. All these possible representation are ‘equivalent’ w.r.t. the structural congruence defined
below.
Definition 4 (Structural Congruence of 3D Shapes) The structural
congruence relation over S, denoted by ≡S , is the smallest relation that satisfies the following rules:
1. S1 hXi S2 ≡S S2 hXi S1 ;
2. (S1 hXi S2 ) hY i S3 ≡S S1 hXi (S2 hY i S3 ) provided that the surface of
contact Y ⊆ B(S2 ) ∩ B(S3 ).
The next example shows how the particular features of Shape Calculus
can be used to construct a model in a well-known biological scenario.
Example 1 (A Biological Example) The glycolysis pathway is part of
the process by which individual cells produce and consume nutrient molecules.
It consists of ten sequential reactions, all catalyzed by a specific enzyme. We
focus, in this example, on the first reaction that can be described as
−−
*
glucose, ATP )
−
− glucose-6-phosphate, ADP, H+
where an ATP is consumed and a molecule of glucose (GLC) is phosphorylated to glucose 6-phosphate (G6P), releasing an ADP molecule and a positive
hydrogen ion (Hydron).
The enzyme catalyzing this first reaction is Hexokinase (HEX). GLC,
G6P, ATP, ADP and H+ are metabolites. Both enzymes and metabolites
are autonomous cellular entities that continuously move within the cytoplasm. The transformation of a metabolite into the one that follows in the
“pipeline” of the pathway (in this case, GLC into G6P) depends on the meeting (collision in binding sites) of the right enzyme (in this example HEX)
with the right metabolites, in this example GLC and ATP. The order of these
8

Figure 3: A network of 3D processes for describing the first reaction of the
glycolysis pathway.
bindings does not matter. After this binding the reaction takes place and the
products7 are released in the cytoplasm. A special case occurs when the enzyme has bound one metabolite and an environmental event makes it release
the metabolite and not proceed to the completion of the reaction.
We model the shape of HEX, which we denote with Sh , by a polyhedron
approximating its real shape and mass, available at public databases (e.g. [1]).
Fig. 3 shows a network of 3D processes in which there are two hexokinases
and some GLC, G6P, ATP and ADP 3D processes. Note that we use a
unique kind of shape for GLC ad G6P, denoted by Sg , and another unique
kind of shape for ATP and ADP, denoted Sa . They will be distinguished by
their behaviours.
Note that modelling of biochemical reactions with our calculus is very
different from the usual ODE-based approach. This is because the Shape
Calculus embeds concepts and features of a particle-based, individual-based
and spatial geometric approach and we wanted to show, in a relatively simple
and well-known scenario, how all these concepts and features can be used.

3.1

Trajectories of Shapes

The general idea of the Shape Calculus is to consider a three-dimensional
space in which several shapes reside, move and interact. One of the choices
7

In this example we neglect the hydron.

9

to be made is how the velocity of each shape changes over time. We believe
that a continuous updating of the velocity - that would be a candidate
for an ‘as precise as possible approach of modelling - is not a convenient
choice. The main reason is the well-known compromise between the benefits
of approximation and the complexity of precision. Our choice, quite common
also in computer graphics [13], is to approximate a continuous trajectory of
a shape with a polygonal chain, i.e. a piecewise linear curve in which each
segment is the result of a movement with a constant velocity. The vertices
of the chain corresponds to velocity updates.
To this purpose we define a global parameter ∆ ∈ R+ , called movement
time step, that represents the maximum period of time after which the velocities of all shapes are updated. The quantification of ∆ depends on the
desired degree of approximation and also on other parameters connected to
collision detection (see Section 3.2). In some situations, the time of updating can be shorter than ∆ because, before that time, collisions between
moving shapes can occur. These collisions must be resolved and the whole
system must re-adapt itself to the new situation. The time domain T = R+
0
is then divided into an infinite sequence of time steps ti such that t0 = 0
and ti ≤ ti−1 + ∆ for all i > 0. An example in [5] (cf. Section 2) shows in
more details how the timeline can be broken up into such time instants.
In the calculus, the updating of velocities is performed by exploiting a
function steer : T → (S ,→ V) that describes how the velocity of all existing
shapes (i.e. all shapes that are currently moving in the space) at each time
t is changed. We assume that, at any given time instant t ∈ T, steer t S is
undefined iff shape S does not exist and, hence, its velocity has not to be
changed.
This approach provides us with the maximal flexibility for defining motion. Static shapes are those shapes whose velocity is always zero8 . A
gravity field can be simulated by updating the velocities according to the
gravity acceleration. A Brownian motion can be simulated by choosing a
random 3D direction and then defining the length of the vector w.r.t. the
mass and/or the volume of the shape. In this paper, we do not consider
movements due to rotations. However, this kind of movements can be easily
added to our shapes by assigning an angular velocity and a moment of inertia to a shape and then by performing a compound motion of translation
and rotation along the movement time step.
8

To represent walls, we also need to assign an infinite value to the mass of these objects,
otherwise they can be moved anyway due to collisions.

10

Let us define now some useful notation and properties.
Definition 5 (Evolution of shapes over time) Let S ∈ S and t ∈ T;
S + t, i.e. the shape S after t time units, is defined by induction on S:
Basic:
Comp:

hV, m, p, vi + t = hV + (t · v), m, p + (t · v), vi
(S1 hXi S2 ) + t = (S1 + t) hX + t · v(S)i (S2 + t)

Definition 6 (Updating shape velocity) Let S ∈ S and w ∈ V. We
define the shape S|[w]|, i.e. S whose velocity is updated with w, as follows:
Basic:
Comp:

hV, m, p, vi|[w]| = hV, m, p, wi
(S1 hXi S2 )|[w]| = (S1 |[w]|) hXi (S2 |[w]|)

The following result comes directly from Def. 3.
Proposition 1 Let S ∈ S, t ∈ T and w ∈ V. If S is well-formed then S + t
and S|[w]| are well-formed.
Our intent is to represent a lot of shapes moving simultaneously in space
as described above. Inevitably, this scenario produces collisions between
shapes when their trajectories encounter.

3.2

Collision Detection

There is a rich literature on collision detection systems, as this problem is
fundamental in popular applications like computer games. Good introductions to existing methods for efficient collision detection are available and
we refer to Ericson [13] and references therein for a detailed treatment.
For our purposes, it is sufficient to define an interface between our calculus and a typical collision detection system. We can then choose one of
them according to their different characteristics, e.g. their applicability in
large-scale environments or their robustness. It must be said, however, that
the choice of the collision detection system may influence the kind of basic (or compound) shapes we can use, as, for instance, some systems may
require the use of only convex shapes to be more efficient9 .
Typically, a collision detection algorithm assumes to start in a situation
in which shapes do not interpenetrate. Then it tries to move all the shapes
9

The basic shapes that we consider in Definition 1 are typically accepted by most of
the collision detection systems.

11

Figure 4: Some steps to determine the first time of contact between two
shapes.
of a little10 time step - that we have already introduced as the movement
time step ∆ - and check if interpenetrations occurred11 . If so, it tries to
consider only half of the original time step and repeat the interpentration
check, i.e. it performs a binary search of the first time of contact t between
two or more shapes, with some degree of approximation. Fig. 4 shows these
steps. In case (a) the passage of the whole ∆ results in an interpenetration.
Then, in (b) the passage of ∆/2 is tried resulting into a non-contact. After
some iterations the situation in (c) is reached.
In addition to the first time of contact, a collision detection algorithm
usually outputs the shapes that are colliding, i.e. are touching without interpenetrating after t, and some information about the surfaces or points of
contact. We now define precisely what we expect to obtain from a collision
detection system.
Definition 7 (First time of contact) Let I be a non-empty finite set of
indexes and let {Si }i∈I be a set of well-formed shapes such that for all i, j ∈ I,
Si and Sj do not interpenetrate (see Def. 3). The first time of contact of
the shapes Si , denoted Ftoc({Si }i∈I ), is a number t ∈ T such that:
10
The time step must be chosen little enough to avoid that any two shapes, at their
possible maximum velocity, start in a non-interpenetration state, engage in an interpenetration and exit from the interpenetration state in a single time step duration.
11
Typically, the major efforts of optimization are concentrated in this step since the
number of checks is, in the worst case, O(N 2 ) - where N is the number of shapes in the
space - but the shapes that are likely to collide are only those that are very close to each
other.

12

1. for all t0 ∈ T, 0 ≤ t0 ≤ t and for all i, j ∈ I, Si + t0 and Sj + t0 do not
interpenetrate;
2. there exist i, j ∈ I, with i 6= j, such that B(Si + t) ∩ B(Sj + t) 6= ∅, i.e.,
some shapes are touching at t;
3. for all  > 0 there exists δ, 0 < δ < , and i, j ∈ I, with i 6= j, such
that Si + (t + δ) and Sj + (t + δ) interpenetrate, i.e., in t some shapes
are touching and any further movement makes them to interpenetrate.
Note that such a definition allows shapes that are touching without interpenetrating, and with velocities that do not make them to interpenetrate
(e.g., the same velocity), to move without triggering a first time of contact.
This will be useful in Section 5 when we split previously compound shapes.
Indeed, after the split these shapes have the same velocity and, hence, do
not affect the next first time of contact.
Definition 8 (Collision information) Let {Si }i∈I be a set of well-formed
shapes and let t = Ftoc({Si }i∈I ) be their first time of contact. The set of
colliding shapes after time t is denoted by colliding({Si }i∈I ) ⊆ S × S × ℘(P).
A tuple hSi , Sj , Xi ∈ colliding({Si }i∈I ) iff:
1. P(Si + t) ∩ P(Sj + t) is non-empty and is equal to B(Si + t) ∩ B(Sj + t);
2. for all  > 0 there exists δ, 0 < δ < , such that Si + (t + δ) and
Sj + (t + δ) interpenetrate.

3.3

Collision Response

In this section, we briefly discuss the problem of collisions response [15],
i.e. how collisions, once detected, can be resolved. We distinguish between
elastic collisions (those in which there is no loss in kinetic energy) and perfectly inelastic ones (in which kinetic energy is fully dissipated)12 . After an
elastic collision, the two shapes will proceed independently to each other
but their velocities will be changed according to the laws for conservation
of linear momentum and kinetic energy - Equations (1)-(2) in Def. 9. On
the contrary, two shapes that collide inelastically will bind together and will
move as a unique body whose velocity is given by the law for conservation
of linear momentum only - Equation (3), in Def. 9.
12

Other different kinds of collisions can be easily added to the calculus provided that
the corresponding collision response laws are given.

13

Definition 9 (Collisions) Let S1 , S2 ∈ S and let X ⊆ P be a surface of
contact between them. If X is neither an edge nor a vertex of S1 , the velocities w1 and w2 of these shapes after an elastic collision in X are given
by:
(1) w1 = v(S1 ) −

λ
·n
m(S1 )

(2) w2 = v(S2 ) +

λ
·n
m(S2 )

where n is the normal of contact away from X ⊆ B(S1 ), i.e. the unit vector
perpendicular to the face of S1 that contains X, and
λ=2

m(S1 ) m(S2 ) v(S1 ) · n − v(S2 ) · n
m(S1 ) + m(S2 )
n·n

If X is either an edge or a vertex of S1 , n is the normal of contact away from
the shape S2 and velocities w1 and w2 are obtained by means of symmetric
X
equations. In both cases, we write S1 ←→e S2 to denote the pair of velocities
(w1 , w2 ). If S1 and S2 collide inelastically in the surface of contact X, they
X

will bind together as a unique body whose velocity (denoted with S1 ←→i S2 )
is given by:
(3) v =

4

m(S2 )
m(S1 )
· v(S1 ) +
· v(S2 )
m(S1 ) + m(S2 )
m(S1 ) + m(S2 )

3D Processes

In this section we introduce the timed process algebra whose terms describe the internal behaviour of our 3D shapes. This is a variation of
Timed CCS [21], where basic actions provide information about binding
capability and splits of shape bonds. We use the following notation. Let
Λ = {a, b, · · · } be a countably infinite set of channels names (names, for
short) and Λ = {a | a ∈ Λ} its complementation; by convention we assume
a = a for each name a. Elements in A = Λ ∪ Λ are ranged over by α, β, · · · .
Binding capabilities are represented by channels, i.e. pairs hα, Xi where
α ∈ A is a name and X is a surface of contact. Intuitively, a surface of
contact is a portion of space (usually, a subset of the boundary of a given
3D shape) where the channel itself is active and where binding with other
processes are possible. Names introduce a notion of compatibility between
channels useful to distinguish between elastic and inelastic collisions. If β =
α and X ∩ Y 6= ∅ we say that the channels hα, Xi and hβ, Y i are compatible,
14

written hα, Xi ∼ hβ, Y i. Otherwise, hα, Xi and hβ, Y i are incompatible
which we write as hα, Xi 6∼ hβ, Y i.
We also introduce two different kinds of actions that represent splits of
shape bonds. In particular, we distinguish between weak-split actions of the
form ω(α, X) and strong-split actions of the form ρ(α, X). With an abuse
of notation, two weak-split actions ω(α, X) and ω(β, Y ) (as similarly for
the strong-split actions ρ(α, X) and ρ(β, Y )) are compatible if so are the
channels hα, Xi and hβ, Y i. We will see that a synchronization between a
pair of compatible weak-split actions results in a weak-split operation, while
synchronizations between multiple pairs of compatible strong-split actions
correspond to a strong-split operation. These operations behave differently
w.r.t. to time passing since the latter operation cannot time pass further,
while the former one can be arbitrarily delayed.
Let C be the set of all channels, ω(C) = {ω(α, X) | hα, Xi ∈ C} and
ρ(C) = {ρ(α, X) | hα, Xi ∈ C} be the sets of weak-split actions and strongsplit actions, resp. Our processes perform basic and atomic actions that
belong to the set Act = C ∪ ω(C) ∪ ρ(C) whose elements are ranged over
by µ, µ0 , · · · . We finally assume a countably infinite collection K of process
name or process constants.
Definition 10 (Shape behaviours)
The set of shape behaviours, denoted by B, is generated by the following
grammar:
B ::= nil hα, Xi.B ω(α, X).B ρ(L).B (t).B B + B K
where hα, Xi ∈ C, L ⊆ C (non-empty) whose elements are pairwise incompatible (i.e. for each pair hα, Xi, hβ, Y i ∈ L it is hα, Xi 6∼ hβ, Y i), t ∈ T
and K is a process name in K.
A brief description of our operators now follows. nil is the Nil-behaviour,
it can not perform any action but can let time pass without limits. A
trailing nil will often be omitted, so e.g. we write ha, Xi.ω(a, X) to abbreviate
ha, Xi.ω(a, X).nil. hα, Xi.B and ω(α, X).B are (action-)prefixing known
from CCS; they evolve in B by performing the actions hα, Xi and ω(α, X),
resp. hα, Xi.B exhibits a binding capability along the channel hα, Xi, while
ω(α, X).B models the behaviour of a shape that, before evolving in B, wants
to split a single bond established via the channel hα, Xi. ρ(L).B is the
strong-split operator; it can evolve in B only after the execution of all strongsplit actions ρ(α, X) with hα, Xi ∈ L. The delay-prefixing operator (t).B
15

µ ∈ C ∪ ω(C)
Nilt
nil

t

Preft
nil
B1

Sumt

t

B10

B2

t

Strt

t

µ.B

µ.B

B20

t

Deft
K

t

ρ(L).B

t0 ≥ t
Delt

− B10 + B20
B1 + B2 →
B

ρ(L).B

t

B0

t

B0

(t0 ).B

t

(t0 − t).B

def

if K = B

Table 1: Temporal behaviour of B’s terms
(see [21]) introduces time delays in 3D processes; t ∈ T is the amount of
time that has to elapse before the idling time is over (see rules Delayt and
Delaya in Tables 1 and 2). Finally, B1 + B2 models a non-deterministic
choice between B1 and B2 and K is a process definition.
In the remainder of this paper, we use processes in B to define the internal
behaviour of 3D shapes. For this reason, we assume that sites in binding
capabilities, as well as in weak- and strong-split actions, are expressed w.r.t.
the local coordinate system whose origin is the reference point of the shape
where they are embedded in.
Definition 11 (Operational semantics of shape behaviours) The
t
SOS-rules that define the temporal transition relations
⊆ (B × B) for
t ∈ T, that describe how shape behaviours evolve by letting time t pass, are
t
t
t
provided in Table 1. We write B
B 0 if (B, B 0 ) ∈ and B
if there is
t
0
0
B ∈ B such that (B, B ) ∈ . Similar conventions will apply later on. Rules
µ
in Table 2 define the action transition relations −
→⊆ (B × B) for µ ∈ Act.
These transitions describe which basic actions a shape behaviour can perform.
Most of the rules in Table 1 are those provided in [21]. Rules Preft
and Strt state that processes like hα, Xi.B, ω(α, X).B and ρ(L).B can be
arbitrarily delayed. The only rules in Table 2 worth noting are those defining the functional behaviour of the strong-split operator. By Rules Str1
and Str2 , if hα, Xi ∈ L then ρ(L).B can do a ρ(α, X)-action and evolve
either in B (if L = {hα, Xi}) or in ρ(L\{hα, Xi}).B (otherwise). Rule Str3
16

µ

Prefa

µ

B−
→ B0

µ ∈ C ∪ ω(C)
Dela

µ

µ.B −
→B

B1 −
→ B0
Suma

µ

(0).B −
→ B0

µ

B−
→ B0
Defa

def

if K = B

µ

K−
→ B0

L = {hα, Xi}
Str1

ρ(α,X)

ρ(L).B −−−−→ B
ρ(α,X)

B −−−−→ B 0

L = {hα, Xi} ∪ L0 L0 6= ∅
Str2

µ

B1 + B2 −
→ B0

Str3

ρ(α,X)

ρ(L).B −−−−→ ρ(L0 ).B

ρ(α,X)

ρ(L).B −−−−→ ρ(L).B 0

Table 2: Functional behaviour of B-terms
is needed to handle arbitrarily nested terms, e.g. ρ({ha, X}).ρ({hb, Y }).B.
Other rules are as expected.
Now we are ready to define 3D processes, i.e. simple or compound shapes
whose behaviour is expressed by a process in B.
Definition 12 (3D processes) The set 3DP of 3D processes is generated
by the following grammar:
P ::= S[B] P ha, Xi P
where S ∈ S, B ∈ B, a ∈ Λ and X is a non-empty subset of P. The shape
of each P ∈ 3DP is defined by induction on P as follows:
Basic:
Comp:

shape(S[B]) = S
shape(P ha, Xi Q) = shape(P ) hXi shape(Q)

We also define v(P ) = v(shape(P )) and B(P ) = B(shape(P )). Below we ofX
X
X
ten write P ←→i Q and P ←→e Q as shorthand for shape(P ) ←→i shape(Q)
X
and shape(P ) ←→e shape(Q), resp. Finally, P |[v]| is the 3D process we obtain by updating P ’s velocity as follows:
Basic:
Comp:

(S[B])|[v]| = (S|[v]|)[B]
(P ha, Xi Q)|[v]| = (P |[v]|) ha, Xi (Q|[v]|)

We finally write steer t P to denote P |[steer t shape(P )]|. We say that a
basic process S[B] is well-formed iff the shape S is well-formed and, for each
17

X ⊆ P that occurs in B, global(X, R(S)) ⊆ B(S). A compound process
P ha, Xi Q is well-formed iff P and Q are well-formed, v(P ) = v(Q) and
the site X expressed w.r.t a global coordinate system is a non-empty subset
of B(P ) ∩ B(Q). Note that this also means that the set P(P ) ∩ P(Q) is nonempty and equal to B(P ) ∩ B(Q). Later on in this paper we only consider
well-formed processes.
We can state the following proposition as an easy consequence of shapes
and 3D processes well-formedness.
Proposition 2 For each P ∈ 3DP well-formed, shape(P ) is well-formed.
Let us model the molecules involved in the reaction of Example 1 as 3D
processes.
Example 2 (3D Processes for HEX, GLC and AT P ) An Hexokinase
def

molecule is modeled as HEX = Sh [HEX] where:
HEX = hatp, Xha i.HA + hglc, Xhg i.HG,
HA = ω(atp, Xha ).HEX + (th ).hglc, Xhg i.ρ({hatp, Xha i, hglc, Yhg i}).HEX,
HG = ω(glc, Xhg ).HEX + (th ).hatp, Xha i.ρ({hatp, Xha i, hglc, Yhg i}).HEX,
and Xha , Yhg are the surfaces of contact shown in Fig. 3. AT P = Sa [ATP]
models an ATP molecule where:
ATP = hatp, Xah i.((ta ).ρ({hatp, Xah i}).ADP + ω(atp, Xah ).ATP)
and the surface of contact Xah is the whole boundary B(Sa ).The process
modelling a molecule of glucose is similar: GLC = Sg [GLC] where
GLC = hglc, Xgh i.((tg ).ρ({hglc, Xgh i}).G6P + ω(glc, Xgh ).GLC
We leave unspecified the behaviours G6P and ADP.
HEX has two channels hatp, Xha i and hglc, Yhg i to bind, resp., with an
ATP and a GLC molecule. By performing an action hatp, Xha i, HEX evolves
in HA. HA can perform either a weak-split action ω(atp, Xha ) to come back
to HEX, or can wait at most th units of time, perform hglc, Yhg i and then
evolve in ρ({hatp, Xha i, hglc, Yhg i}).HEX. Now, two strong-split actions are
enabled after which we come back to HEX. Notice that, after an action
hglc, Yhg i, HEX becomes HG that behaves symmetrically.
An ATP molecule performs a hatp, Xah i-action, waits tr units of time,
and then can release the bond established on the channel hatp, Xah i – and
thus return free as ATP – or can participate in the reaction and become an
ADP. As we will see in Section 5, the result is the split of the complex in the
18

three original shapes whose behaviours are HEX, ADP and G6P, resp. We
omit the description of the behaviour of GLC since it is similar to that of
ATP.
We are ready to define the timed operational semantics of 3D processes.
Definition 13 (Transitional semantics of 3D processes) Rules in Tat
ble 3 define the transition relations
⊆ (3DP × 3DP) for t ∈ T, and
µ
−
→⊆ 3DP × 3DP for µ ∈ Act. Two 3D processes P and Q are said to
hα,Xi

hα,Y i

be compatible, written P ∼ Q, if P −−−→ and Q −−−→ for some compatible
channels hα, Xi and hα, Y i; otherwise, P and Q are incompatible that we
ρ
ω
denote with P 6∼ Q. Below, we often write P −
6→ and P −
6 → as shorthand for
ρ(α,X)

ω(α,X)

P 6−−−−→ and P −
6 −−−→, resp., for any hα, Xi.
Essentially, rules in Table 3 say that a 3D process inherits its functional
and temporal behaviour from the B-terms defining its internal behaviour.
But now sites of binding capabilities and split actions are expressed w.r.t.
a global coordinate system (see rules Basicc and Basics ). For simplicity,
we have omitted a rule defining which weak-split action a basic process can
perform. This can be obtained from rule Basicw by replacing each ρ()action with a corresponding ω()-action. It is worth noting that, due to rule
Compa2 , some of the hα, Y i-actions performed by P (by Q) can be prevented
in P ha, Xi Q since, due to binding a part (or all) of Y has became interior
because it is covered by a piece of Q (of P respectively) the surface of contact
Y 6⊆ B(P ha, Xi Q) and, hence the corresponding channel is no more active.
We have also omitted symmetric rules for Compa1 and Compa2 for the
actions of Q.
The following proposition (see Appendix B for the proof) shows that 3D
µ
t
processes well-formedness is closed w.r.t. transitions
and −
→.
Proposition 3 Let P ∈ 3DP well-formed. Either P
Q ∈ 3DP well-formed.

t

µ

Q or P −
→ Q implies

At this stage a key observation is that the operational rules in Table 3
do not allow synchronization between components of compound process that
proceed independently to each other. Consider, as an example,
P = Sp [ρ({a, Xp }).Bp ],
19

B
Basict
S[B]
P

t

P0

Q

t

t

B0

(S + t)[B 0 ]

Q0

Compt

X 0 = X + (t · v(P ))
t

P ha, Xi Q
hα,Xi

B −−−→ B 0
Basicc

t

P 0 ha, X 0 i Q0

Y = global(X, R(S))
hα,Y i

S[B] −−−→ S[B 0 ]
ρ(α,X)

B −−−−→ B 0
Basics

Y = global(X, R(S))
ρ(α,Y )

S[B] −−−−→ S[B 0 ]
ρ(α,Y )

P −−−−→ P 0
Comps

ρ(α,Y )

P ha, Xi Q −−−−→ P 0 ha, Xi Q
ω(α,Y )

P −−−−→ P 0
Compw

ω(α,Y )

P ha, Xi Q −−−−→ P 0 ha, Xi Q
hα,Y i

P −−−→ P 0
Compc

Y ⊆ B(P ha, Xi Q)
hα,Y i

P ha, Xi Q −−−→ P 0 ha, Xi Q

Table 3: Functional and temporal behaviour of 3DP-terms

20

Q = Sq [ρ({a, Xq }).Bq ], and P ha, Xi Q
where X = Xp0 ∩ Xq0 and, for each i ∈ {p, q}, Xi0 is the site Xi w.r.t. a global
coordinate system, i.e. Xi0 = global(Xi , R(Si )). As stand-alone processes,
P and Q can perform two compatible strong-split actions, namely ρ(a, Xp0 )
and ρ(a, Xq0 ) and evolve, resp., in Sp [Bp ] and Sq [Bq ]. As a consequence,
P ha, Xi Q becomes either Sp [Bp ] ha, Xi Q or P ha, Xi Sp [Bq ].
But these actions are compatible and, according to the intuition given
so far, P and Q have to synchronize on their execution in order to split the
bond ha, Xi. In other terms, a strong-split operation is enabled; such an operation must be performed before time can pass further and must produce as
a result two independent 3D processes, i.e. the network of 3D processes (see
Section 5) that contains both Sp [Bp ] and Sq [Bq ]. Similarly, we would allow
synchronizations between compatible weak-split action in order to perform
a weak-split operation. To properly deal with this kind of behaviours some
technical details are still needed. We first allow synchronization on comρ(a,X)

patible split actions by introducing the transition relations ⇒ and

ω(a,X)

⇒ .

ρ(a,X)

Intuitively, we want that P ha, Xi Q ⇒ Sp [Bp ] ha, Xi Sq [Bq ]. Now, we
can ‘physically’ remove the bond ha, Xi (this will be done by exploiting the
function split over 3D processes we provide in the next section) and obtain
the network of processes we are interested in.
Definition 14 (Semantics of strong and weak splits) The SOS-rules
ρ(a,X)

that define the transition relations ⇒ ⊆ 3DP × 3DP where ρ(α, X) ∈ ρ(C)
are given in Table 4. As usual, symmetric rules have been omitted. We
ω(a,X)

also omit the rules defining the transition relations ⇒ ⊆ 3DP × 3DP for
ω(a, X) ∈ ω(C) since these can be obtained from those in Table 4 by replacing
each action ρ(-) with the corresponding action ω(-).
Recall that strong-split operations require simultaneous split of multiple
bonds. In this case, all the components involved in the reaction must all
together be ready to synchronize on a proper set of compatible strong-split
actions. Consider a more complex example
P = Sp [ρ({ha, Xp i, hb, Yp i}).Bp ],
Q = Sq [ρ({ha, Xq i}).Bq ],
R = Sr [ρ({hb, Yr i}).Br ], and (P ha, Xi Q) hb, Y i R
21

where X = Xp0 ∩ Xq0 and Y = Yp0 ∩ Yr0 (also in this case we write Xi0 ,
for i ∈ {p, q, r}, to represent the site Xi in a global coordinate system). P
can synchronize with Q and R to split, resp., the bonds ha, Xi and hb, Y i.
Indeed, rules in Table 4 implies that
(P ha, Xi Q) hb, Y i R

ρ(a,X)

⇒

ρ(b,Y )

⇒

(Sp [ρ({hb, Yp i}).Bp ] ha, Xi Sq [Bq ]) hb, Y i R
(Sp [Bp ] ha, Xi Sq [Bq ]) hb, Y i Sr [Br ]

After that, all ‘pending strong-split requests’ of (P ha, Xi Q) hb, Y i R are
satisfied. We say that such a compound process is able to complete a reaction.
If it was, for instance, R = Sr [(t).ρ({hb, Yr i}).Br ] then (P ha, Xi Q) hb, Y i R
would not have been able to complete a reaction, since (at least) one involved
component, i.e. R, would not have been able to contribute to the reaction
before than t units of time. In such a case, the bonds can not be spit at all.
This concept is formalized by the definition below.
Definition 15 (Bonds of 3DP-terms) The function bonds : 3DP → ℘(C)
returns the set of bonds that are currently established in P . It can be defined
by induction on P ∈ 3DP:
Basic:
Comp:

bonds(S[B]) = ∅
bonds(P ha, Xi Q) = bonds(P ) ∪ bonds(Q) ∪ {ha, Xi}
ρ(a,X)

By an easy induction on P we can prove that P ⇒ implies ha, Xi ∈
bonds(P ). Moreover, we say that P ∈ 3DP is able to complete a reaction,
ρ

which we write as P &, iff either (1) P −
6→, or (2) P
ρ(a, X) and Q such that Q &.

ρ(α,Xp )

P −−−−−→ P 0
StrSync

ρ(α,Xq )

Q −−−−−→ Q0

ρ(a,X)

⇒

Q for some

α ∈ {a, a} X = Xp ∩ Xq

ρ(a,X)

P ha, Xi Q ⇒ P 0 ha, Xi Q0
P
StrPar

ρ(b,Y )

⇒ P0

ρ(b,Y )

P ha, Xi Q ⇒ P 0 ha, Xi Q

Table 4: Transitional semantics for strong-split actions
22

Finally, if P is able to complete a reaction and there is at a least a bond
ρ
that has to be strongly split (i.e. if P −
6→ does not hold), a reaction can
actually take place and, as a consequence, time cannot pass further. Below
we restrict the timed operational semantics of 3D processes as it has been
defined in Def. 13 in order to take this aspect into account.
t

Definition 16 Let P ∈ 3DP. We say that P →
− Q if P
ρ
P −
6→ or P is not able to complete a reaction.

t

Q and either

Proposition 4 states that the function split is well-defined up to structural
congruence over 3D processes we define below.
Definition 17 (Structural congruence over 3D processes) We define the structural congruence over processes in 3DP, which we denote by ≡P ,
as the smallest relation that satisfies the following axioms:
- S[B] ≡P S 0 [B] provided that S ≡S S 0 ;
- P ha, Xi Q ≡P Q ha, Xi P ;
- P ≡P Q implies P ha, Xi R ≡P Q ha, Xi R;
- Y ⊆ B(Q) ∩ B(R) implies (P ha, Xi Q) hb, Y i R ≡P P ha, Xi (Q hb, Y i R).
Proposition 4 Let P ∈ 3DP well-formed. If ha, Xi ∈ bonds(P ) there is a
well-formed 3D process Q ha, Xi R ≡P P .
We also need the following closure result.
Proposition 5 Let P, Q ∈ 3DP and µ ∈ ω(C) ∪ ρ(C). Then:
µ
1. P ⇒ Q implies shape(Q) = shape(P );
µ
2. P well-formed and P ⇒ Q implies Q well-formed.

5

Networks or 3D processes

Now we can define a network of 3D processes as a collection of 3D processes
moving in the same 3D space.
Definition 18 (Networks of 3D processes) The set N of networks of
3D processes (3D networks, for short) is generated by the grammar:
N ::= Nil P
23

N kN

where P ∈ 3DP. Given a finite set of indexes I, we often write (k Pi )i∈I
to denote the network that consists of all Pi with i ∈ I. We assume that
I = ∅ implies (k Pi )i∈I = Nil. For N = (k Pi )i∈I we let Si = shape(Pi ),
for i ∈ I, and define colliding(N ) as the set of all tuples hPi , Pj , Xi such
that hSi , Sj , Xi ∈ colliding({Si }i∈I ) (see Def. 8). A network N = (k Pi )i∈I
is said to be well-formed iff each Pi is well-formed and, for each pair of
distinct processes Pi and Pj , the shapes Si and Sj do not interpenetrate.
Moreover, we extend the definition of steer on networks in the natural way,
i.e. steer t (k Pi )i∈I = (k steer t Pi )i∈I .
In our running example we construct a network of processes containing
a proper number of HEX, ATP and GLC processes in order to replicate the
conditions in a portion of cytoplasm.
Definition 19 (Splitting bonds) The function split : 3DP × ℘(C) → N
is defined as follows: If ha, Xi ∈ bonds(P ) ∩ C and P ≡P Q ha, Xi R then
split(P, C) = split(Q, C) k split(R, C); if, otherwise, bonds(P ) ∩ C = ∅, then
split(P, C) = P .
It is worth noting that split shapes maintain the same velocity until the
next occurrence of a movement time step. As we mentioned above, this is
not a problem because they will not trigger a collision and, thus, a shorter
first time of contact.
Proposition 6 Let P ∈ 3DP well-formed and C ⊆ C. Then split(P, C) is a
well-formed network of 3D processes.
Definition 20 (Semantics of weak- and strong-split operation) Let
ρ
P ∈ 3DP a 3D process. If P &, we write that P −
→ N ∈ N iff there is a non
empty set of channels C = {ha1 , X1 i, · · · , han , Xn i} ⊆ bonds(P ) such that
P = P0

ρ(a1 ,X1 )

⇒

P1 · · ·

ρ(an ,Xn )

⇒

ρ

Pn , Pn −
6→ and N = split(Pn , C). Similarly,

ω

P −
→ N iff there is a channel ha, Xi ∈ bonds(P ) such that P
N = split(Q, {ha, Xi}).

ω(a,X)

⇒

Q and

Since weak-split operations are due to a synchronization between just
a pair of 3D processes, condition ‘P is able to complete a reaction’ is not
needed, but ‘P

ω(a,X)

⇒ Q’ suffices to our aim.

Example 3 Let us consider P = H hatp, Xi (A hglc, Y i G) where:
24

H = Sh [ ρ({hatp, Xha i, hglc, Yhg i}).HEX ],
A = Sa [ ρ({hatp, Xah i}).ADP + ω(atp, Xah ).ATP ],
G = Sg [ρ({hglc, Ygh i}).G6P + ω(glc, Ygh ).GLC],
0 ∩ X 0 = X (here X 0 and X 0 are the sites X
Xha
ha and Xah expressed
ah
ha
ah
w.r.t. a global coordinate system; this convention will be applied later on)
0 ∩ Y 0 = Y . According to the definitions given so far, P is able to
and Yhg
gh
complete a reaction since:

P

ρ(atp,X)

⇒

ρ(glc,Y )

⇒

Sh [ρ({hglc, Yhg i}).HEX] hatp, Xi (Sa [ADP] hglc, Y i G)
Sh [HEX] hatp, Xi (Sa [ADP] hglc, Y i Sg [G6P]) = R

ρ

Moreover, R −
6→ and
split(R, C) = Sa [HEX] k split(Sa [ADP] hglc, Y i Sg [G6P], C)
= Sh [HEX] k (Sa [ADP] k Sg [G6P]) = N
ρ

where C = {hatp, Xi, hglc, Y i}, implies P −
→ N . Moreover, let us note that,
t
t
for each t ∈ T, P
P but P →
6 since since P is able to complete a reaction
−
ρ
and P −
6→ does not hold.
Below we define the temporal and functional behaviour of 3D networks.
We assume that such networks perform basic actions that belong to set
{ω, ρ, κ}, where ω and ρ denote, resp., weak- and strong- split operations as
a unique action (at the network level we only see whether shape bonds can
be split or not) and κ represents system evolutions due to collision response
(see Section 5.1). We also let elements of the set {ω, ρ} ∪ T to be ranged
over by ν, ν 0 , · · · .
Definition 21 (Temporal and Functional Behaviour of N-terms)
t
Rules in Table 5 defines the transition relations →
− ⊆ N × N for t ∈ T and
ν
−
→⊆ N × N for ν ∈ {ω, ρ}. As usual, symmetric rules have been omitted.
A timed trace from N is a finite sequence of steps of the form N =
ν1
νn
t
N0 −→
N1 · · · −→
Nn = M . We also write that N ⇒ M if there is a timed
n
P
ν1
νn
trace N = N0 −→
N1 · · · −→
Nn = M such that t =
{νi | νi ∈ T}.
i=0

25

t

t

N→
− N0
Emptyt

t

Part

Nil →
− Nil

M→
− M0
t

N kM →
− N0 k M0

ν

N−
→ N0
Para

ν

N kM −
→ N0 k M

Table 5: Temporal and functional behaviour of 3D networks
Proposition 7 Let t ∈ T, P ∈ 3DP, N ∈ N, with P and N well-formed.
ω

ρ

1. P −
→ N and P −
→ N implies N ∈ N well-formed.
t

2. N →
− M implies M well-formed;
t

3. N ⇒ M implies M well-formed.

5.1

Collision response

In this section we describe the semantics of collisions response. As already
said, the notion of compatibility between channels (and, hence, processes)
has been introduced to distinguish between elastic and inelastic collision. In
particular, collisions among compatible processes are always inelastic. So,
ha,Xp i

ha,Xq i

if P −−−−→ P 0 and Q −−−−→ Q0 , with ha, Xp i and ha, Xq i compatible, and
P and Q collide in the non-empty site X = Xp ∩ Xq we get a compound
process (P 0 ha, Xi Q0 )|[v]| where the velocity v is provided by Equation (3)
in Def. 9. Vice versa, a collision between two incompatible processes P and
Q is treated as an elastic one. After such a collision, P and Q (actually the
processes we obtain by updating their velocities according to Equations (1)
and (2) in Def. 9) will proceed independently to each other.
To resolve collisions, we introduce two different kinds of reduction rehP,Q,Xi

hP,Q,Xi

lations over 3D networks, namely −−−−−→e and −−−−−→i , where P, Q are
3D processes and X is a surface of contact (see Table 6). Intuitively, if
hP,Q,Xi

hP,Q,Xi

N −−−−−→e M (N −−−−−→i M ), then M is the 3D network we obtain once
an elastic (inelastic, resp.) collision between P and Q in the surface of contact X has been resolved. These reduction relations also use the structural
congruence over 3D networks.

26

Definition 22 (Structural congruence over 3D networks)
The structural congruence over terms in N, that we denote with ≡, is the
smallest relation that satisfies the following axioms:
- Nil k N ≡ N , N k M ≡ M k N and N k (M k R) ≡ (N k M ) k R;
- P k N ≡ Q k N provided that P ≡P Q.
Rule elas in Table 6 simply changes velocities of two colliding but incompatible processes guided by Equations (1) and (2) in Def. 9, while rule inel
joins two compatible processes P and Q to obtain a compound process whose
velocity is given by Equation (3) in Def. 9. Note that we force P and Q to
synchronize on the execution of two compatible actions hα, Xp i and hα, Xq i
before joining them. In rules elas≡ and inelas≡ we also consider structural congruence over nets of processes. In Def. 23 we collect together all the
reduction-steps needed to solve collisions listed in a given set of collisions
colliding(N ); clearly N is a generic 3D network.
Definition 23 (Resolving collisions) Let N ∈ N and hP, Q, Xi a tuple
hP,Q,Xi

hP,Q,Xi

in colliding(N ). N −−−−−→ M if either P ∼ Q and N −−−−−→i M or P 6∼ Q
hP,Q,Xi

and N −−−−−→e M .
κ
Moreover, we write that N −
→ M if either colliding(N ) = ∅ and N = M
or colliding(N ) 6= ∅ and there is a finite sequence of reduction steps N =
hP1 ,Q1 ,X1 i

hPk ,Qk ,Xk i

N0 −−−−−−−→ N1 · · · −−−−−−−→ Nk = M such that:
1. hPi , Qi , Xi i ∈ colliding(Ni−1 ) for each i ∈ [1, k];
2. colliding(Nk ) = ∅.
Let also note that, at any given time t, colliding(N ) can be obtained
from the set of all the pairs of processes in N that are touching at that time.
This set and hence colliding(N ) is surely finite and changes only when we
resolve some inelastic collision (this is because, after an inelastic collision one
or more binding sites can possibly become internal points of a compound
process, and hence are not available anymore). Moreover a collision between
pairs of processes with the same shape can not be resolved twice. This
is either because two processes P and Q have been bond in a compound
process as a consequence of an inelastic collision, or because P and Q collide
elastically and their velocities have been changed according to Equations
27

X

P ←→e Q = (vp , vq )
elas

hP,Q,Xi

(P k Q) k N −−−−−→e (P |[vp ]| k Q|[vq ]|) k N
hP,Q,Xi

N ≡ N0
elas≡

N 0 −−−−−→e M
hP,Q,Xi

N −−−−−→e M
hα,Xp i

hα,Xq i

P −−−−→ P 0
inel

Xp ∩ Xq

Q −−−−→ Q0

α ∈ {a, a} P ←→

i

Q=v

hP,Q,Xp ∩ Xq i

(P k Q) k N −−−−−−−−−→i ((P 0 ha, Xp ∩ Xq i Q0 )|[v]|) k N
hP,Q,Xi

N ≡ N0
inel≡

N 0 −−−−−→i M
hP,Q,Xi

N −−−−−→i M
Table 6: Reaction rules for elastic and inelastic collisions
(1) and (2) in Def. 9 in order to obtain two processes that do not collide
anymore (see Lemma 5 in Appendix C). Thus, we can always decide if there
is a finite sequence of reduction steps that allows us to resolve all collisions
listed in colliding(N ) and hence obtain a network M with colliding(M ) = ∅.
Proposition 8 Let N ∈ N, P, Q ∈ 3DP and X a not-emptyset subset of P.
hP,Q,Xi

Then N well-formed and N −−−−−→ M implies M well-formed.
By iterative applications of Proposition 8 (see Appendix C for the proof)
it is also:
κ

Lemma 1 Let N a well-formed 3D network. Then N −
→ M implies M
well-formed.
We are now ready to define how a network of 3D processes evolves by
performing an infinite number of movement time steps.
Definition 24 (System evolution) Let N, M ∈ N and t, t0 ∈ T. We say
t0

that (N, t) ⇒ (M, t + t0 ) iff one of the following conditions holds:
t0

κ

1. t0 = Ftoc(N ) ≤ ∆ and N ⇒ N 0 −
→ N 00 and M = steer (t + t0 ) N 00 ;
28

t0

2. t0 = ∆ < Ftoc(N ) and N ⇒ N 0 and M = steer (t + t0 ) N 0 .
A system evolution is any infinite sequence of time steps of the form:
t

t

1
2
(N0 , 0) ⇒
(N1 , t1 ) ⇒
(N2 , t1 + t2 ) · · · (Ni−1 ,

i−1
X

t

i
tj ) ⇒
(Ni ,

j=1

i
X

ti+1

tj ) ⇒ · · ·

j=1

Note that, for each i ≥ 1, ti = min{Ftoc(Ni−1 ), ∆} as discussed in
Section 2. Moreover, in order to make sure that processes will never interpenetrate during a system evolution, if Ftoc(Ni−1 ) ≤ ∆, we first resolve all
the collisions that happen after time ti = Ftoc(Ni−1 ) (by means of transition
κ
−
→) and then apply the changes suggested by the function steer as described
in Section 3.1.
Example 4 This example shows a possible evolution of the 3D network
N0 = (HEX k AT P ) k GLC where HEX, AT P and GLC are the 3D processes of Example 2. Below we use the following notation:
- H(t) = (Sh + t)[HEX], A(t) = (Sa + t)[ATP] and G(t) = (Sg + t)[GLC]
for each t ∈ T. Note that HEX = H(0), AT P = A(0) and GLC =
G(0);
- C = ρ({hatp, Xha i, hglc, Xhg i}).HEX and, for any t ≤ th , HA(t) =
ω(atp, Xha ).HEX + (th − t).hglc, Xhg i.C;
- AH(t) = ω(atp, Xah ).ATP + (ta − t).ρ({atp, Xah }).ADP for any t ∈ T
with t ≤ ta ;
- GH(t) = ω(glc, Xgh ).GLC + (tg − t).ρ({glc, Xgh }).G6P for any t ≤ tg .
Let t1 = Ftoc(N0 ) and assume t1 ≤ ∆. By the operational rules, it is
t1
N0 ⇒
H(t1 ) k A(t1 ) k G(t1 ) = N00 . We also assume that colliding(N00 ) =
0 ∩ X 0 6= ∅, X 0 = global(X , R(S +
{hH(t1 ), A(t1 ), Xi} where X = Xha
ha
h
ah
ha
κ
0 = global(X , R(S + t )). Then: N 0 −
t1 )) and Xah
→
P
(t
)
k
G(t
)
=
N000
a
1
1
1
ah
0

where P (t1 ) = (Sh + t1 )[HA(0)]hatp, Xi(Sa + t1 )[AH(0)] |[vha ]| and vha =
X

H(t1 ) ←→i A(t1 ). Finally:
t

1
(N0 , 0) ⇒
(N1 , t1 )

where N1 = steer t1 N000 = steer t1 P (t1 ) k steer t1 G(t1 ) =
P (t1 )|[v1 ]| k G(t1 )|[v2 ]|. Note that:
29

P (t1 )|[v1 ]| =
=


(Sh + t1 )[HA(0)]hatp, Xi(Sa + t1 )[AH(0)] |[v1 ]|
Sh1 [HA(0)]hatp, XiSa1 [AH(0)]

where Sh1 = ((Sh +t1 )|[v1 ]|) and Sa1 = ((Sa +t1 )|[v1 ]|). Moreover, G(t1 )|[v2 ]| =
((Sg + t1 )|[v2 ]|[GLC] = Sg1 [GLC].
Let t2 = Ftoc(N1 ) and assume t2 = th ≤ min{ta , ∆}13 . Below we write
G0 (t2 ) and P 0 (t2 ) to denote, respectively, the 3D processes
(Sg1 +t2 )[GLC] and

1
1
(Sh +t2 )[HA(th )]hatp, X +t2 ·v1 i(Sa +t2 )[AH(t2 )] . Again by the operational
t

2
rules, N1 ⇒
P 0 (t2 ) k G0 (t2 ) = N10 .
0 ∩ X0
Let colliding(N10 ) = {hP 0 (t2 ), G0 (t2 ), Y i} where Y = Xhg
gh 6= ∅,
1
0
1
0
Xhg = global(Xhg , R(Sh + t2 )) and Xgh = global(Xgh , R(Sg + t2 )) ⊆

Y

B(P 0 (t2 )). If vgh = P 0 (t2 ) ←→i G0 (t2 ), then

κ
1
N10 −
→ P (t2 ) hglc, Y i G(t2 ) |[vgh ]| = N100 where G(t2 ) = (S
 g + t2 )[GH(0)] and
1
1
P (t2 ) = (Sh + t2 )[C]hatp, X + t2 · v1 i(Sa + t2 )[AH(t2 )] . Finally:
t

2
(N1 , t1 ) ⇒
(N2 , t1 + t2 )


where N2 = steer (t1 + t2 ) N100 = P (t2 ) hglc,
Y
i
G(t
)
|[v3 ]|. Observe
that:
2


P (t2 ) hglc, Y i G(t2 ) |[v3 ]| = P (t2 )|[v
]|
hglc,
Y
i
G(t
)|[v
]|
=
3
2
3

(Sh2 [C] hatp, X + t2 · v1 i Sa2 [AH(t2 )] hglc, Y i Sg2 [GH(0)]
where Sh2 = (Sh1 + t2 )|[v3 ]|, Sa2 = (Sa1 + t2 )|[v3 ]| and Sg2 = (Sg1 + t2 )|[v3 ]|.
At this stage the network contains just one process and, as a consequence,
no collisions are possible. Thus, Ftoc(N2 ) = ∞. Assume tg = ta − t2 ≤ ∆14 .
If we let Xg = (X + t2 · v1 ) + tg · v3 and Yg = Y + tg · v3 , then:

tg
ρ
→
N2 ⇒ ((Sh2 + tg )[C] hatp, Xg i (Sa2 + tg )[AH(ta )] hglc, Yg i(Sg2 + tg )[GH(tg )] −

∆−tg
((Sh2 + tg )[HEX] k (Sa2 + tg )[ADP]  k (Sg2 + tg )[G6P] ⇒
((Sh2 + ∆)[HEX] k (Sa2 + ∆)[ADP] k (Sg2 + ∆)[G6P] = N20 . Thus:
∆

(N2 , t1 + t2 ) ⇒ (N3 , t1 + t2 + ∆)
13

If were t2 < th . the 3D processes HA(t2 ) and GLC would be no more compatible, and
a collision between them would be treated as elastic. On the other hand, if were t2 = ta
the idling time for AH(ta ) would be over. As a consequence, time would pass further only
after the execution of a weak-split operation that splits the bond between the Hexokinases
and the Atp molecules
14
If were tg 6= ta −t2 the reaction could never proceed since the involved molecules would
never be able to release – all together – the bonds. Thus the system would deadlock.

30


where N3 = steer (t1 + t2 + ∆) N20 = (Sh3 [HEX] k Sa3 [ADP] k Sg3 [G6P],
Si3 = (Si2 +∆)|[vi ]| and vi = steer (t1 +t2 +∆) (Si2 +∆) for each i ∈ {h, a, g}.
We can prove the following basic property of the Shape Calculus stating that any system evolution does not introduce space inconsistencies like
interpenetration of 3D processes or not well-formed processes.
Theorem 1 (Closure w.r.t. well-formedness) Let N be a well-formed
t0

network of 3D processes. If (N, t) ⇒ (M, t + t0 ) then M is well-formed.
t0

t0

κ

Proof: Assume that (N, t) ⇒ (M, t + t0 ) because of N ⇒ N 0 −
→ N 00 and
0
00
M = steer (t + t ) N (the other case – see Def. 24 – is similar). Then, by
t0

κ

Proposition 7 (item 3) and Lemma 1, N well-formed and N ⇒ N 0 −
→ N 00
implies N 00 and hence M = steer (t + t0 ) N 00 well-formed.

6

Conclusions and Future Work

We have defined the full timed operational semantics of the Shape Calculus
and we have introduced a notion of well-formedness of the different objects
of the calculus. We proved that the evolution of a well-formed network of
3D processes is always well-formed, that is to say, no spatial or temporal inconsistencies can be introduced by the dynamics of the calculus. As future
work we intend to provide verification techniques for the Shape Calculus.
In order to do this we believe that a sort of “tailoring” should be made on
the calculus, making some parts (e.g. movement) more abstract and other
parts (e.g. behaviours) more specific adding quantitative information (for
instance probabilities or costs). The whole process will then be supported
by the definition of proper logical languages to specify properties of interests. Of course we expect that some approximations will be necessary to
reach computability and/or feasibility. Another direction of future work
is the possibility to include in the calculus some new useful, but in some
cases complex, concepts such as re-shaping, message passing of values, and
communication by perception of a compatible process in the neighbourhood.

References
[1] http://www.rcsb.org, RCSB - Protein Data Bank.
31

[2] R. Barbuti, A. Maggiolo-Schettini, P. Milazzo, and G. Pardini. Spatial
Calculus of Looping Sequences. Electr. Notes Theor. Comput. Sci.,
229(1):21–39, 2009. FBTC 2008.
[3] R. Barbuti, A. Maggiolo-Schettini, P. Milazzo, G. Pardini, and L. Tesei.
Spatial P Systems. Natural Computing, 2010. Received: 26 October
2009 Accepted: 24 February 2010 Published online: 24 March 2010.
[4] E. Bartocci, D. R. Cacciagrano, M. R. Di Berardini, E. Merelli, and
L. Tesei. Timed Operational Semantics and Well-formedness of Shape
Calculus. Scientific Annals of Computer Science, 20, 2010.
[5] E. Bartocci, F. Corradini, M. R. Di Berardini, E. Merelli, and L. Tesei.
Shape Calculus. A spatial mobile calculus for 3D shapes. Scientific
Annals of Computer Science, 20, 2010.
[6] E. Bartocci, M. R. Di Berardini, F. Corradini, M. Emanuela, and L. Tesei. A Shape Calculus for Biological Processes. In ICTCS 2009, pages
30–33, 2009.
[7] L. Bortolussi and A. Policriti. Stochastic concurrent constraint programming and differential equations. Electr. Notes Theor. Comput.
Sci., 190(3):27–42, 2007.
[8] F. Buti, D. Cacciagrano, F. Corradini, E. Merelli, M. Pani, and L. Tesei.
Bone remodelling in BioShape. In CS2BIO 2010: Proc. of Interactions
between Computer Science and Biology, 1st International Workshop,
2010. Avail. at http://cosy.cs.unicam.it/bioshape/cs2bio2010.
pdf.
[9] F. Buti, D. Cacciagrano, F. Corradini, E. Merelli, and L. Tesei.
BioShape: a spatial shape-based scale-independent simulation environment for biological systems. In ICCS 2010: Proc. of Simulation of Multiphysics Multiscale Systems, 7th International Workshop, 2010. Avail.
at http://cosy.cs.unicam.it/bioshape/iccs2010.pdf.
[10] D. Cacciagrano, F. Corradini, and M. Merelli. Bone remodelling: a
Complex Automata-based model running in BioShape. In ACRI 2010:
Proc. of Cellular Automata for Research and Industry, 9th International
Conference, 2010. Avail. at http://cosy.cs.unicam.it/bioshape/
acri2010.pdf.

32

[11] L. Cardelli. Brane calculi. In Proc. of CMSB ’04, volume 3082 of LNCS,
pages 257–278, 2004.
[12] F. Ciocchetta and J. Hillston. Bio-pepa: An extension of the process
algebra pepa for biochemical networks. Electr. Notes Theor. Comput.
Sci., 194(3):103–117, 2008.
[13] C. Ericson. Real-time collision detection. Elsevier North-Holland, Inc.,
2005.
[14] A. Finkelstein, J. Hetherington, L. Li, O. Margoninski, P. Saffrey,
R. Seymour, and A. Warner. Computational challenges of systems biology. IEEE Computer, 37(5):26–33, 2004.
[15] C. Hecker. Physics, part 3: Collision response. Game Developer Magazine, pages 11–18, 1997.
[16] M. John, R. Ewald, and A. Uhrmacher. A spatial extension to the π
calculus. Electronic Notes in Theoretical Computer Science, 194(3):133–
148, 2008. FBTC 2007.
[17] R. Milner. Communication and concurrency. Prentice-Hall, Inc. Upper
Saddle River, NJ, USA, 1989.
[18] C. Priami and P. Quaglia. Beta binders for biological interactions. In
CMSB, pages 20–33, 2004.
[19] A. Regev, E. Panina, W. Silverman, L. Cardelli, and E. Shapiro. Bioambients: an abstraction for biological compartments. Theoretical Computer Science, 325(1):141–167, 2004.
[20] BioShape. http://cosy.cs.unicam.it/bioshape/.
[21] W. Yi. Real-time behaviour of asynchronous agents. In CONCUR,
pages 502–520, 1990.

33

Appendix A: Proofs of Section 3
The following lemmas are first needed.
Lemma 2 Let S ∈ S well-formed and t ∈ T. Then:
1. v(S + t) = v(S) and m(S + t) = m(S);
2. R(S + t) = R(S) + t · v(S);
3. P(S + t) = P(S) + t · v(S) (and, hence, B(S + t) = B(S) + t · v(S)).
Proof: We prove Items 1, 2 and 3 by induction on S ∈ S well-formed.
Basic: S = hV, m, p, vi, S + t = hV + (t · v), m, p + (t · v), vi and:
1. v(S + t) = v = v(S) and m(S + t) = m = m(S);
2. R(S + t) = p + (t · v) = R(S) + (t · v);
3. P(S + t) = V + (t · v(S)) = P(S) + (t · v(S)).
Comp: S = S1 hXi S2 and S + t = (S1 + t) hY i (S2 + t) where Y = X + t · v
and v = v(S) = v(Si ). By induction hypothesis:
1. v(Si + t) = v(Si ) = v and m(Si + t) = m(Si ) for i = 1, 2. Thus:
v(S +t) = v and m(S +t) = m(S1 +t)+m(S2 +t) = m(Si )+m(S2 ) = m(S).

2
2
2
P
P
P
m(Si )· R(Si )+t·v

m(Si +t)·R(Si +t)

2. R(S + t) =

i=1
2
P

=

i=1
2
P

m(Si +t)

i=1

m(Si )·R(Si )

=
m(Si )

i=1

i=1
2
P

+
m(Si )

i=1

t · v = R(S) + t · v
3. P(S + t) = P(S1 + t) ∪ P(S2 + t) = P(S1 ) ∪ P(S2 ) = P(S).
To prove Prop. 1 we also need the following lemma; its proof has been
omitted because it is similar to that of Lemma 2.
Lemma 3 Let S ∈ S well-formed and w ∈ V. Then:
1. v(S|[w]|) = {w} and m(S|[w]|) = m(S);
2. P(S|[w]|) = P(S) (and, hence, B(S|[w]|) = B(S)).
Proposition 1 Let S ∈ S, t ∈ T and w ∈ V. If S is well-formed then S + t
and S|[w]| are well-formed.
Proof: We prove these statement by induction in S ∈ S.
Basic: S = hV, m, p, vi. Both S + t = hV + t · v, m, p + t · v, vi and
S|[w]| = hV, m, p, wi are well-formed shapes.
Comp: S = S1 hXi S2 . Let v = v(S) = v(Si ) for i = 1, 2. By Defs 5
and 6, it is S + t = (S1 + t) hY i (S2 + t) where Y = X + t · v, and S|[w]| =
(S1 |[w]|) hXi (S2 |[w]|). We first prove S + t wellformedness.
34

1. By induction hypothesis, S1 + t and S2 + t are well-formed;
2. S well-formed implies that X is non-empty set that is equal to P(S1 ) ∩
P(S2 ) = B(S1 ) ∩ B(S2 ). By Lemma 2, we also have that Y = X + t · v is
non-empty and Y = P(S1 + t) ∩ P(S2 + t) = B(S1 + t) ∩ B(S2 + t).
3. By Lemma 2-1, v(S + t) = v where v = v(Si + t) = v(Si ) for i = 1, 2.
Similarly we can prove that S|[w]| is well-formed. Shapes S1 |[w]| and S2 |[w]|
are well-formed (this follows by induction hypothesis); by Lemma 3-1 it is
v(S|[w]|) = w; finally ∅ =
6 X = P(S1 ) ∩ P(S2 ) = B(S1 ) ∩ B(S2 ), P(Si ) =
P(Si |[w]|) and B(Si ) = B(Si |[w]|) for i = 1, 2 (by Lemma 3-2) imply ∅ =
6
X = P(S1 |[w]|) ∩ P(S2 |[w]|) = B(S1 |[w]|) ∩ B(S2 |[w]|).

Appendix B: Proofs of Section 4
This section is devoted to prove main results stated in Section 4.
t

µ

Proposition 3 Let P ∈ 3DP well-formed. Either P
Q or P −
→ Q implies
Q ∈ 3DP well-formed.
Proof: We first prove (by induction on P ∈ 3DP) that:
1. P

t

Q implies shape(Q) = shape(P ) + t;

µ

2. P −
→ Q implies shape(Q) = shape(P ).
Basic: P = S[B].
t
t
1. By operational rules, P
Q implies B →
− B 0 and Q = (S + t)[B 0 ]. Thus:
shape(Q) = S + t = shape(P ) + t.
µ
2. P −
→ Q implies Q = S[B 0 ] for a proper B 0 ∈ B (see rule Basicc in
Table 3). Hence shape(Q) = S = shape(P ).
Comp: P = P1 ha, Xi P2 .
t
t
t
1. P
Q implies P1
Q1 , P2
Q2 , and Q = Q1 ha, Y i Q2 where Y = X +
(t · v(P )). By induction hypothesis, shape(Q) = shape(Q1 ) hY i shape(Q2 ) =
(shape(P1 ) + t) hY i (shape(P2 ) + t) = shape(P ) + t.
µ
µ
µ
2. P −
→ Q implies either P1 −
→ Q1 and Q = Q1 ha, Xi P2 or P2 −
→
Q2 and Q = P1 ha, Xi Q2 . Let us consider the former case (the latter
one can be proved similarly). By induction hypothesis it is shape(Q) =
shape(Q1 ) hXi shape(P2 ) = shape(P1 ) hXi shape(P2 ) = shape(P ).
t

Now we prove that P well-formed and P
Q imply Q well-formed. Again,
we proceed by induction on P well-formed.
35

t

t

Basic:P = S[B]. If P
Q then Q = (S + t)[B 0 ] where B
B 0 . In
this case, S well-formed and Prop. 1 imply shape(Q) = S + t well-formed.
Moreover global(X, R(P )) ⊆ B(P ) for each site X ⊆ P that occurs in B and,
hence, in B 0 . By Lemma 2-4, global(X, R(Q)) = global(X, R(P )+t·v(P )) =
global(X, R(P ))+t·v(P ) ⊆ B(P )+t·v(P ) = B(Q). Thus, Q is well-formed.
Comp: P = P1 ha, Xi P2 with Pi well-formed for i = 1, 2 and X ⊆ B(P1 ) ∩
t
t
Qi , for i = 1, 2, and Q = Q1 ha, Y i Q2 with
B(P2 ). P
Q implies Pi
Y = X + (t · v(P )). By induction hypothesis, Q1 and Q2 are well-formed.
Moreover, X ⊆ B(P1 ) ∩ B(P2 ) implies Y = X + t · v(P ) ⊆ (B(P1 ) ∩ B(P2 )) +
t · v(P ) = (B(P1 ) + t · v(P )) ∩ (B(P2 ) + t · v(P )) = B(Q1 ) ∩ B(Q2 ).
µ

It remains to prove, by induction on P , that P well-formed and P −
→ Q
imply Q well-formed.
µ

µ

Basic: P = S[B]. If P −
→ Q then B −
→ B 0 for a proper B 0 ∈ 3DP and
Q = S[B 0 ]. P well-formed implies S well-formed. Moreover, for each X that
occurs in B 0 (and hence in B), global(X, R(P )) ⊆ B(P ) = B(S) = B(Q).
So, Q is well-formed.
Comp: P = P1 ha, Xi P2 with Pi well-formed for i = 1, 2 and X ⊆ B(P1 ) ∩
µ
µ
µ
B(P2 ). P −
→ Q implies either P1 −
→ Q1 and Q = Q1 ha, Xi P2 or P2 −
→ Q2
and Q = P1 ha, Xi Q2 . We only prove the former case (the latter one is
similar). By induction hypothesis Q1 is well-formed; moreover, shape(Q1 ) =
shape(P1 ) and, hence, B(Q1 ) = B(P1 ). Thus, Q1 and P2 are well-formed
with X ⊆ B(P1 ) ∩ B(P2 ) = B(Q1 ) ∩ B(P2 ), i.e. Q is well-formed.
Proposition 4 Let P ∈ 3DP well-formed. If ha, Xi ∈ bonds(P ) there is a
well-formed 3D process Q ha, Xi R ≡P P .
Proof: By induction on P well-formed.
Basic: P = S[B]. This case is not possible since bonds(P ) = ∅.
Comp: P = P1 hb, Y i P2 with Pi well-formed for i = 1, 2, Y ⊆ B(P1 ) ∩ B(P2 )
and v(P1 ) = v(P2 ) = v(P ) = v. If ha, Xi = hb, Y i it suffices to choose
Q = P1 and R = P2 . Assume ha, Xi ∈ bonds(P1 ) (the case in which ha, Xi ∈
bonds(P2 ) is symmetric). By induction hypothesis, Q1 ha, Xi R1 ≡P P1 is
well-formed and P = P1 hb, Y i P2 ≡P (Q1 ha, Xi R1 ) hb, Y i P2 . We have two
possible subcases:
1. Y ⊆ B(R1 ) and P ≡P Q ha, Xi R where Q = Q1 and R = R1 hb, Y i P2 ,
2. Y ⊆ B(Q1 ) and P ≡P Q ha, Xi R where Q = R1 and R = Q1 hb, Y i P2 .
We only consider the former case (the latter one is similar) and prove that
36

Q ha, Xi R is well-formed. To this aim we have to show that: (i) R =
R1 hb, Y i P2 is well-formed (note that P1 ≡P Q1 ha, Xi R1 well-formed and
Q = Q1 implies Q1 well-formed), (ii) v(Q) = v(R) (this follows easily
because P well-formed implies v(Q1 ) (i.e. v(Q))= v(R1 ) = v(P2 ) = v(R))
and (iii) X ⊆ B(Q) ∩ B(R). Below we prove first (i) and then (iii)
P1 ≡P Q1 ha, Xi R1 and P = P1 hb, Y i P2 well-formed imply, resp., R1 and
P2 well-formed; moreover, v(R1 ) = v(P1 ) = v = v(P2 ) (because P1 ≡P
Q1 ha, Xi R1 is well-formed). To show that R = R1 hb, Y i P2 is well-formed,
it remains to prove that Y ⊆ B(R1 ) ∩ B(P2 ). We proceed by contradiction.
Assume y ∈ Y such that y ∈
/ B(R1 ) ∩ B(P2 ). Then, Y ⊆ B(R1 ) implies
y∈
/ B(P2 ) and, hence, y ∈
/ B(P1 ) ∩ B(P2 ). But, this is impossible because
Y ⊆ B(P1 ) ∩ B(P2 ).
We prove that X ⊆ B(Q) ∩ B(R) = B(Q1 ) ∩ B(R) by contradiction. Recall
that Q1 ha, Xi R1 well-formed implies X ⊆ B(Q1 ) ∩ B(R1 ). Assume that
there is x ∈ X ⊆ B(Q1 ) ∩ B(R1 ) such that x ∈
/ B(Q1 ) ∩ B(R). Then
x∈
/ B(R) = (B(R1 ) ∪ B(P2 ))\{z | z is interior of P(R1 ) ∪ P(P2 )}. Moreover,
x ∈ X ⊆ B(R1 ) ⊆ B(R1 ) ∩ B(P2 ) and x ∈
/ B(R) implies that x is an
interior point of P(R1 ) ∪ P(P2 ), i.e. x is an interior point of P(P2 ); this
is because x ∈ B(R1 ) implies that x cannot be an interior point of P(R1 ).
Finally, x ∈ X implies that x is also an interior point of P1 ≡P Q1 ha, Xi R1 .
Thus, P1 and P2 interpenetrate each other. But this is not possible since
P ≡P P1 hb, Y i P2 is well-formed.
Proposition 5Let P, Q ∈ 3DP and µ ∈ ω(C) ∪ ρ(C). Then:
µ

1. P ⇒ Q implies shape(Q) = shape(P );
µ

2. P well-formed and P ⇒ Q implies Q well-formed.
Proof: We only prove the statement for µ = ρ(a, X); if µ = ω(a, X) the
statement can be proved similarly.
ρ(a,X)

Basic: P = S[B]. This case is not possible since P 6 ⇒ .
Comp: P = P1 hb, Y i P2 with Pi well-formed for i = 1, 2 and X ⊆ B(P1 ) ∩
B(P2 ). We distinguish two possible subcases:
ρ(α,X1 )

ρ(α,X2 )

(i) hb, Y i = ha, Xi, P1 −−−−−→ Q1 , P2 −−−−−→ Q2 with α ∈ {a, a} and
X = X1 ∩ X2 , and Q = Q1 ha, Xi Q2 .
1. By Prop. 3-2, shape(Qi ) = shape(Pi ) for i = 1, 2 and, hence, shape(Q) =
shape(Q1 ) hXi shape(Q2 ) = shape(P1 ) hXi shape(P2 ) = shape(P ).
37

2. By induction hypothesis, Pi well-formed implies Qi well-formed, for i =
1, 2. Moreover X ⊆ B(P1 ) ∩ B(P2 ) and, again, shape(Qi ) = shape(Pi ) for
i = 1, 2 imply X ⊆ B(Q1 ) ∩ B(Q2 ). So the 3D process Q is well-formed.
(ii) Either P1
P1 ha, Xi Q2 .

ρ(a,X)

⇒

Q1 and Q = Q1 ha, Xi P2 or P2

ρ(a,X)

⇒

Q2 and Q =

1. By induction hypothesis it is shape(Qi ) = shape(Pi ) for i = 1, 2. As in
the previous case, we can prove that shape(Q) = shape(P ).
2. By induction hypothesis we have that Qi and Pj , for {i, j} ∈ {1, 2},
are well-formed. Moreover, by Item 1, shape(Qi ) = shape(Pi ), and hence
X ⊆ B(P1 ) ∩ B(P2 ) = B(Qi ) ∩ B(Pj ). Also in this case we can conclude that
Q is well-formed.

Appendix C: Proofs of Section 5
Proposition 6 Let P ∈ 3DP well-formed and C ⊆ C. Then split(P, C) is a
well-formed network of 3D processes .
Proof: By induction on the number of channels in bonds(P ) ∩ C.
bonds(P ) ∩ C = ∅. In such a case split(P, C) = P is well-formed.
ha, Xi ∈ bonds(P ) ∩ C 6= ∅. By Prop. 4, there are P1 , P2 well-formed
such that P ≡P P1 ha, Xi P2 and split(P, C) = split(P1 , C) k split(P2 , C) =
N1 k N2 . By induction hypothesis Ni is a well-formed 3D network for i = 1, 2.
Now, in order to prove that split(P, C) is well-formed, it still remains to
prove that if Q1 and Q2 are two 3D processes in the network N1 and N2 ,
respectively, then Q1 and Q2 do not interpenetrate. Assume, towards a
contradiction, that there are Q1 and Q2 in N1 and N2 , respectively, such
that Q1 and Q2 interpenetrate, i.e. such that there is (at least) a point x
that is interior of both Q1 and Q2 .
For each i = 1, 2, it holds that either bonds(Pi ) ∩ C = ∅, Ni = Pi
and Qi = Pi or bonds(Pi ) ∩ C = { ha1 , X1 i , ha2 , X2 i , .., hani , Xni i }, Pi ≡P
Pi1 ha1 , X1 i (Pi2 ha2 , X2 i ..(Pini hani , Xni i Pini+1 )) (this follows by iterating
Prop. 4), Ni = Pi1 k (Pi2 k · · · (Pini k Pini+1 )) and Qi = Pij for some j =
1, 2, · · · , ni, ni + 1. Thus, in both cases the set of interior points of Qi is a
subset of interior point of Pi . As a consequence, if Q1 and Q2 interpenetrate
so do P1 and P2 . But this is not possible because P is well-formed. To
prove Prop. 7 we need the following preliminary result.
38

t

Lemma 4 Let N, M ∈ N, P, Q ∈ 3DP and t ∈ T such that N →
− M and
t
P →
− Q. The network N contains P iff M contains Q.
Proof: By induction on N ∈ N.
t

N = Nil. N →
− Nil and Nil does not contain any 3D process.
t

N = P with P ∈ 3DP. By our operational semantics, N →
− M iff M = Q
t
and P →
− Q.
t

t

− Mi for i = 1, 2. P is contained
N = N1 k N2 . N →
− M1 k M2 = M iff Ni →
in N iff P is contained either in N1 or in N2 iff (by induction hypothesis)
and Q is contained either in M1 or in M2 , i.e. iff Q is contained in M .
Proposition 7 Let t ∈ T, P ∈ 3DP, N ∈ N, with P and N well-formed.
ω

ρ

1. P −
→ N and P −
→ N implies N ∈ N well-formed.
t

2. N →
− M implies M well-formed;
t

3. N ⇒ M implies M well-formed.
Proof: Item 1 can be proved by (iterative applications of) Prop. 5-2 and
Prop. 6. Item 3 follows directly from Items 1 and 2 (see Definition 21). In
what follows, we prove Item 2 by induction on N ∈ N.
t

N = Nil. In such a case N →
− M implies M = Nil that is well-formed.
N = P with P ∈ 3DP. The statement is a trivial consequence of Prop. 3-3.
t

t

N = N1 k N2 . If N →
− M then Ni →
− Mi , for i = 1, 2, and M = M1 k M2 . By
induction hypothesis, M1 and M2 are well-formed. So, it remains to prove
that if Q1 and Q2 are 3D processes that compose the networks M1 and M2 ,
resp., then Q1 and Q2 do not interpenetrate. We proceed by contradiction.
Assume that there are Q1 in M1 and Q2 in M2 that interpenetrate each
other. By Lemma 4, Mi contains Qi iff Ni contains Pi for some Pi ∈ 3DP
t
such that Pi →
− Qi . Moreover, by Prop. 3-1, shape(Qi ) = shape(Pi ) + t.
Thus, if Q1 and Q2 interpenetrate the same do P1 and P2 . But this not
possible since N is well-formed.
hP,Q,Xi

Lemma 5 Let N, M ∈ N such that N is well-formed and N −−−−−→ M for
some hP, Q, Xi ∈ colliding(N ). If P 0 and Q0 are two processes composing M
with shape(P 0 ) = shape(P ) and shape(Q0 ) = shape(Q), then hP 0 , Q0 , Y i ∈
/
colliding(M ) for any Y ⊆ P.

39

hP,Q,Xi

hP,Q,Xi

Proof: By rules in Table 6, N −−−−−→e M implies N −−−−−→e M implies
X
M ≡ (P |[vp ]| k Q|[vq ]|) k N 0 where the pair of velocity (vp , vq ) = P ←→e Q.
Moreover, Equations (1) and (2) in Def. 9 ensure that P |[vp ]| and Q|[vq ]| (since
N is well-formed, these are the only processes in M with the same shape of
hP,Q,Xi

P and Q, resp.) can not collide anymore. Now assume N −−−−−→i M . By
hα,Xp i

Def. 23, there are compatible hα, Xp i, hα, Xq i ∈ C such that P −−−−→ P 0 ,
hα,Xq i

Q −−−−→ Q0 and M ≡ ((P 0 ha, Xi Q0 )|[v]|) k N 0 with α ∈ {a, a}, X = Xp ∩
X

Xq 6= ∅ and v = P ←→i Q. The statement follows because there are no P 0
and Q0 in M such that shape(P 0 ) = shape(P ) and shape(Q0 ) = shape(Q).
Proposition 8 Let N ∈ N, P, Q ∈ 3DP and X a not-emptyset subset of P.
hP,Q,Xi

Then N well-formed and N −−−−−→ M implies M well-formed.
hP,Q,Xi

Proof: If N −−−−−→e M then N ≡ (P k Q) k N 0 , M ≡ (P |[vp ]| k Q|[vq ]|) k N 0
X

and (vp , vq ) = P ←→e Q. Moreover, N well-formed implies that P , Q and
N 0 are well-formed and processes P and Q do not interpenetrate each other
and with any other 3D process composing N 0 (see Def. 18). Finally: P |[vp ]|
and Q|[vq ]| are well-formed 3D processes with shape(P |[vp ]|) = shape(P ) and
shape(Q|[vq ]|) = shape(Q) (see Lemma 3). Thus, P |[vp ]| and Q|[vq ]| do not
interpenetrate each other and with any other 3D process in N 0 and we can
conclude that M is well-formed.
hP,Q,Xi

Now assume N −−−−−→i M . Again, N ≡ (P k Q) k N 0 and, by rule inel,
hα,Xp i

there are hα, Xp i, hα, Xq i ∈ C compatible such that α ∈ {a, a}, P −−−−→ P 0 ,
hα,Xq i

Q −−−−→ Q0 and M ≡ ((P 0 ha, Xi Q0 )|[v]|) k N 0 where X = Xp ∩ Xq 6= ∅
X

and v = P ←→i Q. By Prop. 3-3, P and Q well-formed implies P 0 and Q0
well-formed. Moreover:
hα,Xp i

hα,Xq i

(1) P −−−−→ P 0 and Q −−−−→ Q0 imply Xp ⊆ B(P ) and Xq ⊆ B(Q), resp.
Thus, X = Xp ∩ Xq ⊆ B(P ) ∩ B(Q) = B(P 0 ) ∩ B(Q0 ) (since Prop. 3-2
implies shape(P 0 ) = shape(P ) and shape(Q0 ) = shape(Q)), P 0 ha, Xi Q0 and
(P 0 ha, Xi Q0 )|[v]| are well-formed 3D processes.
(2) shape((P 0 ha, Xi Q0 )|[v]|) = shape(P 0 ha, Xi Q0 ) = P(P 0 ) ∪ P(Q0 ) =
P(P ) ∪ P(Q). As a consequence, (P 0 ha, Xi Q0 )|[v]| can not interpenetrate
any 3D process that compose the network N 0 (otherwise either P or Q must
do the same).
Aso in this case we can conclude that M is well-formed.
40

