A synchronous π-calculus
arXiv:cs/0606019v2 [cs.LO] 9 Feb 2007

Roberto M. Amadio∗
Université Paris 7†
April 13, 2018

Abstract
The SL synchronous programming model is a relaxation of the Esterel synchronous model where the reaction to the absence of a signal within an instant can
only happen at the next instant. In previous work, we have revisited the SL synchronous programming model. In particular, we have discussed an alternative design
of the model, introduced a CPS translation to a tail recursive form, and proposed a
notion of bisimulation equivalence. In the present work, we extend the tail recursive
model with first-order data types obtaining a non-deterministic synchronous model
whose complexity is comparable to the one of the π-calculus. We show that our
approach to bisimulation equivalence can cope with this extension and in particular
that labelled bisimulation can be characterised as a contextual bisimulation.

∗
†

Partially supported by ANR-06-SETI-010-02.
Laboratoire Preuves, Programmes et Systèmes, UMR-CNRS 7126.

1

1

Introduction

Concurrent and/or distributed systems are usually classified according to two main parameters (see, e.g., [19]): the relative speed of the processes (or threads, or components,
or nodes) and their interaction mechanism. With respect to the first parameter one refers
to synchronous, asynchronous, partially synchronous,. . . systems. In particular, in synchronous systems, there is a notion of instant (or phase, or pulse, or round) and at each
instant each process performs some actions and synchronizes with all other processes. One
may say that all processes proceed at the same speed and it is in this specific sense that
we will refer to synchrony in this work.
With respect to the second parameter, one considers shared memory, message passing, signals, broadcast,. . . Concerning the message passing interaction mechanism, one
distinguishes various situations according to whether the communication channel includes
a bounded or unbounded and an ordered or unordered buffer. In particular the situation
where the buffer has 0 capacity corresponds to a rendez-vous communication mechanism
which is also called synchronous communication in that it forces a synchronisation.
The notion of synchrony (in the sense adopted in this work) is a valuable logical concept
that simplifies the design and analysis of systems. One may verify this claim by consulting
standard textbooks in concurrent/distributed algorithms such as [20, 34] and comparing the
algorithms for basic problems such as leader election, minimum spanning tree, consensus,. . .
in the synchronous and asynchronous case. In [20, 34], the formalisation of the so called
synchronous network model is quite simple. One assumes a fixed network topology and
describes the behaviour of each process essentially as an infinite state Moore machine [18]:
at each instant, each process, depending on its current state, emits a message on each
outgoing edge, then it receives a messages from each incoming edge, and computes its
state for the next instant.
In this paper, we are looking at the synchronous model from the point of view of
process calculi. This means in particular, that we are looking for a notion of equivalence
of synchronous systems with good compositionality properties. The works on SCCS [24]
and Meije [5] are an early attempt at providing a process calculus representation of the
synchronous model. SCCS and Meije are built over the same action structure: essentially,
the free abelian group generated by a set of particulate actions. The models differ in the
choice of the combinators: SCCS starts with a synchronous parallel composition and then
adds operators to desynchronise processes while Meije starts with an asynchronous parallel
composition and then adds operators that allow to synchronise processes. As a matter of
fact, the SCCS and Meije operators are inter-definable so that the calculi can be regarded
as two presentations of the same model.
SCCS/Meije is a simple model with nice mathematical properties but it has failed so
far to turn into a model for a realistic synchronous programming language. For this reason,
we will not take the SCCS/Meije model as a starting point, but the synchronous language
SL introduced in [12]. Threads in the SL model interact through signals as opposed to
channels. A cooperative scheduling (as opposed to pre-emptive, see [28]) is sometimes
considered, though this is not quite a compulsory choice and it is not followed here. This
2

style of synchronous and possibly cooperative programming has been advocated as a more
effective approach to the development of applications such as event-driven controllers, data
flow architectures, graphical user interfaces, simulations, web services, multi-player games
(we refer to [2] for a discussion of the applications and implementation techniques).
The SL model can be regarded as a relaxation of the Esterel model [8] where the
reaction to the absence of a signal within an instant can only happen at the next instant.
This design choice avoids some paradoxical situations and simplifies the implementation
of the model. Unlike the SCCS/Meije model, the SL model has gradually evolved into a
general purpose programming language for concurrent applications and has been embedded
in various programming environments such as C, Java, Scheme, and Caml (see [11, 30,
33, 21]). For instance, the Reactive ML language [21] includes a large fragment of the
Caml language plus primitives to generate signals and synchronise on them. We should
also mention that related ideas have been developed by Saraswat et al. [32] in the area of
constraint programming.
The Meije and the Esterel/SL models were developed in Sophia-Antipolis in the same
research team, but, as of today, there seems to be no strong positive or negative result on
the possibility of representing one of the models into the other. Still there are a number
of features that plead in favour of the Esterel/SL model. First, the shift from channel
based to signal based communication allows to preserve (to some extent) the determinacy
of the computation while allowing for multi-point interaction. Second, pure signals, i.e.,
signals carrying no values, as opposed to pure channels, allow for a representation of data in
binary rather than unary notation. Third, there is a natural generalisation of the calculus
to include general data types. Fourth, the length of an instant is programmable rather
than being given in extenso as a finite word of so called particulate actions. Fifth, efficient
implementations of the model have been developed.
In the early 80’s, the development of the SCCS/Meije model relied on the same mathematical framework (labelled transition system and bisimulation) that was used for the development of the CCS model. However, the following years have witnessed the development
of two quite distinct research directions concerned with asynchronous and synchronous programming, respectively. Nowadays, the π-calculus [26] and its relatives can be regarded as
typical abstract models of asynchronous concurrent programming while various languages
such as Lustre [14], Esterel [8], and SL [12] carry the flag of synchronous programming.
We remark that while the π-calculus has inherited many of the techniques developed for
CCS, the semantic theory of the SL model remains largely underdeveloped. In recent work
[1], we have revisited the SL synchronous programming model. In particular, we have discussed an alternative design of the model, introduced a CPS translation to a tail recursive
form, and proposed a novel notion of bisimulation equivalence with good compositionality properties. The original SL language as well as the revised one assume that signals
are pure in the sense that they carry no value. Then computations are naturally deterministic and bisimulation equivalence collapses with trace equivalence. However, practical
programming languages that have been developed on top of the model include data types
beyond pure signals and this extension makes the computation non-deterministic unless
significant restrictions are imposed. For instance, in the Reactive ML language we have
3

already quoted, signals carry values and the emission of two distinct values on the same
signal may produce a non-deterministic behaviour.
In the present work, we introduce a minimal extension of the tail recursive model where
signals may carry first-order values including signal names. The linguistic complexity of
the resulting language is comparable to the one of the π-calculus and we tentatively call
it the Sπ-calculus (pronounced s − pi).1 Our contribution is to show that the notion
of bisimulation equivalence introduced in [1] is sufficiently robust to be lifted from the
deterministic language with pure signals to the non-deterministic language with data types
and signal name generation. The main role in this story is played by a new notion of labelled
bisimulation. We show that this notion has good congruence properties and that it can be
characterised via a suitable notion of contextual bisimulation in the sense of [17]. The proof
of the characterisation theorem turns out to be considerably more complex than in the pure
case having to cope with phenomena such as non-determinism and name extrusion.
While this approach to the semantics of concurrency has already been explored in the
framework of asynchronous languages including, e.g., the π-calculus [17, 3, 15], Prasad’s
calculus of broadcasting systems [29, 16], and the ambient calculus [23], this seems to be the
first concrete application of the approach to a synchronous language. We expect that the
resulting semantic theory for the SL model will have a positive fall-out on the development
of various static analyses techniques to guarantee properties such as determinacy [21],
reactivity [4], and non-interference [22].
In the following, we assume familiarity with the technical development of the theory of
bisimulation for the π-calculus and some acquaintance with the synchronous languages of
the Esterel family.

2

The Sπ-calculus

Programs P, Q, . . . in the Sπ-calculus are defined as follows:
P ::= 0 | A(e) | se | s(x).P, K | [s1 = s2 ]P1 , P2 | [u ☎ p]P1 , P2 | νs P | P1 | P2
K ::= A(r)
We use the notation m for a vector m1 , . . . , mn , n ≥ 0. The informal behaviour of programs
follows. 0 is the terminated thread. A(e) is a (tail) recursive call with a vector e of
expressions as argument. The identifier A is defined by a unique equation A(x) = P with
the usual condition that the variables free in P are contained in {x}. se evaluates the
expression e and emits its value on the signal s. A value emitted on a signal persists
within the instant and it is reset at the end of each instant. s(x).P, K is the present
statement which is the fundamental operator of the SL model. If the values v1 , . . . , vn
have been emitted on the signal s in the current instant then s(x).P, K evolves nondeterministically into [vi /x]P for some vi ([ / ] is our notation for substitution). On the
1

S for synchronous as in SCCS [25] and SL [12]. Not to be confused with the so called ‘synchronous’
π-calculus which would be more correctly described as the π-calculus with rendez-vous communication nor
with the SPI-calculus where the S suggests a pervasive ‘spy’ controlling and corrupting all communications.

4

other hand, if no value is emitted then the continuation K is evaluated at the end of the
instant. [s1 = s2 ]P1 , P2 is the usual matching function of the π-calculus that runs P1 if
s1 = s2 and P2 , otherwise. Here both s1 and s2 are free. [u ☎ p]P1 , P2 , matches u against
the pattern p. We assume u is either a variable x or a value v and p has the shape c(p),
where c is a constructor and p a vector of patterns. At run time, u is always a value and
we run σP1 if σ is the result of matching u against p, and P2 otherwise. Note that as usual
the variables occurring in the pattern p are bound. νs P creates a new signal name s and
runs P . (P1 | P2 ) runs in parallel P1 and P2 . The continuation K is simply a recursive call
whose arguments are either expressions or values associated with signals at the end of the
instant in a sense that we explain below.2
The definition of program relies on the following syntactic categories:
Sig
Var
Cnst
Val
Pat
Exp
Rexp

::= s | t | · · ·
::= Sig | x | y | z | · · ·
::= ∗ | nil | cons | c | d | · · ·
::= Sig | Cnst(Val , . . . , Val )
::= Var | Cnst(Pat, . . . , Pat)
::= Pat
::=!Sig | Var | Cnst(Rexp, . . . , Rexp)

(signal names)
(variables)
(constructors)
(values v, v ′ , . . .)
(patterns p, p′ , . . .)
(expressions e, e′ , . . .)
(exp. with dereferenciation r, r ′ , . . .)

As in the π-calculus, signal names stand both for signal constants as generated by the ν
operator and signal variables as in the formal parameter of the present operator. Variables
Var include signal names as well as variables of other types. Constructors Cnst include ∗,
nil, and cons. We will also write [v1 ; . . . ; vn ] for the list of values cons(v1 , . . . , cons(vn , nil) . . .),
n ≥ 0. Values Val are terms built out of constructors and signal names. Patterns Pat
are terms built out of constructors and variables (including signal names). For the sake of
simplicity, expressions Exp here happen to be the same as patterns but we could easily add
first-order functional symbols defined by recursive equations. Finally, Rexp is composed
of either expressions or the dereferenced value of a signal at the end of the instant. Intuitively, the latter corresponds to the set of values emitted on the signal during the instant.
If P, p are a program and a pattern then we denote with fn(P ), fn(p) the set of free signal
names occurring in them, respectively. We also use FV (P ), FV (p) to denote the set of
free variables (including signal names).

2.1

Typing

Types include the basic type 1 inhabited by the constant ∗ and, assuming t is a type, the
type sig(t) of signals carrying values of type t, and the type list(t) of lists of values of type t
with constructors nil and cons. 1 and list(t) are examples of inductive types. More inductive
types (booleans, numbers, trees,. . .) can be added along with more constructors. We
2

The reader may have noticed that we prefer the term program to the term process. By this choice, we
want to stress that the parallel threads that compose a program are tightly coupled and are executed and
observed as a whole.

5

assume that variables (including signals), constructor symbols, and thread identifiers come
with their (first-order) types. For instance, a constructor c may have a type (t1 , t2 ) → t
meaning that it waits two arguments of type t1 and t2 respectively and returns a value of
type t. It is then straightforward to define when a program is well-typed and verify that
this property is preserved by the following reduction semantics. We just notice that if a
signal name s has type sig(t) then its dereferenced value !s should have type list(t). In the
following, we will tacitly assume that we are handling well typed programs, expressions,
substitutions,. . .

2.2

Matching

As already mentioned, the Sπ-calculus includes two distinct matching constructions: one
operating over signal names works as in the π-calculus and the other operating over values
of inductive type actually computes a matching substitution match(v, p) which is defined
as follows:3

σ if dom(σ) = FV (p), σ(p) = v
match(v, p) =
↑ otherwise
To appreciate the difference, assume s 6= s′ and consider P = [s = s′ ]P1 , P2 and P ′ =
[[s] ☎ [s′ ]]P1 , P2 . In the first case, P reduces to P2 while in the second case, P ′ reduces to
[s/s′ ]P1 . Indeed, in the first case s′ is a constant while in the second case it is a bound
variable.

2.3

Informal reduction semantics

Assume v1 6= v2 are two distinct values and consider the following program in Sπ:
P = ν s1 , s2 ( s1 v1

|

s1 v2

|

s1 (x). (s1 (y). (s2 (z). A(x, y) , B(!s1 )) , 0) , 0 )

If we forget about the underlined parts and we regard s1 , s2 as channel names then P could
also be viewed as a π-calculus process. In this case, P would reduce to
P1 = νs1 , s2 (s2 (z).A(σ(x), σ(y))
where σ is a substitution such that σ(x), σ(y) ∈ {v1 , v2 } and σ(x) 6= σ(y). In Sπ, signals
persist within the instant and P reduces to
P2 = νs1 , s2 (s1 v1 | s1 v2 | (s2 (z).A(σ(x), σ(y)), B(!s1 )))
where σ(x), σ(y) ∈ {v1 , v2 }.
One can easily formalise this behaviour by assuming a standard structural equivalence,
by introducing the usual rules for matching and for unfolding recursive definitions (cf. rules
sig
ind
ind
=sig
1 , =2 , =1 , =2 , and rec in the following Table 1), and by adding the rule:
sv | s(x).P, K → sv | [v/x]P
3

Without loss of expressive power, one could assume that in the second matching instruction the pattern
p contains exactly one constructor symbol and that all the variables occurring in it are distinct.

6

What happens next? In the π-calculus, P1 is deadlocked and no further computation
is possible. In the Sπ-calculus, the fact that no further computation is possible in P2
is detected and marks the end of the current instant. Then an additional computation
represented by the relation 7→ moves P2 to the following instant:
P2 7→ P2′ = νs1 , s2 B(ℓ)
where ℓ ∈ {[v1 ; v2 ], [v2 ; v1 ]}. Thus at the end of the instant, a dereferenced signal such as
!s1 becomes a list of (distinct) values emitted on s1 during the instant and then all signals
are reset.
We will further comment on the relationships between the π-calculus and the Sπcalculus in section 2.6 once the formal definitions are in place. In the following section
2.4, Table 1 will formalise the reduction relation (in the special case where the transition
is labelled with the action τ ) while Table 2 will describe the evaluation relation at the end
of the instant.

2.4

Transitions
α

The behaviour of a program is specified by (i) a labelled transition system → describing
the possible interactions of the program during an instant and (ii) a transition system 7→
determining how a program evolves at the end of each instant.
As usual, the behaviour is defined only for programs whose only free variables are
signals. The labelled transition system is similar to the one of the polyadic π-calculus
modulo a different treatment of emission which we explain below. We define actions α as
follows:
α ::= τ | sv | νt sv
where in the emission action the signal names t are distinct, occur in v, and differ from s.
The functions n (names), fn (free names), and bn (bound names) are defined on actions as
usual: fn(τ ) = ∅, fn(sv) = {s} ∪ fn(v), fn(νt sv) = ({s} ∪ fn(v))\{t}; bn(τ ) = bn(sv) = ∅,
bn(νt sv) = {t}; n(α) = fn(α) ∪bn(α). The related labelled transition system is defined in
table 1 where rules apply only to programs whose only free variables are signal names and
with standard conventions on the renaming of bound names. As usual, the symmetric rule
for (par ) and (synch) are omitted. The rules are those of the polyadic π-calculus but for
the following points. (1) In the rule (out), the emission is persistent. (2) In the rule (in),
the continuation carries the memory that the environment has emitted sv. For example,
this guarantees, that in the program s(x).(s(y).P, 0), 0, if the environment provides a value
sv for the first input then that value persists and is available for the second input too. (3)
α
α
ind
′
′
The rules (=ind
1 ) and (=2 ) handle the pattern matching. We write P → · for ∃ P P → P .
τ
τ
α
τ
α
τ
We will also write P ⇒ P ′ for P (→)∗ P ′ and P ⇒ P ′ with α 6= τ for P (⇒) (→)(⇒)P ′ .
A program is suspended, i.e., it reaches the end of an instant, when the labelled transition system cannot produce further (internal) τ transitions.
τ

Definition 1 We write P ↓ if ¬(P → ·) and say that the program P is suspended.
7

(out)

(in)

sv

sv → sv

α

(par)

P1 → P1′ bn(α) ∩ fn(P2 ) = ∅
α
P1 | P2 → P1′ | P2

νt sv

(synch)

(=sig
1 )

(=ind
1 )

(rec)

P → P′ t ∈
/ n(α)
α
νt P → νt P ′

(νex )

P → P′

[s = s]P1 , P2 → P1
match(v, p) = σ
τ
[v ☎ p]P1 , P2 → σP1

t′ 6= s t′ ∈ n(v)\{t}

νt′ P
(=sig
2 )

τ

sv

P1 → P1′ P2 → P2′ {t} ∩ fn(P2 ) = ∅
τ
P1 | P2 → νt (P1′ | P2′ )
νt sv

α

(ν)

sv

s(x).P, K → [v/x]P | sv

(=ind
2 )

(νt′ ,t)sv

→

s1 6= s2
τ
[s1 = s2 ]P1 , P2 → P2
match(v, p) =↑
τ
[v ☎ p]P1 , P2 → P2

A(x) = P
τ
A(v) → [v/x]P
Table 1: Labelled transition system during an instant

8

P′

(0)

∅,V

0 7−→ 0
Ei ,V

(par)

(out)

Pi 7−→ Pi′

v occurs in V (s)

i = 1, 2

E1 ∪E2 ,V

(P1 | P2 ) 7−→ (P1′ | P2′ )

(in)

[{v}/s],V

sv 7−→ 0
E,V ′

(ν)

P 7−→ P ′

s∈
/ dom(V )
∅,V

s(x).P, K 7−→ V (K)

V ′ (s) k−E(s) V [[]/s] = V ′ [[]/s]
E[∅/s],V

νs P 7−→ νs P ′

E,V

P 7−→ P ′ V k−E
P 7→ P ′
Table 2: Transition system at the end of the instant
When the program P is suspended, an additional computation is carried on to move to
the next instant. This computation is described by the transition system 7→. First of all,
we have to compute the set of values emitted on every signal. To this end, we introduce
some notation.
Let E vary over functions from signal names to finite sets of values. Denote with ∅ the
function that associates the empty set with every signal name, with [M/s] the function
that associates the set M with the signal name s and the empty set with all the other
signal names, and with ∪ the union of functions defined pointwise.
We represent a set of values as a list of the values contained in the set. More precisely,
we write v k−M and say that v represents M if M = {v1 , . . . , vn } and v = [vπ(1) ; . . . ; vπ(n) ]
for some permutation π over {1, . . . , n}. Suppose V is a function from signal names to
lists of values. We write V k−E if V (s) k−E(s) for every signal name s. We also write
dom(V ) for {s | V (s) 6= []}. If K is a continuation, i.e., a recursive call A(r), then
V (K) is obtained from K by replacing each occurrence !s of a dereferenced signal with the
associated value V (s). We denote with V [ℓ/s] the function that behaves as V except on s
where V [ℓ/s](s) = ℓ.
To define the transition 7→ at the end of the instant, we rely on an auxiliary judgement
E,V
P 7−→ P ′ . Intuitively, this judgement states that: (1) P is suspended, (2) P emits exactly
the values specified by E, and (3) the behaviour of P in the following instant is P ′ and
depends on V . The transition system presented in table 2 formalizes this intuition. For
instance, one can show that:
E,V

νs1 (s1 (x).0, A(!s2 ) | s2 v3 ) | (s2 v2 | s1 v1 ) 7−→ νs1 (A(V (s2 )) | 0) | (0 | 0)
where E = [{v1 }/s1 , {v2 , v3 }/s2 ] and, e.g., V = [[v1 ]/s1 , [v3 ; v2 ]/s2 ].

2.5

Derived operators

We introduce some derived operators and some abbreviations. The calculi with pure signals
considered in [12, 2, 1] can be recovered by assuming that all signals have type Sig(1). In
9

this case, we will simply write s for s∗ and s.P, K for s(x).P, K where x ∈
/ FV (P ). We
denote with Ω a looping process defined, e.g., by Ω = A() where A() = A(). We abbreviate
s(x).P, 0 with s(x).P . We can derive an internal choice operator by defining,
P1 ⊕ P2 = νs (s(x)[x ☎ 0]P1 , P2 | s0 | s1)
where, e.g., we set 0 = [] and 1 = [∗]. The pause operation suspends the execution till the
end of the instant. It is defined by:
pause.K = νs s.0, K
where: s ∈
/ fn(K). We can also simulate an operator await s(x).P that waits for a value
on a signal s for arbitrarily many instants by defining:
await s(x).P = s(x).P, A(x)
where {x} = {s} ∪ (FV (P )\{x}) and A(x) = s(x).P, A(x).
It is also interesting to program a generalised matching operator [x = νs v]X P that
given a value x, checks whether x has the shape νs v where the freshness of the signal
names s is relative to a finite set X of signal names, i.e., no name in s belongs to X. If this
is the case, we run P and otherwise we do nothing. Assuming, {s} ⊆ fn(v), fn(v)\{s} ⊆ X,
{s} ∩ X = ∅, and X = ∅ whenever {s} = ∅, there are three cases to consider:
1. v = s is a signal name and s is empty. Then [x = s]X P is coded as [x = s]P, 0.
2. v = s is a signal name and s = s. Then [x = νs s]X P is coded as [x ∈
/ X]P where if
X = {s1 , . . . , sn } then [x ∈
/ X]P is coded as [x = s1 ]0, (· · · , [x = sn ]0, P · · · ).
3. v = c(p1 , . . . , pn ). Let {s′ } = fn(v)\{s} be the set of signal names which are free in
νs v. We associate with the vector of signal names s′ a vector of fresh signal names
s′′ . Let v ′′ = [s′′ /s′ ]v. Then [x = νs v]X P is coded as:
[x ☎ v ′′ ][s′′ = s′ ][{s} ∩ X = ∅][s distinct]P
where: (1) [s′′1 , . . . , s′′m = s′1 , . . . , s′m ]Q is an abbreviation for [s′′1 = s′1 ] . . . ([s′′m =
s′m ]Q, 0) . . . , 0, (2) [{s} ∩ X = ∅] is expressed by requiring that every signal name
in {s} does not belong to X, and (3) [s distinct] is expressed by requiring that the
signal names in s are pairwise different. For example, to express
[x = νs1 , s2 c(s1 , c(s′3 , s2 , s1 ), s′3 )]{s′3 ,s′4} P
/ {s′3 , s′4 }][s1 6= s2 ]P .
/ {s′3 , s′4 }][s2 ∈
we write [x ☎ c(s1 , c(s′′3 , s2 , s1 ), s′′3 )][s′′3 = s′3 ][s1 ∈
Note that the introduction of the auxiliary signal names s′′ is required because in the
pattern considered the signal names are interpreted as variables and not as constants.
Also, note that the names s1 , s2 , and s′′3 are bound in P .
10

2.6

Comparison with the π-calculus

In order to make a comparison easier, the syntax of the Sπ-calculus is similar to the one
of the π-calculus. However there are some important semantic differences to keep in mind.
Deadlock vs. End of instant. What happens when all threads are either terminated or
waiting for an event that cannot occur? In the π-calculus, the computation stops. In the
Sπ-calculus (and more generally, in the SL model), this situation is detected and marks
the end of the current instant. Then suspended threads are reinitialised, signals are reset,
and the computation moves to the following instant.
Channels vs. Signals. In the π-calculus, a message is consumed by its recipient. In the
Sπ-calculus, a value emitted along the signal persists within an instant and it is reset at
the end of it. We note that in the semantics the only relevant information is whether a
given value was emitted or not, e.g., we do not distinguish the situation where the same
value is emitted once or twice within an instant.
Data types. The (polyadic) π-calculus has tuples as basic data type, while the Sπ-calculus
has lists. The reason for including lists rather than tuples in the basic calculus is that at
the end of the instant we transform a set of values into a suitable data structure (in our
case a list) that represents the set and that can be processed as a whole in the following
instant. Note in particular, that the list associated with a signal is empty if and only if no
value was emitted on the signal during the instant. This allows to detect the absence of a
signal at the end of the instant.
Determinism vs. Non-determinism. In the Sπ-calculus there are two sources of nondeterminism. (1) Several values emitted on the same signal compete to be received during
the instant, e.g., s0 | s1 | s(x).P may evolve into either s0 | s1 | [0/x]P or s0 | s1 | [1/x]P .
(2) At the end of the instant, values emitted on a signal are collected in an order that
cannot be predicted, e.g., νs′ , s′′ (ss′ | ss′′ | pause.A(!s, s′ , s′′ )) may evolve into either
A([s′ ; s′′ ], s′ , s′′ ) or A([s′′ ; s′ ], s′ , s′′ ). Accordingly, one may consider two restrictions to make
the computation deterministic. (i) If a signal can be read during an instant then at most
one value can be emitted on that signal during an instant.4 (ii) If a signal can only be read
at the end of the instant then the processing of the associated list of values is independent
of its order.5

2.7

Comparison with CBS and the timed π-calculus

In the calculus of broadcasting systems (CBS, [29]), threads interact through a unique
broadcast channel. The execution mechanism guarantees that at each step one process
sends a message while all the other processes either receive the message or ignore it. There
4

For instance, the calculus with pure signals satisfies this condition.
In the languages of the Esterel family, sometimes one makes the hypothesis that the values collected
at the end of the instant are combined by means of an associative and commutative function. While
this works in certain cases, it seems hard to conceive such a function when manipulating objects such as
pointers. It seems that a general notion of deterministic program should be built upon a suitable notion
of program equivalence such as the one we develop here.
5

11

is a similarity between the emission of a value on a signal and the broadcast of a value in
the sense that in both cases the value can be received an arbitrary number of times. On
the other hand, it appears that the CBS model does not offer a direct representation of the
notion of instant.
Berger’s timed π-calculus [7] includes a primitive timert x(y).P, Q which means: wait
for a message on x for at most t time units and if it does not come then do Q. While there
is a syntactic similarity with the present statement of the SL model, we remark that the
notion of time unit is very different from the notion of instant in the SL model. In the SL
model, an instant lasts exactly the time needed for every process to accomplish the tasks
it has scheduled for the current instant. In the timed model, a time unit lasts exactly one
reduction step. As a matter of fact, the notion of ‘reduction step’ is based on a rather
arbitrary definition and it fails to be a robust programming concept.

3

Labelled bisimulation and its characterisation

We introduce a new notion of labelled bisimulation, a related notion of contextual bisimulation and state our main result: the two bisimulations coincide.
Definition 2 We write:
τ

P ⇓ if ∃ P ′ ( P ⇒ P ′ and P ′ ↓ )
α
α
P ⇓L if ∃ α1 , P1 . . . , αn , Pn ( P →1 P1 · · · →n Pn ,

(weak suspension)
n ≥ 0, and Pn ↓ ) (L-suspension)

Obviously, P ↓ implies P ⇓ which in turn implies P ⇓L and we will see that these
implications cannot be reversed. The L-suspension predicate (L for labelled) plays an
important role in the definition of labelled bisimulation which is the central concept of this
paper.
Definition 3 (labelled bisimulation) A symmetric relation R on programs is a labelled
bisimulation if whenever P R Q the following holds:
τ
τ
(L1) If P → P ′ then ∃ Q′ (Q ⇒ Q′ and P ′ R Q′ ).
νt sv

νt sv

(L2) If P → P ′, P ⇓L , {t} ∩ fn(Q) = ∅ then ∃ Q′ (Q ⇒ Q′ and P ′ R Q′ ).
sv
sv
τ
(L3) If P → P ′ then ∃ Q′ ( ( Q ⇒ Q′ and P ′ R Q′ ) or ( Q ⇒ Q′ and P ′ R (Q′ | sv) ) ).
(L4) If S = s1 v1 | · · · | sn vn , n ≥ 0, P ′ = (P | S) ↓, and P ′ 7→ P ′′ then
τ
∃ Q′ , Q′′ ( (Q | S) ⇒ Q′ , Q′ ↓, P ′ R Q′ , Q′ 7→ Q′′ , and P ′′ R Q′′ ).
We denote with ≈L the largest labelled bisimulation.
In reactive synchronous programming, a program is usually supposed to read ‘input’
signals at the beginning of each instant and to react delivering ‘output’ signals at the end
of each instant. In particular, a program that does not reach a suspension point cannot
produce an observable output signal. For instance, if we run s | Ω then the emission on

12

the signal s should not be observable because the program never suspends. Following this
intuition, we comment on the conditions (L1 − 4).
(L1) This condition is standard in the framework of a bisimulation semantics. As in the
asynchronous case, it exposes the branching structure of a system to the extent that it
distinguishes, e.g., the program (s1 ⊕ s2 ) ⊕ s3 from the program s1 ⊕ (s2 ⊕ s3 ). We will
comment on alternative approaches at the end of this section.
(L2) According to the intuition sketched above, the condition (L2) requires that an output
of a program P is observable only if P ⇓L , i.e., only if P may potentially reach a suspension
point (remember that in Sπ an output persists within an instant). The reasons for choosing
the L-suspension predicate rather than, e.g., the weak suspension predicate will be clarified
in section 4 and have to do with the fact that L-suspension has better properties with
respect to parallel composition. We also anticipate that in the premise of condition (L2),
it is equivalent to require P ⇓L or P ′ ⇓L (cf. remark 19) and that in the conclusion the
property Q′ ⇓L can be derived (cf. proposition 11). Last but not least, we should stress
that in practice we are interested in programs that react at each instant and for this reason,
programs that do not satisfy the L-suspension predicate are usually rejected by means of
static analyses. In this relevant case, the condition (L2) is the usual output condition of
the π-calculus.
(L3) The reception of a signal is not directly observable just as the reception of a message
in the π-calculus with asynchronous communication. For instance, there is no reason to
distinguish s.0, 0 from 0. Techniques for handling this situation have already been developed in the framework of the π-calculus with asynchronous communication and amount to
modify the input clause as in condition (L3) (see [3]). It is a pleasant surprise that this
idea can be transposed to the current context.
(L4) The condition (L4) corresponds to the end of the instant and of course it does not
arise in the π-calculus. The end of the instant is an observable event since, as we explained
above, it is at the end of the instant that we get the results of the program for the current
instant. Let us explain the role of the context S = s1 v1 | · · · | sn vn in this condition.
Consider the programs:
P = s1 .0, A(!s2 )

Q = s1 .0, A([])

A(l) = [l ☎ []]0, s3

Then P ↓, Q ↓, P 7→ A([]), and Q 7→ A([]). However, if we plug P and Q in the context
[·] | s2 then the resulting programs exhibit different behaviours. In other terms, when
comparing two suspended programs we should also consider the effect that emitted values
may have on the computation performed at the end of the instant. We stress that the
context S must preserve the suspension of the program, therefore the emissions in S are
only relevant if they correspond to a signal s which is dereferenced at the end of the instant.
In particular, the number of contexts S to be considered in rule (L4) is finite whenever the
number of distinct values that can be emitted on dereferenced signals is finite (possibly up
to injective renaming).

13

Admittedly, the definition of labelled bisimulation is technical and following previous
work [17, 3, 15], we seek its justification through suitable notions of barbed and contextual
bisimulation.
νt sv

Definition 4 (commitment) We write P ց s if P → · and say that P commits to
emit on s.
Definition 5 (barbed bisimulation) A symmetric relation R on programs is a barbed
bisimulation if whenever P R Q the following holds:
τ
τ
(B1) If P → P ′ then ∃ Q′ Q ⇒ Q′ and P ′ R Q′ .
τ
(B2) If P ց s and P ⇓L then ∃ Q′ (Q ⇒ Q′ , Q′ ց s, and P R Q′ ).
τ
(B3) If P ↓ and P 7→ P ′′ then ∃ Q′ , Q′′ (Q ⇒ Q′ , Q′ ↓, P R Q′ , Q′ 7→ Q′′ , and P ′′ R Q′′ ).
We denote with ≈B the largest barbed bisimulation.
We claim that this is a ‘natural’ definition. Condition (B1) corresponds to the usual
treatment of τ moves. Condition (B2) corresponds to the observation of the output commitments in the π-calculus with asynchronous communication modulo the L-suspension
predicate whose role has already been discussed in presenting the condition (L2). We will
see that the L-suspension predicate ⇓L can be defined just in terms of internal reduction
(remark 10). As in condition (L2), the condition Q′ ⇓L is a consequence of the definition
(cf. proposition 24(2)). Finally, condition (B3) corresponds to the observation of the end
of the instant and it is a special case of condition (L4) where the context S is empty.
Definition 6 A static context C is defined as follows:
C ::= [ ] | C | P | νs C

(1)

A reasonable notion of program equivalence should be preserved by the static contexts,
i.e., by parallel composition and name generation. We define accordingly a notion of
contextual bisimulation (cf. [17, 15]).
Definition 7 (contextual bisimulation) A symmetric relation R on programs is a contextual bisimulation if it is a barbed bisimulation (conditions (B1 −3)) and moreover whenever P R Q then
(C1) C[P ] R C[Q], for any static context C.
We denote with ≈C the largest contextual barbed bisimulation.
Our main result shows that labelled and contextual bisimulation collapse. In particular,
this implies that labelled bisimulation is preserved by the contexts C. The proof will be
developed in the following sections.
Theorem 8 Let P, Q be programs. Then P ≈L Q if and only if P ≈C Q.
14

We claim that our approach to the semantics of the Sπ-calculus is rather natural and
mathematically robust, however we cannot claim that it is more canonical than, say, the
weak, early bisimulation semantics of the π-calculus. We have chosen to explore a path
following our mathematical taste, however, as in the π-calculus, other paths could be explored. In this respect, we will just mention three directions. First, one could remark that
condition (B1) in definition 5 allows to observe the branching structure of a program and
argue that only suspended programs should be observed. This would lead us towards a
failure semantics/testing scenario [13, 9] (in the testing semantics, a program that cannot
perform internal reductions is called stable and this is similar to a suspended program in
the synchronous context). Second, one could require that program equivalence is preserved
by all contexts and not just the static ones and proceed to adapt, say, the concept of open
bisimulation [31] to the present language. Third, one could plead for reduction congruence
[27] rather than for contextual bisimulation and then try to see whether the two concepts coincide following [15]. We refer to the literature for standard arguments concerning
bisimulation vs. testing semantics (e.g., [25]), early vs. open bisimulation (e.g., [31]), and
contextual vs. reduction bisimulation (e.g., [15]).

4

Understanding L-suspension

In this section, we study the properties of the L-suspension predicate and justify its use in
the definition of labelled bisimulation.
Proposition 9 (characterisations of L-suspension) Let P be a program. The following are equivalent:
(1) P ⇓L .
(2) There is a program Q such that (P | Q) ⇓.
(3) There is a static context C (cf. definition 6) such that C[P ] ⇓L .
α

α

Proof. (1 ⇒ 2) Suppose P0 →1 P1 · · · →n Pn and Pn ↓. We build Q by induction on n. If
n = 0 we can take Q = 0. Otherwise, suppose n > 0. By inductive hypothesis, there is Q1
such that (P1 | Q1 ) ⇓. We proceed by case analysis on the first action α1 .
τ
(α1 = τ ) Then we can take Q = Q1 and (P0 | Q) → (P1 | Q1 ).
sv

τ

(α1 = sv) Let Q = (Q1 | sv). We have (P0 | Q) → (P1 | Q1 | sv). Since P1 → P1 , we
observe that (P1 | Q1 ) ⇓ implies (P1 | Q1 | sv) ⇓.
(α1 = νt sv) We distinguish three subcases.
τ

1. If α1 = st then define Q = s(t).Q1 and observe that (P0 | Q) → (P1 | Q1 ).
τ

2. If α1 = νt st then define again Q = s(t).Q1 and observe that (i) (P0 | Q) → νt (P1 |
Q1 ) and (ii) (P1 | Q1 ) ⇓ implies νt (P1 | Q1 ) ⇓.

15

3. If α1 = νt sc(v) then let {t′ } = fn(c(v))\{t} and t′′ a tuple of fresh names (one for
each name in t′ ). We define Q = s(x).[x ☎ [t′′ /t′]c(v)]Q1 , 0 where x, t′′ ∈
/ FV (Q1 )
τ
and observe that: (i) (P0 | Q) ⇒ νt (P1 | Q1 ) and (ii) (P1 | Q1 ) ⇓ implies νt (P1 |
Q1 ) ⇓. For instance, if P0
x, t′′ ∈
/ FV (Q1 ).

νt sc(t,t′ )

→

P1 then we take Q = s(x).[x ☎ c(t, t′′ )]Q1 , 0 with

(2 ⇒ 3) Take C = [ ] | Q and note that by definition (P | Q) ⇓ implies (P | Q) ⇓L .
τ

τ

(3 ⇒ 1) First, check by induction on a static context C that P → · implies C[P ] → ·.
α
Hence, C[P ] ↓ implies P ↓. Second, show that C[P ] → Q implies that Q = C ′ [P ′ ] and
α′

α

α

either P = P ′ or P → P ′ . Third, suppose C[P ] →1 Q1 · · · →n Qn with Qn ↓. Show by
induction on n that P ⇓L .
✷
Remark 10 The second characterisation, shows that the L-suspension predicate can be
defined just in terms of the internal (τ ) transitions and the suspension predicate. Thus it
does not depend on the choice of observing certain labels.
Proposition 11 (L-suspension and labelled equivalence) (1) If ¬P ⇓L and ¬Q ⇓L
then P ≈L Q.
(2) If P ≈L Q and P ⇓L then Q ⇓L .
α

Proof. (1) First we note that ¬P ⇓L and P → P ′ implies ¬P ′ ⇓L . Second, we check
that R = {(P, Q) | ¬P ⇓L and ¬Q ⇓L } is a labelled bisimulation.
τ
τ
(L1) If P → P ′ then ¬P ′ ⇓L . Then Q ⇒ Q and P ′ R Q.
(L2) The condition holds since ¬P ⇓L .
sv
τ
(L3) If P → P ′ then ¬P ′ ⇓L . Then Q ⇒ Q and by proposition 9, ¬Q ⇓L implies
¬(Q | sv) ⇓L .
(L4) The condition holds since ¬(P | S) ↓. Indeed if (P | S) ↓ then (P | S) ⇓L and by
proposition 9, P ⇓L which contradicts the hypothesis.
(2) Suppose P0 ≈L Q0 and P0 ⇓L . We proceed by induction on the length n of the shortest
α
α
sequence of transitions to a suspended program: P0 →1 · · · →n Pn and Pn ↓. If n = 0 then
τ
by (L4), Q0 ⇒ Q′ and Q′ ↓. Thus Q0 ⇓L . If n > 0 then we analyse the first action α1 .
τ
(α1 = τ ) By (L1), Q0 ⇒ Q1 and P1 ≈L Q1 . By inductive hypothesis Q1 ⇓L and therefore
Q0 ⇓L .
νt sv

(α1 = νt sv) By (L2), since P0 ⇓L , we have Q0 ⇒ Q1 and P1 ≈L Q1 . By inductive
hypothesis, Q1 ⇓L . Thus Q0 ⇓L .
sv
(α1 = sv) According to (L3) we have two subcases. If Q0 ⇒ Q1 and P1 ≈L Q1 then
τ
we reason as in the previous case. If Q0 ⇒ Q1 and P1 ≈L (Q1 | sv) then by inductive
hypothesis (Q1 | sv) ⇓L . By proposition 9, if (Q1 | sv) ⇓L then Q1 ⇓L . Thus Q0 ⇓L .
✷

16

Thus labelled bisimulation equates all programs which cannot L-suspend and moreover
it never equates a program which L-suspends to one which cannot. In this sense, Lsuspension is reminiscent of the notion of solvability in the λ-calculus [6, p. 41]. In spite
of these nice properties, one may wonder whether the L-suspension predicate could be
replaced by the suspension or weak suspension predicate.
Definition 12 We denote with ≈↓L (≈⇓L ) the notion of labelled bisimulation obtained by
replacing in (L2) the condition P ⇓L with the condition P ↓ (P ⇓). Similarly, we denote with ≈↓B , ≈↓C (≈⇓B , ≈⇓C ) the notions of barbed and contextual bisimulations obtained by
replacing in (B2) the condition P ⇓L with the condition P ↓ (P ⇓).
Proposition 13 (comparing bisimulations) (1) The following inclusions hold:
≈B ⊂ ≈⇓B ⊂ ≈↓B ,

≈L ⊂ ≈⇓L ⊂ ≈↓L ,

≈C ⊆ ≈⇓C ⊆ ≈↓C .

(2) The barbed bisimulations and the labelled bisimulations ≈⇓L and ≈↓L are not preserved
by parallel composition.
Proof. (1) The non-strict inclusions follow from the remark that P ↓ implies P ⇓ which
implies P ⇓L . We provide examples for the 4 strict inclusions.
• Consider P = (s1 | (s2 ⊕ s3 )) and Q = (s1 | s2 ) ⊕ (s1 | s3 ). Note that P, Q ⇓ but ¬P, Q ↓
and that to reach a suspension point, P and Q have to resolve their internal choices. Now
we have P ≈↓L Q (and therefore P ≈↓B Q) but P 6≈⇓B Q (and therefore P 6≈⇓L Q). To see the
latter, observe that P ց s1 and that to match this commitment Q must choose between
s2 and s3 .
• Let (t, t′ ) abbreviate [t; t′ ] and s → 0, Ω abbreviate s(x).[x ☎ 0]0, Ω. Consider:
P1 = νt, t′ (s(t, t′ ) | (t.s1 ⊕ t.s2 ) | Q)
P2 = νt, t′ (((s(t, t′ ) | (t.s1 )) ⊕ (s(t, t′ ) | (t.s2 ))) | Q)
Q = t′ → 0, Ω | t′ 1
Note that P1 , P2 ⇓L but ¬P1 , P2 ⇓. The point is that the program Q loops unless the name
t′ is extruded to the environment and the latter provides a value 0 on the signal t′ . Then
P1 ≈⇓L P2 . However, P1 6≈L P2 . To see this, notice that P1 ց s and that to match this
commitment, P2 has to resolve first the internal choice between s1 and s2 . A variant of
this example where we remove the input prefix t. before the emissions si , i = 1, 2, shows
that ≈B is strictly included in ≈⇓B .
(2) It is well known that barbed bisimulation is not preserved by parallel composition.
For instance, s.s1 ≈B s.s2 , but (s.s1 | s) 6≈B (s.s2 | s) if s1 6= s2 . To show that ≈↓L and ≈⇓L
are not preserved by parallel composition consider again the programs P1 and P2 above in
parallel with:
R = s(t, t′ ).((t | t′ 0) ⊕ (t | t′ 0 | s3 ))

17

where s(t, t′ ).P abbreviates s(x).[x ☎ [t; t′ ]]P, 0. Remark that
τ

(P1 | R) ⇒ νt, t′ (s(t, t′ ) | (t.s1 ⊕ t.s2 ) | Q | t | t′ 0) ≡ P1′
τ

To match this move, suppose (P2 | R) ⇒ P2′ . Now P2′ must be able to suspend while losing
the possibility of committing on s3 . Hence, there must be a synchronisation on s between
P2 and R. In turn, this synchronisation forces P2 to choose between s1 and s2 . Suppose,
e.g., (P2 | R) chooses s1 , then in a following move P1′ chooses s2 and becomes:
νt, t′ (s(t, t′ ) | s2 | 0 | t | t′ 0 | t′ 1)
which is suspended and commits on s2 . The program P2′ cannot match this move.

✷

Note that in (1) the inclusions for the barbed and labelled bisimulations are strict. On
the other hand, we do not know whether the inclusions of the contextual bisimulations
are strict. However, by (2) we do know that the notions of labelled bisimulation where Lsuspension is replaced by (weak) suspension are not preserved by parallel composition and
therefore cannot characterise the weaker notions of contextual bisimulation. The conclusion
we draw from this analysis is that ≈L is the good notion of labelled bisimulation among
those considered.

5

Strong labelled bisimulation and an up-to technique

It is technically convenient to introduce a strong notion of labelled bisimulation which is
used to bootstrap the reasoning about the weaker notion we are aiming at.
Definition 14 (strong labelled bisimulation) A symmetric relation R on programs is
a strong labelled bisimulation if whenever P R Q the following holds:
α
α
(S1) P → P ′ and bn(α) ∩ fn(Q) = ∅ implies ∃ Q′ (Q → Q′ and P ′ R Q′ ).
(S2) (P | S) ↓ with S = (s1 v1 | · · · | sn vn ), n ≥ 0 and (P | S) 7→ P ′ implies (P | S) R (Q |
S) and ∃ Q′ (Q 7→ Q′ and P ′ R Q′ ).
We denote with ≡L the largest strong labelled bisimulation.
Proposition 15 If P ≡L Q then P ≈L Q.
Proof. We check that ≡L is a labelled bisimulation. Conditions (L1 − 3) follow from condition (S1). Condition (L4) follows from condition (S2) noticing that (P | S) ≡L (Q | S)
and (P | S) ↓ implies by (S1) that (Q | S) ↓.
✷
When comparing strong labelled bisimulation with labelled bisimulation it should be
noticed that in the former not only we forbid weak internal moves but we also drop the
convergence condition in (L2) and the possibility of matching an input with an internal
transition in (L3). For this reason, we adopt the notation ≡L rather than the usual ∼L .
18

Definition 16 We say that a relation R is a strong labelled bisimulation up to strong
labelled bisimulation if the conditions (S1 − 2) hold when we replace R with the larger
relation (≡L ) ◦ R ◦ (≡L ).
The following proposition summarizes some useful properties of strong labelled bisimulation. In the present context, an injective renaming is an injective function mapping
signal names to signal names.
Proposition 17 (properties of ≡L ) (1) If P ≡L Q and σ is an injective renaming then
σP ≡L σQ.
(2) ≡L is a reflexive and transitive relation.
(3) The following laws hold:
(P | 0) ≡L P,
P1 | (P2 | P3 ) ≡L (P1 | P2 ) | P3 ,
(P1 | P2 ) ≡L (P2 | P1 ),
νs1 , s2 P ≡L νs2 , s1 P
νs P1 | P2 ≡L νs (P1 | P2 ) if s ∈
/ fn(P2 ).
(4) If P ≡L Q then (P | S) ≡L (Q | S) where S = (P1 | · · · | Pn ) and Pi = 0 or Pi = si vi ,
for i = 1, . . . , n, n ≥ 0.
Proof hint. Most properties follow by routine verifications. We just highlight some
points.
(2) Recalling that P ≡L Q and P ↓ implies Q ↓.
(3) Introduce a notion of normalised program where parallel composition associates to the
left, all restrictions are carried at top level, and 0 programs are the identity for parallel
composition. Then define a relation R where two programs are related if their normalised
forms are identical up to bijective permutations of the restricted names and the parallel
components. A pair of programs equated by the laws under consideration is in R. Show
that R is a strong labelled bisimulation.
(4) Show that {(P | S, Q | S) | P ≡L Q} is a strong labelled bisimulation where S is
defined as in the statement.
✷
The following proposition summarizes the properties of the output transition.
νt sv

Proposition 18 (emission) (1) If P → P ′ then P ≡L νt (sv | P ′′ ) and P ′ ≡L (sv |
P ′′ ).
νt sv

(2) If P → P ′ then P ⇓L if and only if P ′ ⇓L .
νt sv

Proof. (1) In deriving P → P ′ one can only rely on the rules (out, par, ν, νex ). We
use the laws of strong labelled bisimulation (proposition 17(2)) to put the program in the
desired form.
(2) By definition, P ′ ⇓L implies P ⇓L . In the other direction, relying on (1), assume
that the program has the shape νt (sv | P ). We also know that this program L-suspends.
19

By proposition 9, there is a program Q such νt (sv | P ) | Q ⇓. That is, assuming
{t} ∩ fn(Q) = ∅, we have that νt (sv | P | Q) ⇓. The latter implies that there is a Q′ such
τ
that (sv | P | Q) ⇒ Q′ and Q′ ↓. Again, by proposition 9, this means that (sv | P ) ⇓L . ✷
Remark 19 By proposition 18(2), in condition (L2) of definition 3, it is equivalent to
require P ⇓L or P ′ ⇓L .
Our main application of strong labelled bisimulation is in the context of a rather standard ‘up to technique’.
Definition 20 A relation R is a labelled bisimulation up to ≡L if the conditions (L1 − 4)
are satisfied when we replace the relation R with the (larger) relation (≡L ) ◦ R ◦ (≡L ).
Proposition 21 (up-to technique) Let R be a labelled bisimulation up to ≡L . Then:
(1) The relation (≡L ) ◦ R ◦ (≡L ) is a labelled bisimulation.
(2) If P R Q then P ≈L Q.
Proof. (1) A direct diagram chasing using proposition 17.
(2) Follows directly from (1).

6

✷

Congruence properties of labelled bisimulation

We are now ready to study the congruence properties of labelled bisimulation. The most
important part of the proof concerns the preservation under parallel composition and name
generation and it is composed of 12 cases.
Proposition 22 (1) If P1 ≈L P2 and σ is an injective renaming then σP1 ≈L σP2 .
(2) If P1 ≈L P2 then (P1 | sv) ≈L (P2 | sv).
(3) The relation ≈L is reflexive and transitive.
(4) If P1 ≈L P2 then νs P1 ≈L νs P2 and (P1 | Q) ≈L (P2 | Q).
Proof. (1) By propositions 17(1) and 15.
(2) We show that the relation R =≈L ∪{( P1 | sv, P2 | sv ) | P1 ≈L P2 } is a labelled
bisimulation up to ≡L . We assume P1 ≈L P2 and we analyse the conditions (L1 − 4).
τ

(L1) Suppose (P1 | sv) → (P1′ | sv). If the action τ is performed by P1 then the hypothesis
sv
and condition (L1) allow to conclude. Otherwise, suppose P1 → P1′ . Then we apply the
sv
hypothesis and condition (L3). Two cases may arise: (1) If P2 ⇒ P2′ and P1′ ≈L P2′ then
τ
the conclusion is immediate. (2) If P2 ⇒ P2′ and P1′ ≈L (P2′ | sv) then we note that
(P2′ | sv) ≡L (P2′ | sv) | sv and we close the diagram up to ≡L .

20

νt s′ v

(L2) Suppose (P1 | sv) ⇓L and (P1 | sv) → (P1′ | sv). If the emission action is performed
by sv then the conclusion is immediate. Otherwise, note that P1 ⇓L . Hence by (L2),
νt s′ v

νt s′ v

P2 ⇒ P2′ and P1′ ≈L P2′ . But then (P2 | sv) ⇒ (P2′ | sv) and we can conclude.
s′ v ′

s′ v ′

(L3) Suppose (P1 | sv) → (P1′ | sv). Necessarily, P1 → P1′ . By (L3), two cases may arise.
s′ v ′

τ

If P2 ⇒ P2′ and P1′ ≈L P2′ then the conclusion is direct. On the other hand, if P2 ⇒ P2′
and P1′ ≈L (P2′ | s′ v ′ ) then we note that
(P1′ | sv) R ((P2′ | s′ v ′ ) | sv) ≡L ((P2′ | sv) | s′ v ′ )
and we close the diagram up to ≡L .
(L4) Let S = s1 v1 | · · · | sn vn . Suppose (P1 | sv | S) ↓ and (P1 | sv | S) 7→ P1′ . By
τ
(L4) applied to (sv | S), we derive that (P2 | sv | S) ⇒ (P2′′ | sv | S), (P2′′ | sv | S) ↓,
(P1 | sv | S) ≈L (P2′′ | sv | S), (P2′′ | sv | S) 7→ P2′ , and P1′ ≈L P2′ .
(3) It is easily checked that the identity relation is a labelled bisimulation. Reflexivity follows. As for transitivity, we check that the relation R =≈L ◦ ≈L is a labelled bisimulation
up to ≡L . Suppose P1 ≈L P2 ≈L P3 .
(L1) Standard argument.
νt sv

(L2) Suppose P1 ⇓L and P1 → P1′ . Note that by (1) we can assume that the names t are
νt sv
not in P2 . By (L2), P2 ⇒ P2′ and P1′ ≈L P2′ . By proposition 18(2), P1 ⇓L implies P1′ ⇓L .
By proposition 11(2), P1′ ⇓L and P1′ ≈L P2′ implies P2′ ⇓L . We conclude by applying (L1)
and (L2) to P2 and P3 .
sv

(L3) Suppose P1 → P1′ . Two interesting cases arise when either P2 or P3 match an
τ
input action with an internal transition. (1) Suppose first P2 ⇒ P2′ and P1 ≈L (P2′ | sv).
τ
By P2 ≈L P3 and repeated application of (L1) we derive that P3 ⇒ P3′ and P2′ ≈L P3′ .
By property (2), the latter implies that (P2′ | sv) ≈L (P3′ | sv) and we combine with
τ
sv
τ
P1 ≈L (P2′ | sv) to conclude. (2) Next suppose P2 ⇒ P21 → P22 ⇒ P2′ and P1 ≈L P2′ .
τ
τ
Suppose that P3 matches these transitions as follows: P3 ⇒ P31 ⇒ P32 , P22 ≈L (P32 | sv),
τ
and moreover (P32 | sv) ⇒ (P3′ | sv) with P2′ ≈L (P3′ | sv). Two subcases may arise: (i)
τ
τ
sv
P32 ⇒ P3′ . Then we have P3 ⇒ P3′ , P2′ ≈L (P3′ | sv) and we can conclude. (ii) P32 ⇒ P3′ .
sv
Then we have P3 ⇒ P3′ and P2′ ≈L (P3′ | sv) ≡L P3′ . Note that P32 does not need to perform
the action sv more than once.
(L4) Let S = s1 v1 | · · · | sn vn . Suppose (P1 | S) ↓ and (P1 | S) 7→ P1′ . By (L4),
τ
(P2 | S) ⇒ (P2′′ | S), (P2′′ | S) ↓, (P1 | S) ≈L (P2′′ | S), (P2′′ | S) 7→ P2′ , and P1′ ≈L P2′ .
τ
τ
By (L1), (P3 | S) ⇒ (P3′′ | S) and (P2′′ | S) ≈L (P3′′ | S). By (L4), (P3′′ | S) ⇒ (P3′′′ | S),
(P3′′′ | S) ↓, (P2′′ | S) ≈L (P3′′′ | S), (P3′′′ | S) 7→ P3′ , P2′ ≈L P3′ and we can conclude.
(4) We show that R = {(νt (P1 | Q), νt (P2 | Q)) | P1 ≈L P2 }∪ ≈L is a labelled
bisimulation up to ≡L .
τ

(L1) Suppose νt (P1 | Q) → ·. This may happen because either P1 or Q perform a τ action
or because P1 and Q synchronise. We consider the various situations that may occur.
21

τ

τ

(L1)[1] Suppose Q → Q′ . Then νt (P2 | Q) → νt (P2 | Q′ ) and we can conclude.
τ
τ
τ
(L1)[2] Suppose P1 → P1′ . By (L2) P2 ⇒ P2′ and P1′ ≈L P2′ . Then νt (P2 | Q) ⇒ νt (P2′ |
Q) and we can conclude.
νt′ sv

sv

(L1)[3] Suppose P1 → P1′ and Q → Q′ . According to (L3), we have two subcases.
sv
τ
(L1)[3.1] Suppose P2 ⇒ P2′ and P1′ ≈L P2′ . Then νt (P2 | Q) ⇒ νt, t′ (P2′ | Q′ ) and we can
conclude.
τ
(L1)[3.2] Suppose P2 ⇒ P2′ and P1′ ≈L (P2′ | sv). By proposition 18(2), Q ≡L νt′ Q′ and
τ
Q′ ≡L (Q′′ | sv) for some Q′′ . Then νt (P2 | Q) ⇒ νt (P2′ | Q) ≡L νt, t′ (P2′ | sv) | Q′′ and
we can conclude up to ≡L .
νt′ sv

sv

(L1)[4] Suppose P1 → P1′ and Q → Q′ . We have two subcases.
(L1)[4.1] Suppose ¬P1 ⇓L . By propositions 9 and 11, ¬νt (P1 | Q) ⇓L , ¬P2 ⇓L , ¬νt (P2 |
Q) ⇓L , ¬P1′ ⇓L , and ¬νt, t′ (P1′ | Q′ ) ⇓L . Hence, νt, t′ (P1′ | Q′ ) ≈L νt (P2 | Q) and we can
conclude.
νt′ sv
τ
(L1)[4.2] Suppose P1 ⇓L . By (L2), P2 ⇒ P2′ and P1′ ≈L P2′ . Hence νt (P2 | Q) ⇒
νt, t′ (P2′ | Q′ ) and we can conclude.
νt′ sv

(L2) Suppose νt (P1 | Q) → · and νt (P1 | Q) ⇓L . Also assume t = t1 , t2 and t′ = t1 , t3
up to reordering so that the emission extrudes exactly the names t1 among the names in
t. We have two subcases depending which component performs the action.
νt

νt′ sv

sv

3
(L2)[1] Suppose Q →
Q′ . Then νt (P2 | Q) → νt2 (P2 | Q′ ) and we can conclude.

νt

sv

νt

sv

3
3
P1′ . By proposition 9, we know that P1 ⇓L . Hence P2 ⇒
P2′
(L2)[2] Suppose P1 →

νt′ sv

and P1′ ≈L P2′ . Then νt (P2 | Q) → νt2 (P2′ | Q) and we can conclude.
sv

(L3) Suppose νt (P1 | Q) → · We have two subcases depending which component performs
the action.
sv
sv
(L3)[1] Suppose Q → Q′ . Then νt (P2 | Q) → νt (P2 | Q′ ) and we can conclude.
sv
(L3)[2] Suppose P1 → P1′ . According to (L3) we have two subcases.
sv
sv
(L3)[2.1] Suppose P2 ⇒ P2′ and P1′ ≈L P2′ . Then νt (P2 | Q) ⇒ νt (P2′ | Q) and we can
conclude.
τ
τ
(L3)[2.2] Suppose P2 ⇒ P2′ and P1′ ≈L (P2′ | sv). Then νt (P2 | Q) ⇒ νt (P2′ | Q) and
since νt (P2′ | Q) | sv ≡L νt ((P2′ | sv) | Q) we can conclude up to ≡L .
(L4) Suppose S = s1 v1 | · · · | sn vn and νt (P1 | Q) | S ↓. Up to strong labelled
bisimulation, we can express Q as νtQ (SQ | IQ ) where SQ is the parallel composition of
emissions and IQ is the parallel composition of receptions. Thus we have: νt (P1 | Q) |
S ≡L νt, tQ (P1 | SQ | IQ | S), and νt (P2 | Q) | S ≡L νt, tQ (P2 | SQ | IQ | S) assuming
{t} ∩ fn(S) = ∅ and {tQ } ∩ fn(Pi | S) = ∅ for i = 1, 2.
If νt (P1 | Q) | S 7→ P then P ≡L νt, tQ (P1′′ | Q′ ) where in particular, we have that
(P1 | SQ | S) ↓ and (P1 | SQ | S) 7→ (P1′ | 0 | 0).

22

τ

By the hypothesis P1 ≈L P2 and (L4) we derive that: (i) (P2 | SQ | S) ⇒ (P2′′ | SQ | S),
(ii) (P2′′ | SQ | S) ↓, (iii) (P2′′ | SQ | S) 7→ (P2′ | 0 | 0), (iv) (P1 | SQ | S) ≈L (P2′′ | SQ | S),
and (v) (P1′ | 0 | 0) ≈L (P2′ | 0 | 0).
Because (P1 | SQ | S) and (P2′′ | SQ | S) are suspended and labelled bisimilar, the
two programs must commit (cf. definition 4) on the same signal names and moreover
on each signal name they must emit the same set of values up to renaming of bound
names. It follows that the program νt, tQ (P2′′ | SQ | IQ | S) is suspended. The only
possibility for an internal transition is that an emission in P2′′ enables a reception in IQ
but this contradicts the hypothesis that νt, tQ (P1 | SQ | IQ | S) is suspended. Moreover,
(P2′′ | SQ | IQ | S) 7→ (P2′ | 0 | Q′ | 0).
Therefore, we have that
τ

νt (P2 | Q) | S ≡L νt, tQ (P2 | SQ | IQ | S) ⇒ νt, tQ (P2′′ | SQ | IQ | S),
νt, tQ (P2′′ | SQ | IQ | S) ↓, and νt, tQ (P2′′ | SQ | IQ | S) 7→ νt, tQ (P2′ | 0 | Q′ | 0). Now
νt, tQ (P1 | SQ | IQ | S) R νt, tQ (P2′′ | SQ | IQ | S) because (P1 | SQ | S) ≈L (P2′′ | SQ | S)
and νt, tQ (P1′ | Q′ ) R νt, tQ (P2′ | Q′ ) because P1′ ≈L P2′ .
✷
We can now derive the first half of the proof of theorem 8.
Corollary 23 Let P, Q be programs. Then P ≈L Q implies P ≈C Q.
Proof. Labelled bisimulation is a barbed bisimulation and by proposition 22 it is preserved by the contexts C. Hence it is a contextual bisimulation.
✷

7

Building discriminating contexts

To complete the proof of theorem 8, it remains to show that our contexts are sufficiently
strong to make all distinctions labelled bisimulation does. First we note the analogous of
proposition 11 for contextual bisimulation.
Proposition 24 (1) If ¬P ⇓L and ¬Q ⇓L then P ≈C Q.
(2) If P ≈C Q and P ⇓L then Q ⇓L .
Proof. (1) By proposition 11, P ≈L Q and by corollary 23, P ≈C Q.
τ

(2) By proposition 9, there is a program R such that (P | R) ⇓, i.e., (P | R) ⇒ P1 and
τ
P1 ↓. By (C1), (P | R) ≈C (Q | R). By (B1), (Q | R) ⇒ Q′1 and P1 ≈C Q′1 . By (B3),
τ
Q′1 ⇒ Q1 and Q1 ↓. Thus (Q | R) ⇓ and again by proposition 9 this implies that Q ⇓L . ✷
Proposition 25 If P ≈C Q then P ≈L Q.

23

Proof. We denote with ai , bi , ci , . . . ‘fresh’ signal names not occurring in the programs
under consideration. We will rely on the signal names ai to extrude the scope of some signal
names and on the signal names bi , ci to monitor the internal transitions of the programs.
We define a relation R:
P1 R P2 if νt (P1 | O) ≈C νt (P2 | O) for some t, O,
where: t = t1 . . . , tn , O = a1 t1 | · · · | an tn , {a1 , . . . , an } ∩ fn(P1 | P2 ) = ∅.
By definition, if P1 ≈C P2 then P1 R P2 taking t as the empty vector and O as the empty
parallel composition. The purpose of the relation R is to enlarge the definition of contextual
bisimulation so that some signal names t are at once restricted and observable thanks to
the emission performed by O. We will will show that R is a labelled bisimulation up to
strong labelled bisimulation so that we have the following implications:
P1 ≈C P2

⇒

P1 R P2

⇒

P1 ≈L P2 .

• We have seen in section 2.5 that an internal choice operator ⊕ is definable in the Sπcalculus. In order to simplify the notation, in the following we assume that P1 ⊕ P2 reduces
to either P1 or P2 by just one τ -transition. In reality, the reduction takes one τ -transition
to perform the internal choice, a second deterministic τ -transition to select the right branch
of the matching operator, and some garbage collection to remove signals that are under
the scope of a restriction and cannot be received. The second transition and the garbage
collection do not affect the structure of the proof and we will ignore them.
• Assuming O = a1 t1 | · · · | an tn and a = a1 , . . . , an , we will repeatedly use a program
R(a)[P ] which is defined as follows:
R(a)[P ] = a1 (t1 ).b1 ⊕ (c1 ⊕
a2 (t2 ).b2 ⊕ (c2 ⊕
...
an (tn ).bn ⊕ (cn ⊕ P ) . . .)
Next we assume P1 R P2 because νt (P1 | O) ≈C νt (P2 | O) for some t, O, and consider
the conditions (L1 − 4).
τ

τ

τ

(L1) Suppose P1 → P1′ . Then νt (P1 | O) → νt (P1′ | O). By (B1), νt (P2 | O) ⇒ Q
and νt (P1′ | O) ≈C Q. Note however that O cannot interact with P2 and its derivatives
τ
because the signal names a do not occur in (P1 | P2 ). Hence it must be that P2 ⇒ P2′ and
Q = νt (P2′ | O). Then by definition of the relation R, we derive that P1′ R P2′ .
νt′ sv

(L2) Suppose P1 ⇓L and P1 → P1′ with t′ = t′1 , . . . , t′m . Let X = fn(P1 | P2 ). Let
R = R(a)[s(x).[x = νt′ v]X∪{t′ } (bn+1 ⊕ (cn+1 ⊕ O ′))], where
O ′ = an+1 t′1 | · · · | an+m t′m
Now we have:

τ

νt (P1 | O) | R ⇒ νt, t′ (P1′ | O | O ′)
24

by a series of reductions where first R interacts with O to learn the names t1 . . . , tn , then
it interacts with P1 to read a value νt′ v (note that the freshness of t′ is checked with
respect to both X and t), and finally it emits with O ′ the names t′ extruded by P1 . We
remark that in all the intermediate steps the program has the L-suspension property, thus
condition (B2) applies and in particular the commitments on bi , ci are observable.
Next, we decompose this series of reductions in several steps and analyse how the
program νt (P2 | O) | R may match them according to the definition of contextual bisimulation. Suppose first
τ

νt (P1 | O) | R ⇒ νt1 (νt2 , . . . , tn (P1 | O) | (c1 ⊕ a2 (t2 ) · · · ))
The reduced program cannot commit on b1 while it can commit on c1 . If νt (P2 | O) | R
has to match this reduction, then R must necessarily perform the input action and stop
at the same point of the control (c1 ⊕ a2 (t2 ) · · · ). By this communication, the scope of
the restricted name t1 is extruded to R. The program O is composed only of emissions
and therefore it cannot change. The program P2 may perform some internal actions but it
cannot interact with O and R.
τ
If we repeat this argument n times, we conclude that νt (P1 | O) | R ⇒ νt (P1 |
τ
τ
O | cn ⊕ s(x) · · · ) and νt (P2 | O) | R ⇒ νt (P2′ | O | cn ⊕ s(x) · · · ) where P2 ⇒ P2′ .
Now the first program performs a communication on s between P1 and the residual of R
and, provided the emitted value has the expected shape νt′ v, it reduces to νt, t′ (P1′ |
νt′ sv

O | cn+1 ⊕ O ′). In order to match this transition, it must be that P2′ ⇒ P2′′ and the
second program reduces to νt, t′ (P2′′ | O | cn+1 ⊕ O ′ ). Now if the first program moves to
τ
νt, t′ (P1′ | O | O ′), the second must move to νt, t′ (P2′′′ | O | O ′ ) where P ′′ ⇒ P2′′′ and
τ

νt′ sv

τ

νt, t′ (P1′ | O | O ′) ≈C νt, t′ (P2′′′ | O | O ′ ). Since P2 ⇒ · ⇒ · ⇒ P2′′′ , we can conclude
νt′ sv

that P2 ⇒ P2′′′ and P1′ R P2′′′ .
sv

(L3) Suppose P1 → P1′ . We consider two subcases.
(L3)[1] Suppose ¬P1 ⇓L . Then, ¬P1′ ⇓L . By proposition 9, ¬νt (P1 | O) ⇓L and ¬νt (P1′ |
O) ⇓L . By proposition 24, ¬νt (P2 | O) ⇓L . Let us show that the latter implies ¬P2 ⇓L .
τ
If P2 ⇓L , by proposition 9 there is a Q such that (P2 | Q) ⇒ Q′ and Q′ ↓. Then we would
have:
τ
τ
νt (P2 | O) | R(a)[Q] ⇒ νt (P2 | O | Q) ⇒ νt Q′ | O .
Now if Q′ ↓ then νt Q′ | O ↓, and this contradicts the hypothesis that ¬νt (P2 | O) ⇓L .
τ
Thus P2 ⇒ P2 , ¬(P2 | sv) ⇓L , and P1′ ≈L (P2 | sv).
(L3)[2] Suppose P1 ⇓L . In this case, the commitments are observable. We define
R = R(a)[sv]
τ

τ

Then νt (P1 | O) | R ⇒ νt (P1′ | O | sv) and νt (P2 | O) | R ⇒ νt (P2′ | O | sv). We note
sv
that νt (P1′ | O | sv) ≡L νt (P1′ | O) since P1 → P1′ . We have two subcases.
sv

(L3)[2.1] Suppose P2 ⇒ P2′ . Then P2′ ≡L (P2′ | sv) and therefore P1′ R P2′ up to ≡L .
25

τ

(L3)[2.2] Suppose P2 ⇒ P2′ . Then P1′ R (P2′ | sv) up to ≡L .
(L4) Suppose (P1 | S) ↓ and (P1 | S) 7→ P1′ . We consider
R1 = R(a)[S]

R2 = R(a)[S | pause.O]

By (C1), νt (P1 | O) | Ri ≈C νt (P2 | O) | Ri for i = 1, 2. Also
τ

νt (P1 | O) | R1 ⇒ νt (P1 | O | S) ↓
and

τ

νt (P1 | O) | R2 ⇒ νt (P1 | O | S | pause.O) 7→ νt (P1′ | O) .
Then we must have:
τ
(1) νt (P2 | O) | R1 ⇒ νt (P2′′ | O | S) ↓ and νt (P1 | O | S) ≈C νt (P2′′ | O | S). By
τ
definition of O and R1 this implies that (P2 | S) ⇒ (P2′′ | S) and (P2′′ | S) ↓.
τ
(2) νt (P2 | O) | R2 ⇒ νt (P2′′ | O | S | pause.O) 7→ νt (P2′ | O) and νt (P1′ | O) ≈C
νt (P2′ | O). Again by definition of O we have that (P2′′ | S) 7→ P2′ .
✷

8

Conclusion

We have proposed a synchronous version of the π-calculus which borrows the notion of
instant from the SL model–a relaxation of the Esterel model. We have shown that the
resulting language is amenable to a semantic treatment similar to that available for the πcalculus. Retrospectively, we feel that the developed theory relies on two key insights: the
introduction of the notion of L-suspension and the remark that the observation of signals
is similar to the observation of channels with asynchronous communication.

References
[1] R. Amadio. The SL synchronous language, revisited. Journal of Logic and Algebraic Programming,
70:121-150, 2007.
[2] R. Amadio, G. Boudol, F. Boussinot and I. Castellani. Reactive programming, revisited. In Proc.
Workshop on Algebraic Process Calculi: the first 25 years and beyond, Electronic Notes in Theoretical
Computer Science, 162:49-60, 2006.
[3] R. Amadio, I. Castellani and D. Sangiorgi. On bisimulations for the asynchronous π-calculus. In
Theoretical Computer Science, 195:291-324, 1998.
[4] R. Amadio, S. Dal-Zilio. Resource control for synchronous cooperative threads. Theoretical Computer
Science 358:229-254, 2006.
[5] D. Austry and G. Boudol. Algèbre de processus et synchronisation. In Theoretical Computer Science,
30:91-131, 1984.
[6] H. Barendregt. The lambda calculus. North-Holland, revised edition, 1984.
[7] M. Berger. Congruence for two timed asynchronous π-calculi. In Proc. CONCUR, Springer LNCS
3170:115-130, 2004.

26

[8] G. Berry and G. Gonthier. The Esterel synchronous programming language. Science of computer
programming, 19(2):87–152, 1992.
[9] M. Boreale, R. De Nicola and R. Pugliese. Trace and testing equivalence on asynchronous processes.
Information and Computation, 172(2):139-164, 2002.
[10] G. Boudol. ULM, a core programming model for global computing. In Proc. of ESOP, Springer LNCS
2986:234–248, 2004.
[11] F. Boussinot. Reactive C: An extension of C to program reactive systems. Software Practice and
Experience, 21(4):401–428, 1991.
[12] F. Boussinot and R. De Simone. The SL synchronous language. IEEE Trans. on Software Engineering,
22(4):256–266, 1996.
[13] I. Castellani and M. Hennessy. Testing theories for asynchronous languages. In Proc FST-TCS,
SLNCS 1530:90–101, 1998.
[14] P. Caspi and D. Pilaud and N. Halbwachs and J. Plaice. LUSTRE: a declarative language for
programming synchronous systems. ACM POPL, pages 178-188, 1987.
[15] C. Fournet and G. Gonthier. A hierarchy of equivalences for asynchronous calculi (extended abstract)
In Proc. ICALP, SLNCS 1443:844–855, 1998.
[16] M. Hennessy and J. Rathke. Bisimulations for a calculus of broadcasting systems. In Theoretical
Computer Science, 200(1-2):225-260, 1998.
[17] K. Honda and N. Yoshida. On reduction-based process semantics. In Theoretical Computer Science,
151(2):437-486, 1995.
[18] J. Hopcroft and J. Ullman. Introduction to automata theory, languages, and computation. PrenticeHall, 1989.
[19] L. Lamport and N. Lynch. Distributed computing: models and methods. In Handbook of Theoretical
Computer Science, volume B. Elsevier, 1990.
[20] N. Lynch. Distributed algorithms. Morgan-Kaufmann, 1996.
[21] L. Mandel and M. Pouzet. ReactiveML, a reactive extension to ML. In Proc. ACM Principles and
Practice of Declarative Programming, pages 82–93, 2005.
[22] A. Matos, G. Boudol and I. Castellani. Typing non-inteference for reactive programs. RR-INRIA
5594, June 2005. To appear in Journal of Logic and Algebraic Programming.
[23] M. Merro, F. Zappa Nardelli. Behavioral theory for mobile ambients. Journal of the ACM, 52(6):9611023, 2005.
[24] R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25(3):267–310, 1983.
[25] R. Milner. Communication and concurrency. Prentice-Hall, 1989.
[26] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, parts 1-2. Information and
Computation, 100(1):1–77, 1992.
[27] R. Milner and D. Sangiorgi. Barbed bisimulation. In Proc. ICALP, SLNCS 623:685–695, 1992.
[28] J. Ousterhout. Why threads are a bad idea (for most purposes). Invited talk at the USENIX Technical
Conference, 1996.
[29] K.V.S. Prasad. A calculus of broadcasting systems. In Sci. Comput. Program., 25(2-3):285-327, 1995.
[30] Reactive programming, INRIA, Mimosa Project. http://www-sop.inria.fr/mimosa/rp.

27

[31] D. Sangiorgi. A theory of bisimulation for the π-calculus. Acta Informatica, 33(1):69-97, 1996.
[32] V. Saraswat, R. Jagadeesan, and V. Gupta. Timed default concurrent constraint programming. In
Journal of Symbolic computation, 22(5,6) 475-520, 1996.
[33] M. Serrano, F. Boussinot, and B. Serpette. Scheme fair threads. In Proc. ACM Principles and practice
of declarative programming, pages 203-214, 2004.
[34] G. Tel Introduction to distributed algorithms. Cambridge University Press, 1994

28

