arXiv:cs/0511092v1 [] 28 Nov 2005

The SL synchronous language, revisited
Roberto M. Amadio∗
Université Paris 7†
5th June 2017

Abstract
We revisit the SL synchronous programming model introduced by Boussinot and
De Simone (IEEE, Trans. on Soft. Eng., 1996). We discuss an alternative design
of the model including thread spawning and recursive definitions and we explore
some basic properties of the revised model: determinism, reactivity, CPS translation
to a tail recursive form, computational expressivity, and a compositional notion of
program equivalence.

1

Introduction

In synchronous models the computation of a set of participants is regulated by a notion of
instant. The Synchronous Language introduced in [8] belongs to this category. A program
in this language generally contains sub-programs running in parallel and interacting via
shared signals. By default, at the beginning of each instant a signal is absent and once it
is emitted it remains in that state till the end of the instant. The model can be regarded
as a relaxation of the Esterel model [5] where the reaction to the absence of a signal is
delayed to the following instant, thus avoiding the difficult problems due to causality cycles
in Esterel programs.
The model has gradually evolved into a programming language for concurrent applications and has been implemented in the context of various programming languages such
as C, Java, Scheme, and Caml (see, e.g., [19, 20, 13]). The design accommodates a dynamic computing environment with threads entering or leaving the synchronisation space
[6]. In this context, it seems natural to suppose that the scheduling of the threads is only
determined at run time (as opposed to certain synchronous languages such as Esterel
or Lustre). It appears that many typical “concurrent” applications such as event-driven
controllers, data flow architectures, graphical user interfaces, simulations, web services,
multiplayer games, are more effectively programmed in the synchronous framework.
∗
†

Partially supported by ACI Sécurité Informatique CRISS.
Laboratoire Preuves, Programmes et Systèmes, UMR-CNRS 7126.

1

The SL language was carefully designed to be compiled to finite state automata. Motivated by the evolution of the language mentioned above, we consider a synchronous
language including thread spawning, and recursive definitions (section 2) and we explore
some basic properties of the revised model. First, we prove that the resulting language is
deterministic and provide a simple static analysis that entails reactivity (section 3). Second, we propose a continuation passing style translation to a more basic language of tail
recursive threads (section 4). Third, we show that the language without signal generation
has the same computational power as a class of ‘monotonic’ Mealy machines, while the language with signal generation is Turing equivalent (section 5). Fourth, we introduce a notion
of contextual barbed bisimulation and characterise it via a suitable labelled bisimulation
(section 6). Some standard proofs are delayed to the appendix A.

1.1

Related work

This work is a continuation of [1] where we outline results and problems connected with
the SL model 10 years after its proposal. A determinacy theorem was already stated in the
original paper [8] with a similar proof based on the confluence of the ‘small step’ reduction.
Of course, many other determinacy theorems occur in the literature on synchronous programming (cf., e.g., [12]). The static analysis technique for ensuring reactivity is inspired
by previous work by the author [3, 4] where, roughly, the reactivity of a (tail recursive)
SL model with data types is studied. The tail recursive SL model and the related CPS
translation appear to be original. They arose out of an attempt to understand the relative
expressivity of various synchronous operators such as await, when and watch. The results
on the computational expressivity of the revised model, notably its characterisation via
monotonic Mealy machine, were motivated by the compilation to finite state machines in
the original SL proposal [8]. Finally, there seems to be no previous attempt at developing a compositional notion of bisimulation equivalence for the SL model in a CCS style.
However a specific notion of bisimulation for ‘closed systems’ has been proposed recently
in the framework of the work on non-interference for synchronous systems [14].

2

The model

In this section, we present a formalisation of the model which is largely inspired by the
original proposition [8] and a recent survey [1]. We anticipate that in section 4 we will
simplify the control structure by moving to a tail recursive model and in section 6 we will
discuss an alternative presentation in the spirit of process calculi.

2.1

Environments

We assume a countable set S of signal names s, s′ , . . .. We suppose a subset Int =
Input ∪ Output of S of observable signal names representing input or output signals and
such that S\Int is infinite. An environment E is a partial function from signal names to
2

boolean values true and false whose domain of definition dom(E) contains Int and such
that S\dom(E) is infinite.

2.2

Threads

We denote with x a vector of elements x1 , . . . , xn , n ≥ 0 and with [ / ] the usual substitution. By default, bound names can be renamed. We denote with A(s), B(s), . . . thread
identifiers with parameters s. As usual, each thread identifier is defined by exactly one
equation A(x) = T where T is a thread defined by the grammar:
T ::= 0 | (T ; T ) | (emit s) | (νs T ) | (thread T ) | (await s) | (watch s T ) | A(s)
and the signal names free in T are contained in {x}. Sometimes, some of the parameters
(possibly all) are fixed and in these cases we will feel free to omit them. A thread is executed
relatively to an environment which is shared with other parallel threads. The intended
semantics is as follows: 0 is the terminated thread; T ; T is the usual sequentialisation;
(emit s) emits s, i.e. sets to true the signal s and terminates, (νs T ) creates a fresh signal
which is local to the thread T (s is bound in T ) and executes T ; (thread T ) spawns a
thread T which will be executed in parallel and terminates; (await s) terminates if the
signal s is present and suspends the execution otherwise; (watch s T ) allows the execution
of T but terminates T at the end of the first instant where the signal s is present. The
implementation of the watch instruction requires to stack the signals that may cause the
abortion of the current thread together with the associated continuations. For instance,
in (watch s1 (watch s2 T1 ); T2 ); T3 , we start executing T1 . Assuming that at the end of
the instant, the execution of T1 is not completed, the computation in the following instant
resumes with T3 if s1 was present at the end of the instant, with T2 if s1 was absent and s2
was present at the end of the instant, and with the residual of T1 , otherwise. We point out
that a thread spawned by the thread instruction, escapes the watch signals and the related
continuations.

2.3

Thread reduction

A program P is a finite non-empty multi-set of threads. We denote with sig(T ) (sig(P )) the
set of signals free in T (in threads in P ). Whenever we write (T, E), (P, E) it is intended
that sig(T ) ⊆ dom(E), sig(P ) ⊆ dom(E), respectively. All reduction rules maintain the
invariant that the signals defined in the thread or in the program are in the domain of
definition of the associated environment. In particular, all signal names which are not
in the domain of definition of the environment are guaranteed to be fresh, i.e., not used
elsewhere in the program. Finally, we make the usual assumption that reduction rules are
given modulo renaming of the bound signal names.
We assume that sequential composition ‘;’ associates to the right. A redex ∆ is defined
by the grammar:
∆ ::= 0; T | (emit s) | (νs T ) | (thread T ) | (await s) | (watch s 0) | A(s) .
3

An evaluation context C is defined by the grammar:
C ::= [ ] | [ ]; T | (watch s C) | (watch s C); T .
We have a canonical decomposition of a thread in an evaluation context and a redex whose
proof is delayed to appendix A.1.
Proposition 1 (unique decomposition) A thread T 6= 0 admits a unique decomposition T = C[∆] into an evaluation context C and a redex ∆. Moreover, if T = 0 then no
decomposition exists.
P

The reduction relation (T, E) → (T ′ , E ′ ) is defined first on redexes by the rules (T1−7 )
and then it is lifted to threads by the rule (T8 ):
∅

(T1 ) (0; T, E)

→ (T, E)

(T2 ) (emit s, E)

→ (0, E[true/s])

∅

∅

(T3 ) (watch s 0, E) → (0, E)
∅

(T4 ) (νs T, E)

→ (T, E[false/s]) if s ∈
/ dom(E)

(T5 ) (A(s), E)

→ ([s/x]T, E)

(T6 ) (await s, E)
(T7 ) (thread T, E)
(T8 ) (C[∆], E)

∅

if A(x) = T

∅

→ (0, E)

if E(s) = true

{|T |}

→ (0, E)
P
→ (C[T ′ ], E ′ )

P

if (∆, E) → (T ′ , E ′ )

We write (T, E) ↓ if T cannot be reduced in the environment E according to the rules above.
We also say that (T, E) is suspended. An inspection of the rules reveals that (T, E) ↓ if
and only if T = 0 or T = C[(await s)] with E(s) = false. Thus the await statement is the
only one that may cause the suspension of a thread. The suspension predicate is extended
to programs as follows (P, E) ↓ if ∀ T ∈ P (T, E) ↓.

2.4

Program reduction

To execute a program P in an environment E during an instant proceed as follows:
(1) Schedule (non-deterministically) the executions of the threads that compose it as long
as some progress is possible according to the rule:
(P ∪ {|T |}, E) → (P ∪ {|T ′ |} ∪ P ′′ , E ′ )
P ′′

if

P ′′

(T, E) → (T ′ , E ′ ) .
P ′′

We also write (P ∪ {|T |}, E) → (P ∪ {|T ′ |}, E ′ ) if (T, E) → (T ′ , E ′ ).
(2) Transform all (watch s T ) instructions where the signal s is present into the terminated
thread 0. Formally, we rely on the function ⌊ ⌋E defined on a multiset of suspended threads
as follows:
⌊P ⌋E = {|⌊T ⌋E | T ∈ P |} ⌊0⌋E = 0 ⌊T ; T ′ ⌋E = ⌊T ⌋E ; T ′ ⌊await s⌋E = (await s)

0
if E(s) = true
⌊watch s T ⌋E =
(watch s ⌊T ⌋E ) otherwise
4

2.5

Trace semantics
I/O

Finally, the input-output behaviour of a program is described by labelled transitions P →
P ′ where I ⊆ Input and O ⊆ Output are the signals in the interface which are present in
input at the beginning of the instant and in output at the end of the instant, respectively.
As in Mealy machines, the transition means that from program (state) P with ‘input’
signals I we move to program (state) P ′ with ‘output’ signals O. This is formalised by the
rule:
∗

(I/O)

(P, EI,P ) → (P ′ , E ′ ),

(P ′, E ′ ) ↓,

O = {s ∈ Output | E ′ (s) = true}

I/O

P → P′

if s ∈ I
 true
false
if s ∈ (Int ∪ sig(P ))\I
where: EI,P (s) =

undefined otherwise

Note that in the definition of EI,P we insist on having all signals free in the program in the
domain of definition of the environment and we leave the others undefined so that they
can be potentially used in the rule (T4 ). A complete run of a program P is a reduction
I1 /O1

I2 /O2

P → P1 → P2 · · · which is either infinite or is finite and cannot be further extended.
We define an extensional semantics of a program P , as the set tr (P ) of (finite or infinite)
words associated with its complete runs. Namely:
I1 /O1

I2 /O2

tr (P ) = {(I1 /O1)(I2 /O2) · · · | Ij ⊆ Input, Oj ⊆ Output , P → P1 → P2 · · · }

2.6

(1)

Derived instructions

We may abbreviate (νs1 · · · (νsn T ) · · · ) as (νs1 , . . . , sn T ) and (thread T1 ); · · · (thread Tn ) as
(thread T1 , . . . , Tn ). Table 1 presents some derived instructions which are frequently used
in the programming practice. The instruction (loop T ) can be thought as T ; T ; T ; · · · .
Note that in (loop T ); T ′ , T ′ is dead code, i.e., it can never be executed. The instruction
(now T ) runs T for the current instant, i.e., if the execution of T is not completed within
the current instant then it is aborted. The instruction pause suspends the execution of
the thread for the current instant and resumes it in the following one. We will rely on
this instruction to guarantee the termination of the computation of each thread within an
instant (see section 3). The instruction (present s T1 T2 ) branches on the presence of a
signal. Note that the branch T2 corresponding to the absence of the signal is executed in
the following instant and that we suppose s′ ∈
/ sig(T1 ) ∪ sig(T2 ). The instruction (T1 || T2 )
runs in parallel the threads T1 and T2 and waits for their termination. Here we suppose
/ sig(T1 ) ∪ sig(T2 ).
that s1 , s2 , s′1 , s′2 ∈

2.7

Comparison with [8]

The main novelty with respect to [8] is the replacement of loop and parallel composition
operators with recursive definitions and thread spawning. We should stress that the en5

(loop T )
(now T )
pause
(present s T1 T2 )

(T1 || T2 )

= A where: A = T ; A
= νs (emit s); (watch s T ) s ∈
/ sig(T )
= νs (now (await s))
= νs′ (thread
(now (await s); (thread T1 ; (emit s′ ))),
(watch s pause; (thread T2 ; (emit s′ ))) ); (await s′ )
= νs1 , s2 , s′1 , s′2 (thread
(watch s′1 T1 ; (loop (emit s1 ); pause)),
(watch s′2 T2 ; (loop (emit s2 ); pause)) );
(await s1 ); (emit s′1 ); (await s2 ); (emit s′2 )
Table 1: Some derived instructions

coding of the present and parallel composition operators do not correspond exactly to the
operators in the original language. This is because the instructions T1 and T2 are under
a thread instruction and therefore their execution does not depend on watch signals that
may be on top of them. If this must be the case, then we must prefix T1 and T2 with suitable watch instructions. The CPS translation discussed in section 4, provides a systematic
method to simulate the stack of watch signals.

2.8

Cooperative vs. preemptive concurrency

In cooperative concurrency a running thread cannot be interrupted unless it explicitly decides to return the control to the scheduler. This is to be contrasted with preemptive
concurrency where a running thread can be interrupted at any point unless it explicitly requires that a series of actions is atomic (e.g., via a lock). We refer to, e.g., [17]
for an extended comparison of the cooperative and preemptive models in the practice of
programming. In its original proposal, the SL language adopts a cooperative notion of
concurrency. Technically this means that a ‘big step’ reduction is defined on top of the
‘small step’ reduction we have introduced. The big step reduction runs a thread atomically
till it terminates or it suspends on an await statement. Programs are then evaluated according to this big step reduction. In particular, this means that the small step reductions
cannot be freely interleaved. In the following, we will focus on the small step/preemptive
semantics and neglect the big step/cooperative semantics for two reasons: (1) All main
results (determinism, reactivity, CPS translation) are naturally obtained at the level of the
small step/preemptive semantics and are then lifted to the big step/cooperative semantics. (2) The cooperative semantics goes against the natural idea of executing a program
with parallel threads on a multi-processor where the threads run in parallel on different
processors up to a synchronisation point.

6

3

Determinism and reactivity

We consider two important properties a SL program should have: determinism and reactivity. While the first property is ensured by the design of the language (as was the case
in the original language), we enforce the second by means of a new static analysis.

3.1

Determinism

It is immediate to verify that the evaluation of a thread T in an environment E is deterministic. Therefore the only potential source of non-determinism comes from the scheduling of
the threads. The basic remark is that the emission of a signal can never block the execution
of a statement within an instant. The more signals are emitted the more the computation
of a thread can progress within an instant. Of course, this monotonicity property relies on
the fact that a thread cannot detect the absence of a signal before the end of an instant.
Technically, the property that entails determinism is the fact that the small step reduction is strongly confluent up to renaming. A renaming σ is a bijection σ on signal
names which is the identity on the names in the interface Int. We introduce a notion of
equality up to renaming: (i) T =α T ′ if there is a renaming σ such that σT = T ′ and (ii)
(T, E) =α (T ′ , E ′ ) if there is a renaming σ such that σT = T ′ and E = E ′ ◦ σ. In a similar
way, we define P =α P ′ and (P, E) =α (P ′ , E ′ ). We rely on equality up to renaming to
define a notion of determinism.
Definition 2 The set of deterministic programs is the largest set of programs D such that
I/O1

I/O2

if P ∈ D, I ⊆ Input, P → P1 , and P → P2 then O1 = O2 and P1 =α P2 ∈ D.
In appendix A.2, we show how to derive determinism from strong confluence by means
of a standard tiling argument.
Theorem 3 All programs are deterministic.

3.2

Reactivity

We now turn to a formal definition of reactivity.
Definition 4 The set of reactive programs is the largest set of programs R such that if
P ∈ R then for every choice I ⊆ Input of the input signals there are O, P ′ such that
I/O

P → P ′ and P ′ ∈ R.
We can write programs which are not reactive. For instance, the thread A = (await s); A
may potentially loop within an instant. Whenever a thread loops within an instant the
computation of the whole program is blocked as the instant never terminates. In the programming practice, reactivity is ensured by instrumenting the code with pause statements
that force the computation to suspend for the current instant. Following this practice,
7

we take the pause statement as a primitive, though it can can be defined as seen in section 2.6. This can be easily done by observing that a suspended thread may also have the
shape C[pause] and by extending the evaluation at the end of the instant with the equation
⌊pause⌋E = 0. We introduce next a static analysis that guarantees reactivity on a code
with explicit pause statements.
We denote with X, Y, . . . finite multisets of thread identifiers and with ℓ a label ranging
over the symbols 0 and ↓. We define a function Call associating with a thread T a pair
(X, ℓ) where intuitively the multi-set X represents the thread identifiers that T may call
within the current instant and ℓ indicates whether a continuation of T has the possibility
of running within the current instant (ℓ = 0) or not (ℓ =↓). As usual, πi projects a tuple
on the ith component.
Call (0) = Call (emit s) = Call (await s) = (∅, 0)

Call (pause) = (∅, ↓)

Call (νs T ) = Call(watch s T ) = Call (T )

Call (A(s)) = ({|A|}, 0)

Call(thread T ) = (π1 (Call (T )), 0)

Call(T1 ; T2 ) = Call (T1 ); Call(T2 )

where the operation ‘;’ is defined on the codomain of Call as follows:
(Y, 0)
(Y, ↓)
;
(X, 0) (X ∪ Y, 0) (X ∪ Y, ↓)
(X, ↓)
(X, ↓)
(X, ↓)
We notice that this operation is associative. It is convenient to define the Call function
also on evaluation contexts as follows:
Call ([ ]) = ∅
Call ([ ]; T ) = Call (T )
Call (watch s C) = Call(C) Call ((watch s C); T ′) = Call (C); Call(T ′ )
and observe the following property which is proved by induction on the structure of the
context.
Proposition 5 For every evaluation context C and thread T , Call(C[T ]) = Call (T ); Call(C).
We can now introduce a static condition that guarantees reactivity. Intuitively, to
ensure the reactivity of a program P , it is enough to find an acyclic precedence relation on
the related thread identifiers which is consistent with their definitions. Namely, we define:
Cnst(P ) = {A > B | A(x) = T equation for program P, B ∈ π1 (Call(T ))}
Theorem 6 A program P is reactive if there is a well founded order > on thread identifiers
that satisfies the inequalities in Cnst(P ).
Proof. The order > on thread identifiers induces a well founded order on the finite multisets of thread identifiers. We denote this order with >m,Id . We define a size function sz
from threads to natural number N as follows:
sz (0) = sz (pause) = 0, sz (emit s) = sz (await s) = sz (A(s)) = 1,
sz (νs T ) = sz (watch s T ) = sz (thread T ) = 1 + sz (T ), sz (T1 ; T2 ) = 1 + sz (T1 ) + sz (T2 )
8

We denote with >lex the lexicographic order from left to right induced by the order >m,Id
and the standard order on natural numbers. This order is well-founded. Finally, we
consider the multi-set order >m induced by >lex on finite multi-sets. Again, this order is
well founded. Next, we define a ‘measure’ µ associating with a program a finite multi-set:
µ(P ) = {|(π1 (Call(T )), sz (T )) | T ∈ P |} .
It just remains to check that the small step reduction decreases this measure. Namely, if
P ′′
(P, E) → (P ′ , E ′ ) then µ(P ) >m µ(P ′) ∪ µ(P ′′ ), where the ∪ is of course intended on multisets. We recall that in the multi-set order an element can be replaced by a finite multi-set
of strictly smaller elements. We proceed by case analysis on the small step reduction.
• Suppose the program reduction is induced by the thread reduction:
∅

(C[∆], E) → (C[T ], E) .
where ∆ has the shape 0; T ′ , emit s, νs T ′ , await s, or watch s 0. In these cases the first
component does not increase while the size decreases.
• Suppose the program reduction is induced by the thread reduction:
{|T |}

(C[(thread T )], E) → (C[0], E) .
Assume Call (T ) = (X, ℓ) and Call (C) = (Y, ℓ′ ). By proposition 5, we have:
Call (C[thread T ]) = Call(thread T ); Call(C) = (X, 0); (Y, ℓ′ ) = (X ∪ Y, ℓ′ )
Call (C[0]) = Call(0); Call(C) = (Y, ℓ′ ) .
Thus the first component does not increase while the size decreases.
• Finally, suppose the program reduction comes from the unfolding of a recursive definition
A(x) = T :
∅
C[A(s)] → C[[s/x]T ] .
Assume Call (T ) = (X, ℓ) and Call (C) = (Y, ℓ′ ). Then
Call(C[A(s)]) = ({|A|} ∪ Y, ℓ),

Call (C[T ]) = Call(T ); Call(C) = (X, ℓ); (Y, ℓ′ ) .

By hypothesis, {|A|} > X. We derive that {|A|} ∪ Y >m,Id X ∪ Y ≥m,Id Y , and we notice
that (X, ℓ); (Y, ℓ′ ) equals (X ∪ Y, ℓ′ ) if ℓ = 0 and (X, ↓), otherwise.
✷
Theorem 6 provides a sufficient (but not necessary) criteria to ensure reactivity.
Example 7 Theorem 6 provides a sufficient (but not necessary) criteria to ensure reactivity. Indeed, the precision of the analysis can be improved by unfolding some recursive
equations. For instance, consider the thread A defined by the system:
A = (watch s1 B); (emit s4 ); A
B = (await s2 ); (emit s3 ); pause; B
9

If we compute the corresponding Call we obtain:
Call ((watch s1 B); (emit s4 ); A)
= ({|B|}, 0); (∅, 0); ({|A|}, 0)
= ({|A, B|}, 0)
Call ((await s2 ); (emit s3 ); pause; B) = (∅, 0); (∅, 0); (∅, ↓); ({|B|}, 0) = (∅, ↓)
and obviously we cannot find a well founded order such that A > A. However, if we unfold
B definition in A then we obtain (∅, ↓); (∅, 0); ({|A|}, 0) = (∅, ↓), and the constraints are
trivially satisfied.

4

A tail-recursive model and a CPS translation

We introduce a more basic language of tail recursive threads to which the ‘high level language’ introduced in section 2 can be compiled via a continuation passing style (CPS)
translation. Tail recursive threads are denoted by t, t′ , . . . and they are defined as follows
t ::= 0 | A(s) | emit s.t | νs t | thread t.t | present s t b
where A is a thread identifier with the usual conventions (cf. section 2). Let b, b′ , . . . stand
for branching threads defined as follows.
b ::= t | ite s b b
Branching threads can only occur in the ‘else’ branch of a present instruction and they are
executed only at the end of an instant once the presence or absence of a signal has been
established. The small step thread reduction can be simply defined as follows:
∅

(t1 ) (emit s.t, E)

→ (t, E[true/s])

(t2 ) (νs t, E)

→ (t, E[false/s]) if s ∈
/ dom(E)

(t3 ) (A(s), E)

→ ([s/x]t, E)

∅

∅

∅

(t4 ) (present s t b, E) → (t, E)
(t5 ) (thread t′ .t, E)

if A(x) = t
if E(s) = true

{|t′ |}

→ (t, E)

The execution of the branching threads at the end of the instant is defined as follows:
⌊0⌋E = 0 ⌊present s t b⌋E =
 h|b|iE
h|b1 |iE if E(s) = true
h|t|iE = t h|ite s b1 b2 |iE =
h|b2 |iE if E(s) = false
A program is now a finite non-empty multi-set of tail recursive threads and program reduction is defined as in section 2.4. We can define the instructions pause and await in ‘prefix
form’ as follows:
pause.b = νs present s 0 b
await s.t = A, where: A = present s t A,

{s} = sig(t) ∪ {s} .

Determinism is guaranteed by the design of the language while reactivity can be enforced
by a static analysis similar (but simpler) than the one presented in section 3.
10

4.1

CPS translation

We denote with ǫ an empty sequence. The translation [[ ]] described in table 2 has 2
parameters: (1) a thread t which stands for the default continuation and (2) a sequence
τ ≡ (s1 , t1 ) · · · (sn , tn ). If si is the ‘first’ (from left to right) signal which is present then
ti is the continuation. Whenever we cross a watch statement we insert a pair (s, t) in the
sequence τ . Then we can translate the await statement with the present statement provided
that at the end of each instant we check (from left to right) whether there is a pair (s, t)
in τ such that the signal s is present. In this case, the continuation t must be run at the
following instant.
Some later versions of the SL language include a (when s T ) statement whose informal
semantics is to run T (possibly over several instants) when s is present. It is possible
to elaborate the CPS translation to handle this operator. The idea is to introduce as an
additional parameter to the translation, the list of signals that have to be present for the
computation to progress.
In the translation of a thread identifier, say, A(t,τ ) (x, s′ ) = [[T ]](t, τ ) the identifier A(t,τ )
takes as additional parameters the signal names free in (t, τ ). For the sake of readability,
in the following we will simply write A(t,τ )(x) and omit the parameters s′ .
It is important to notice that the translation associates with an equation A(x) = T a
potentially infinite family of equations A(t,τ ) (x) = [[T ]](t, τ ), the index (t, τ ) depending on
the evaluation context. However, whenever the evaluation contexts are ‘bounded’ in the
sense described in the following section 4.2, only a finite number of indices are needed and
the CPS translation preserves the finiteness of the system of recursive equations.
Example 8 We compute the CPS translation of the thread A in example 7 (without unfolding). To keep the translation compact, we will use a slightly optimised CPS translation
of the pause statement that goes as follows:
[[pause]](t, (s1 , t1 ) · · · (sn , tn )) = pause.ite s1 t1 (· · · (ite sn tn t) · · · )
Then the translation can be written as follows:
A(0,ǫ) = B (t1 ,τ1 )
t1
= emit s4 .A(0,ǫ)
τ1
= (s1 , t1 )
B (t1 ,τ1 ) = present s2 t2 (ite s1 t1 B (t1 ,τ1 ) )
t2
= emit s3 .pause.ite s1 t1 B (t1 ,τ1 ) .
The translation is lifted to programs as follows: [[P ]] = {|[[T ]](0, ǫ) | T ∈ P |}. We show
that a program generates exactly the same traces (cf. section 2.5) as its CPS translation.
To this end, it is convenient to extend the CPS translation to evaluation contexts as follows:
[[[ ]]](t, τ )
[[[ ]; T ]](t, τ )
[[watch s C]](t, τ )
[[(watch s C); T ]](t, τ )

= (t, τ )
= ([[T ]](t, τ ), τ )
= [[C]](t, τ · (s, t))
= [[C]]([[T ]](t, τ ), τ · (s, [[T ]](t, τ )))

Then we note the following decomposition property of the CPS translation whose proof is
by induction on the evaluation context.
11

[[0]](t, τ )
[[T1 ; T2 ]](t, τ )

=t
= [[T1 ]]([[T2 ]](t, τ ), τ )

[[emit s]](t, τ )

= emit s.t

[[νs T ]](t, τ )
[[thread T ]](t, τ )

= νs [[T ]](t, τ ), where: s ∈
/ sig(t) ∪ sig(τ )
= thread [[T ]](0, ǫ).t

[[watch s T ]](t, τ ) = [[T ]](t, τ · (s, t))
[[await s]](t, τ )

= present s t b, where: τ = (s1 , t1 ) · · · (sm , tm ),
b ≡ (ite s1 t1 . . . (ite sm tm A) . . .), A = present s t b

[[A(s)]](t, τ )

= A(t,τ ) (s, s′ ),

where: sig(t, τ ) = {s′ }, A(x) = T,
{x} ∩ {s′ } = ∅, A(t,τ ) (x, s′ ) = [[T ]](t, τ ) .

Table 2: A CPS translation
Proposition 9 For all C evaluation context, T thread, t tail recursive thread, τ sequence,
[[C[T ]]](t, τ ) = [[T ]]([[C]](t, τ )) .
Definition 10 We define a relation R between threads in the source and target language:
T R t if either (1) t = [[T ]](0, ǫ) or (2) T = C[await s], t = A, and A = [[T ]](0, ǫ).
The idea is that T R t if t = [[T ]](0, ǫ) up to the unfolding of the recursive definition in
the CPS translation of an await statement. The need for the unfolding arises when checking
the commutation of the CPS translation with the computation at the end of the instant.
Then, we show that the relation R behaves as a kind of weak bisimulation with respect
to reduction and suspension and that it is preserved by the computation at the end of the
instant. This point requires a series of technical lemmas which are presented in appendix
A.3. In turn, these lemmas entail directly the following theorem 11.
Theorem 11 Let P be a program. Then tr (P ) = tr ([[P ]]).

4.2

A static analysis to bound evaluation contexts

The source language allows an unlimited accumulation of evaluation contexts. To avoid
stack overflow at run time, we define a simple control flow analysis that guarantees that
each thread has an evaluation context of bounded size. For instance, have this property: (i) the fragment of the language using loop rather than recursive definitions and (ii)
programs where recursive calls under a watch are guarded by a thread statement such as
A = (watch s pause; (thread A)). On the other hand, fail this property recursive definitions
such as: (i) A = pause; A; B and (ii) A = (watch s pause; A).
Let L = {ǫ, κ} be a set of labels. Intuitively, ǫ indicates an empty evaluation context,
while κ indicates a (potentially) non-empty evaluation context. Sequential composition and
the watch statement increase the size of the evaluation context while the thread statement
12

resets its size to 0. Following this intuition, we define a function Call that associates with
a thread and a label a set of pairs of thread identifiers and labels.
Call (0, ℓ) = Call (await s, ℓ) = Call(emit s, ℓ) = ∅,
Call (thread T, ℓ) = Call (T, ǫ),

Call (A, ℓ) = {(A, ℓ)},

Call(T1 ; T2 , ℓ) = Call (T1 , κ) ∪ Call(T2 , ℓ),

Call (watch s T, ℓ) = Call(T, κ) .
Definition 12 (constraints) We denote with Cnst(P ) the least set of inequality and
equality constraints on thread identifiers such that for any equation A(x) = T in the program P : (1) if (B, κ) ∈ Call (T ) then A > B ∈ Cnst(P ) and (2) if (B, ǫ) ∈ Call (T ) then
A ≥ B ∈ Cnst(P ).
If  is a pre-order we define: (i) x ≃ y if x  y and y  x and (ii) x ≻ y if x  y and
x 6≃ y.
Definition 13 (satisfaction) We say that a pre-order  on thread identifiers satisfies
the constraints Cnst(P ) if: (1) A > B ∈ Cnst(P ) implies A ≻ B, (2) A ≥ B ∈ Cnst(P )
implies A  B, and (3) ≻ is well-founded.
We can now state the correctness of our criteria whose proof is delayed to appendix
A.4. The reader may check the criteria on example 8.
Proposition 14 If there is a pre-order that satisfies Cnst(P ) then the CPS translation
preserves the finiteness of the system of equations.

5

Expressivity

In this section we present two basic results on the computational expressivity of the model.
First, we show that reactive programs without signal generation are trace equivalent to
monotonic deterministic finite state machines, modulo a natural encoding. Second, we
notice that the combination of recursion and signal name generation allows to simulate
the computation of two counter machines. Thus, unlike the original SL language, it is not
always possible to compile our programs to finite state machines.

5.1

Monotonic Mealy machines

A monotonic Mealy machine is a particular Mealy machine whose input and output alphabets are powersets and such that the function that determines the output respects the
inclusion order on powersets. As for programs, we can associate with a monotonic Mealy
machine a set of traces.

13

Definition 15 (monotonic Mealy machine) A finite state, deterministic, reactive, and
monotonic Mealy machine (monotonic Mealy machine for short) is a tuple M = (Q, qo , I, O, fQ,
fO ) where Q is a finite set of states, qo ∈ Q is the initial state, I = 2n , O = 2m for n, m
natural numbers are the input and output alphabets, respectively, fQ : I × Q → Q is the
function computing the next state, and fO : I × Q → O is the function computing the
output which is monotonic in the input, namely X ⊆ Y implies fO (X, q) ⊆ fO (Y, q).
Theorem 16 For every monotonic Mealy machine with input alphabet I = 2n and output
alphabet O = 2m there is a trace equivalent program with n input signals and m output
signals.
Proof. The function fQ ( , q) that for a given state q computes the next state as a function
of the input can be coded as a cascade of ite’s. The function fO ( , q) that for a given state
q computes the output as a function of the input can be coded as the parallel composition
of threads that emit a certain output signal if a certain number of input signals is present
in the instant and do nothing otherwise.
Next we develop some details. Let M = (Q, qo , I, O, fQ, fO ) with I = 2n and O = 2m be
a monotonic Mealy machine. We build the corresponding program. We introduce signals
s1 , . . . , sn for the input and signals s′1 , . . . , s′m for the output. Moreover, we introduce a
thread identifier q for every state q ∈ Q. Given a state q, we associate with the function
fQ ( , q) : 2n → Q a branching thread b(q). For instance, if the function is defined by:
fQ ((1, 1), q) = q1 ,

fQ ((1, 0), q) = q2 ,

fQ ((0, 1), q) = q3 ,

fQ ((0, 0), q) = q1 ,

then the corresponding branching thread is:
b(q) = ite s1 (ite s2 q1 q2 ) (ite s2 q3 q1 )
For every state q, we introduce an equation of the shape:
q = Output(q).pause.b(q)

(2)

where Output(q) is intended to compute the output function fO ( , q) : 2n → 2m . To
formalise this, we need some notation. Let X ⊆ {1, . . . , n} denote an input symbol and
j ∈ {1, . . . , m}. By monotonicity, if X ⊆ Y and j ∈ fO (X, q) then j ∈ fO (Y, q). Given a
family of threads {tj }j∈J , we write threadj∈J tj .t for the thread that spawns, in an arbitrary
order, the threads tj and then runs t. Given a set of input signals {s1 , . . . , sk } and an
output signal s′j , we write await{s1 , . . . , sk }.t for
present s1 (· · · (present sk t 0) · · · ) 0
which executes t in the first instant it is run if and only if all the signals s1 , . . . , sk are
present, and terminates otherwise. No signals are emitted in the instants following the
first one. With these conventions Output(q).t is an abbreviation for
( threadX⊆{1,...,n},

j∈fO (X,q)

(await {sx | x ∈ X}. emit s′j ) ). t
14

so that the explicit form for equation (2) is:
q = ( threadX⊆{1,...,n},

j∈fO (X,q)

(await {sx | x ∈ X}. emit s′j ) ). pause. b(q) .

✷
One may wonder whether our synchronous language may represent non-monotonic
Mealy machines. The answer to this question is negative as long we adopt the encoding of
the input above where 2n input symbols are mapped to n signals. This fact easily follows
from the monotonicity property of the model noted in section 3. However, the answer is
positive if we adopt a less compact representation where n input symbols are mapped to
n signals.
Next we focus on the expressive power of the reactive programs we can write in the
tail recursive calculus presented in section 4 without signal generation but with general
recursion and thread spawning.
Theorem 17 For every reactive tail recursive program with n input signals and m output
signals and without signal generation there is a trace equivalent monotonic Mealy machine
with input alphabet 2n and output alphabet 2m .
Proof. The construction takes several steps but the basic idea is simple: it is useless to
run twice or more times through the same ‘control point’ within the same instant. Instead
we record the set of control points that have been reached along with the signals that have
been emitted and in doing so we are bound to reach a fixed point.
We start with some preliminary considerations that allow to simplify the representation
of programs.
(1) Since there is no signal generation a program depends on a finite set So of signal
names. As a first step we can remove parameters from recursive equations. To this end,
replace every parametric equation A(x) = t with a finite number of equations (without
parameters) of the shape As = [s/x]t for s ranging over tuples of signal names in So .
(2) As a second step, we put the recursive equations in normal form. By introducing
auxiliary thread identifiers, we may assume the equations have the shape A = t where
t ::= 0 | emit s.B | present s B b | thread B.B ′
b ::= A | ite s b b
We denote with Id o the finite set of thread identifiers.
(3) Because there is no signal name generation, we may simply represent the environment
E as a subset of So and because the threads are in normal form we may simply represent a
program P as a multi-set of identifiers in Id o . The small step reduction of the pair (P, E)
is then described as follows:

 (P ∪ {|B|}, E ∪ {s}) if A = emit s.B
(P ∪ {|B|}, E)
if A = present s B b, s ∈ E
(P ∪ {|A|}, E) →

(P ∪ {|B1 , B2 |}, E) if A = thread B1 .B2
15

Notice that in this presentation, the unfolding of recursive definitions is kept implicit. If
the program is reactive we know that the evaluation of a pair (P, E) eventually terminates
in a configuration (P ′ , E ′ ) such that if A ∈ P ′ then either A = 0 or A = present s B b and
s∈
/ E ′ . The evaluation at the end of the instant ⌊P ′ ⌋E ′ is then a particular case of the
one defined in section 4 for tail recursive threads and produces again a multi-set of thread
identifiers.
(4) We now consider an alternative representation of a program as a set q of identifiers in
Id o . We define a small step reduction on configurations (q, E) as follows:

/ q ∪ {A} or s ∈
/ E)
 (q ∪ {A, B}, E ∪ {s}) if A = emit s.B, (B ∈
(q ∪ {A, B}, E)
if A = present s B b, s ∈ E, B ∈
/ q ∪ {A}
(q ∪ {A}, E) →

(q ∪ {A, B1 , B2 }, E) if A = thread B1 .B2 , {B1 , B2 } 6⊆ q ∪ {A}
Note that at each reduction step either the program q or the environment E increase strictly
while the other component does not decrease. Consequently, this reduction process (unlike
the previous one) necessarily terminates. The evaluation at the end of the instant is now
defined as follows:
⌊q⌋E = {A ∈ q | A = 0} ∪ {h|b|iE | A ∈ q, A = present s B b, and s ∈
/ E} .
Notice that q may contain, e.g., a thread identifier A such as A = emit s.B and that A is
removed by the function ⌊ ⌋E .
(5) We now relate the two representations of the programs and the associated evaluation
strategies where if P is a multi-set we let set(P ) = {A | A ∈ P } be the corresponding set
where we forget multiplicities.
Lemma 18 Suppose (P1 , E1 ) → · · · → (Pn , En ) with n ≥ 1 and q = set(P1 ∪ · · · ∪ Pn ).
Then:
(1) If (Pn , En ) → (Pn+1 , En+1 ) then either En = En+1 and set(Pn+1 ) ⊆ q or (q, En ) →
(q ′ , En+1 ) and q ′ = set(P1 ∪ · · · ∪ Pn+1 ).
(2) If (q, En ) → (q ′ , En+1 ) then (Pn , En ) → (Pn+1 , En+1 ) and q ′ = set(P1 ∪ · · · ∪ Pn+1 ).
(3) If (Pn , En ) ↓ then set(⌊Pn ⌋En ) = ⌊q⌋En .
Proof. (1) By case analysis on the small step reduction for multi-sets.
(2) By case analysis on the small step reduction for sets. Note that if the reduction rule
is applied to A ∈ q then necessarily A ∈ Pn . Indeed, if A ∈ Pk and A ∈
/ Pk+1 with k < n
we can conclude that a reduction rule has been applied to A on the multi-set side and this
contradicts the hypotheses for the firing of the rule on the set side.
(3) We check that if A = 0 and A ∈ q then A ∈ Pn and that if A = present s B t, s ∈
/ En
and A ∈ q then A ∈ Pn .
✷
(6) We define
Closure(q, E) = (q ′ , E ′ ) if (q, E) → · · · → (q ′′ , E ′ ) 6→ and q ′ = ⌊q ′′ ⌋E ′
16

The Closure operator is well defined because the reduction relation is strongly confluent
and it always terminates.
(7) As a final step, given a reactive program P in normal form with identifiers Id o , n
input signals s1 , . . . , sn and m output signals s′1 , . . . , s′m , we build a trace equivalent monotonic Mealy machine M = (Q, qo , I, O, fQ, fO ) as follows: Q = 2Id o , qo = set(P ), I = 2n ,
O = 2m , and (fQ (E, q), fO (E, q)) = Closure(q, E).
✷
By combining theorems 16 and 17, we can conclude that the reactive programs we can
write without signal generation are exactly those definable by monotonic Mealy machines
modulo a natural encoding.

5.2

Undecidability

The following result can be used to show that various questions about the behaviours of
programs are undecidable. The encoding idea is similar to the one presented for CCS in
[15]. The details are presented in appendix A.5.
Theorem 19 For any deterministic 2-counter machine there is a reactive program with
signal generation that will eventually emit on a certain signal if and only if the computation
of the 2-counter machine terminates.

6

Program equivalence

The formalisation of the SL model we have considered so far is close to an abstract machine.
Typical symptoms include an ad hoc definition of α-renaming (cf. section 3), a global
notion of environment, and the fact that roughly threads compose but do not reduce while
programs reduce but do not compose. We introduce next an alternative description of the
tail recursive model featuring a uniform notation for threads, programs, and environments.
This alternative description is instrumental to the development of a notion of program
equivalence based on the concept of bisimulation following a CCS style. The theory is
built so that it does not depend on the determinacy of the language. Indeed practical
extensions of the language have been considered where signals carry data values and the
act of receiving a value may introduce non-determinism. A theory of program equivalence
should be sufficiently robust to accommodate these extensions.

6.1

Programs

We extend the syntax of tail recursive threads so that it includes both environments and
programs in a uniform notation.
P ::= 0 | emit s | present s P B | P | P | νs P | A(s)
B ::= P | ite s B B
17

We refrain from introducing syntax like ‘emit s.P and ‘thread P ′.P which can be understood
as syntactic sugar for (emit s) | P and P ′ | P , respectively.

6.2

Actions and labelled transition system

Actions are denoted by α, α′, . . . and they are defined by the grammar: α ::= τ | s | s. We
write s ∈ α if α = s or α = s. We define a labelled transition system which is similar to
the one for CCS except for a different treatment of emission which is persistent within an
instant. Technically, (i) an emission behaves as a replicated output (rule (out)) and (ii)
in the continuation of a present statement the tested signal is still emitted (rule (in)); this
guarantees that the continuation can only evolve in an environment where the signal s is
emitted.1
(out)
(τ )
(ν)

s

emit s → emit s
s
s
P1 → P1′ P2 → P2′
τ
P1 | P2 → P1′ | P2′
α
P → P′ s ∈
/α
α
νs P → νs P ′

(in)
(par )
(rec)

s

present s P B → P | (emit s)
α
P1 → P1′
α
P1 | P2 → P1′ | P2
A(x) = P
τ
A(s) → [s/x]P

As usual, we omit the symmetric rules for (par , τ ). We note the following properties of the
labelled transition system where = stands for syntactic identity up to renaming of bound
names.
s

Proposition 20 (1) If P → P ′ then P = P ′ .
s

α

s

(2) If P → P and P → P ′ then P ′ → P ′ .
s

s

(3) If P → P ′ then P ′ → P ′ .

6.3

End of the instant

We define the computation at the end of the instant while relying on the following notation:
α
α
τ
P → · for ∃ P ′ P → P ′ and P ↓ for ¬(P → ·). Suppose P ↓ and all bound signal names
in P are renamed so as to be distinct and different from the free signal names. First, we
compute the set of emitted signals S = Em(P ) as follows:
Em(emit s) = {s},

Em(0) = Em(present s P B) = ∅,

Em(P1 | P2 ) = Em(P1 ) ∪ Em(P2 ),
1

Em(νs P ) = Em(P ) .

This is close in spirit, if not in the technical development, to Prasad’s Calculus of Broadcasting Systems
[18]; see also [10].

18

Second, we compute ⌊P ⌋ = ⌊P ⌋Em(P ) where we remove all emitted signals and compute
the B branches relying on the auxiliary functions ⌊ ⌋S and h| |iS defined as follows:
⌊emit s⌋S = ⌊0⌋S = 0,

⌊present s P B⌋S = h|B|iS ,

⌊νs P ⌋S = νs ⌊P ⌋S ,

⌊P1 | P2 ⌋S = ⌊P1 ⌋S | ⌊P2 ⌋S ,

h|B1 |iS if s ∈ S
h|ite s B1 B2 |iS =
h|B2 |iS if s ∈
/S.

h|P |iS = P,

One can verify that the function ⌊ ⌋ is invariant under α-renaming: if P1 = P2 then
⌊P1 ⌋ = ⌊P2 ⌋.

6.4

Barbed and contextual bisimulations
τ

τ

α

τ

α

τ

As usual, we write P ⇒ P ′ for P (→)∗ P ′ and P ⇒ P ′ with α 6= τ for P (⇒)(→)(⇒)P ′ .
Definition 21 We define:
τ

P ⇓ if ∃ P ′ P ⇒ P ′ and P ′ ↓
(weak suspension)
α1
αn
P ⇓L if P → P1 · · · → Pn , n ≥ 0, and Pn ↓ (L-suspension)
Obviously P ↓ implies P ⇓ which in turn implies P ⇓L . The L-suspension predicate (L
for labelled) plays an important role in the following definitions of bisimulation.
Definition 22 A (static) context C is defined by C ::= [ ] | C | P | νs C.
Proposition 23 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 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 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 . We may assume
α1 is not an emission action for otherwise we can build a shorter sequence of transitions.
τ
(α1 = τ ) Then we take Q = Q1 and (P0 | Q1 ) → (P1 | Q1 ).
s

τ

(α1 = s) Let Q = (Q1 | s). We have (P0 | Q) → (P1 | Q1 | s). Since P1 → P1 , we observe
that (P1 | Q1 ) ⇓ implies (P1 | Q1 | s) ⇓.
(2 ⇒ 3) Take C = [ ] | Q.
τ

τ

(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
19

induction on n that P ⇓L . Proceed by case analysis on the context C and the action α1 .
✷
Interestingly, the second characterisation, shows that the L-suspension predicate can
be defined just in terms of the τ transitions and the suspension predicate. This means that
the following definitions of barbed and contextual bisimulation can be given independently
of the labelled transition system.
Definition 24 (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 ↓ then ∃ Q′ Q ⇒ Q′ , Q′ ↓, P R Q′ , and ⌊P ⌋ R ⌊Q′ ⌋.
s

τ

s

(B3) If P → · and P ⇓L then ∃ Q′ Q ⇒ Q′ , Q′ → ·, and P R Q′ .
We denote with ≈B the largest barbed bisimulation.
It is easily checked that ≈B is reflexive and transitive. A reasonable notion of program
equivalence should be preserved by the static contexts. We define accordingly a notion of
contextual bisimulation.2
Definition 25 (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 context C.
We denote with ≈C the largest contextual bisimulation.
Again it is easily checked that ≈C is reflexive and transitive. By its very definition, it
follows that P ≈C Q implies C[P ] ≈C C[Q] and P ≈B Q.

6.5

Labelled bisimulation

Aiming at a more effective description of the notion of contextual bisimulation, we introduce
a notion of labelled bisimulation.
Definition 26 (labelled bisimulation) A symmetric relation R on programs is a labelled bisimulation if it is a barbed bisimulation (conditions B1-3) and moreover whenever
P R Q the following holds:
τ
(L1) If P ′ = (P | S) ↓ with S = emit s1 | · · · | emit sn , n ≥ 0 then ∃ Q′ (Q | S) ⇒
Q′ , Q′ ↓, P ′ R Q′ , and ⌊P ′ ⌋ R ⌊Q′ ⌋.
s
s
τ
(L2) If P → P ′ then either ∃ Q′ ( Q ⇒ Q′ and P ′ R Q′ ) or ∃ Q′ ( Q ⇒ Q′ and P ′ R (Q′ |
emit s) ).
We denote with ≈L the largest labelled bisimulation.
2

Here we adopt the notion of contextual equivalence introduced by [11] for the π-calculus. An alternative
approach is to consider a notion of barbed equivalence [16]. We refer to [9] for a comparison of the two
methods.

20

Remark 27 (1) Condition (L1) strengthens (B2) therefore in the following proof the
analysis of (B2) is subsumed by the one of (L1). To see the necessity of condition (L1),
consider
P = present s1 0 (ite s2 (emit s3 ) 0)

and

Q = present s2 0 0 .

Then P ↓, Q ↓, and ⌊P ⌋ = ⌊Q⌋ = 0 so that conditions (B1 − 3) and (L2) are satisfied.
However, if we plug P and Q in the context [ ] | (emit s2 ) then the resulting programs exhibit
different behaviours. It is not difficult to show that condition (L1) can be optimised so that
we only consider emissions on signals which are free in the programs under consideration.
For instance, a simple corollary of this optimisation is that labelled bisimulation is decidable
for programs without recursive definitions.
(2) Condition (L2) has already appeared in the literature in the context of the asynchronous
π-calculus [2].
(3) There is no condition for the emission because by proposition 20 condition (B3) is
s
s
equivalent to the following one: if P → P ′ and P ′ ⇓L then ∃ Q′ ( Q ⇒ Q′ and P ′ R Q′ ).
(4) The condition P ⇓L in (B3) is always satisfied by reactive programs which are those
we are really interested in. We will see in section 6.9, that thanks to strong confluence,
the condition P ⇓L can be replaced by the condition P ⇓ or equivalently by the condition
P ↓. However, one should keep in mind that there are non-deterministic extensions of
the language where this identification fails and where moreover the definitions based on
the weaker conditions P ↓ or P ⇓ lead to notions of labelled bisimulation which are not
preserved by parallel composition. For this reason, our definitions of bisimulation are based
on the L-suspension predicate.
We can now state the main result of this section.
Theorem 28 P ≈C Q iff P ≈L Q.
We outline the proof argument which is developed in the following. First, we note
that labelled bisimulation equates all programs which cannot L-suspend and moreover it
never equates a program which L-suspends to one which cannot. Second, we introduce
a notion of strong labelled bisimulation which is contained in labelled bisimulation. It is
shown that strong labelled bisimulation satisfies some useful laws like associativity, commutativity, commutation of signal name generation, . . . Third, we develop a notion of
labelled bisimulation up to strong labelled bisimulation that considerably simplifies reasoning about labelled bisimulation. Fourth, we show that ≈C is a labelled bisimulation up
to strong labelled bisimulation so that P ≈C Q implies P ≈L Q. Fifth, we show that labelled bisimulation is preserved by parallel composition with signal emission, it is reflexive
and transitive, and it is preserved by signal name generation, parallel composition, and the
present operator. In particular, it follows that ≈L is preserved by the static contexts, i.e.,
≈L is a contextual barbed bisimulation and therefore P ≈L Q implies P ≈C Q.
21

6.6

Labelled bisimulation and L-suspension

We observe some remarkable properties of the L-suspension predicate.
Proposition 29 (1) If ¬P ⇓L and ¬Q ⇓L then P ≈L Q.
(2) If P ≈L Q and P ⇓L then Q ⇓L .
Proof. First we note the following properties:
(A) By proposition 23, if (P | Q) ⇓L then P ⇓L .
α
(B) By definition, if ¬P ⇓L and P → P ′ then ¬P ′ ⇓L .
(1) We show that {(P, Q) | ¬P ⇓L and ¬Q ⇓L } is a labelled bisimulation.
τ
(B1) By (B), if ¬P ⇓L and P → P ′ then ¬P ′ ⇓L .
(B3) The hypothesis is not satisfied.
(L1) By (A), if ¬P ⇓L then ¬(P | S) ⇓L . Hence ¬(P | S) ↓.
s
(L2) By (B), if ¬P ⇓L and P → P ′ then ¬P ′ ⇓L . Then we match the transition with
τ
Q ⇒ Q and by (A) ¬Q ⇓L implies ¬(Q | (emit s)) ⇓L .
α

α

(2) We proceed by induction on the shortest reduction such that P →1 P1 · · · →n Pn and
Pn ↓. Note that in such a reduction no emission action s occurs (otherwise a shortest
τ
reduction can be found). If n = 0 then (B2) requires Q ⇒ Q′ and Q′ ↓. Hence Q ⇓L .
τ
If n > 0 then we consider the first action α1 . If α1 = τ then (B1) requires Q ⇒ Q1 and
P1 ≈L Q1 . Then Q1 ⇓L by inductive hypothesis on P1 . Hence Q ⇓L . If α1 = s then we have
s
to consider two cases. If Q ⇒ Q1 and P1 ≈L Q1 then Q1 ⇓L by inductive hypothesis on P1 .
τ
Hence Q ⇓L . If on the other hand Q ⇒ Q1 and P1 ≈L Q1 | (emit s) then Q1 | (emit s) ⇓L .
Hence by (A) Q1 ⇓L , and Q ⇓L .
✷

6.7

Strong labelled bisimulation and an up-to technique

To bootstrap reasoning about labelled bisimulation, it is convenient to introduce a much
stronger notion of labelled bisimulation.
Definition 30 (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 ′ implies ∃ Q′ Q → Q′ and P ′ R Q′ .
(S2) (P | S) ↓ with S = (emit s1 ) | · · · | (emit sn ), n ≥ 0 implies (P | S) R (Q | S) and
⌊P | S⌋ R ⌊Q | S⌋.3
We denote with ≡L the largest strong labelled bisimulation.
3

The condition (Q | S) ↓ follows by (S1).

22

Note that in definition 30 not only we forbid weak internal moves but we also drop the
convergence condition in (B3) and the possibility of matching an input with an internal
transition in (L2). For this reason, we adopt the notation ≡L rather than the usual ∼L .
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 ).
Strong labelled bisimulation enjoys some useful properties whose standard proof is delayed
to appendix A.7
Lemma 31 (1) ≡L is a reflexive and transitive relation.
(2) If P ≡L Q then P ≈L Q.
(3) The following laws hold:
P | 0 ≡L P,
P1 | (P2 | P3 ) ≡L (P1 | P2 ) | P3 ,
P1 | P2 ≡L P2 | P1 , νs P1 | P2 ≡L νs (P1 | P2 ) if s ∈
/ sig(P2 ).
(4) If P ≡L Q then P | S ≡L Q | S where S = P1 | · · · | Pn and Pi = 0 or Pi = (emit si ),
for i = 1, . . . , n, n ≥ 0.
(5) If R is a strong labelled bisimulation up to strong labelled bisimulation then (≡L
) ◦ R ◦ (≡L ) is a strong labelled bisimulation.
s

(6) If P → · then P ≡L P | (emit s).
(7) If P1 ≡L P2 , then νs P1 ≡L νs P2 and P1 | Q ≡L P2 | Q.
We use strong labelled bisimulation in the context of a rather standard ‘up to technique’.
Definition 32 A relation R is a labelled bisimulation up to ≡L if the conditions (B1 − 3)
and (L1 − 2) are satisfied when replacing the relation R with the (larger) relation (≡L
) ◦ R ◦ (≡L ).
Lemma 33 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 the congruence properties of ≡L .
(2) Follows directly from (1).

6.8

✷

Characterisation

As a first application of the ‘up to technique’, we show that P ≈C Q implies P ≈L Q.
Lemma 34 ≈C is a labelled bisimulation up to ≡L .

23

Proof. Suppose P ≈C Q. We check conditions (L1 − 2).
(L1) Suppose S = (emit s1 ) | · · · | (emit sn ) and (P | S) ↓. Since ≈C is preserved by
parallel composition we derive P | S ≈C Q | S. Then we conclude by applying condition
(B2).
s

(L2) Suppose P → P ′ . By lemma 31(6), this implies P ′ ≡L P ′ | (emit s). Since ≈C
is preserved by parallel composition we know P | (emit s) ≈C Q | (emit s). From this
τ
and the fact that P | (emit s) → P ′ | (emit s) condition (B1) allows to derive that
τ
Q | (emit s) ⇒ Q′ | (emit s) and P ′ | (emit s) ≈C Q′ | (emit s). Two cases may arise: (1)
s
τ
Q ⇒ Q′ . Then we have P ′ ≡L P ′ | (emit s) ≈C Q′ | (emit s) ≡L Q′ . (2) Q ⇒ Q′ . Then we
have P ′ ≡L P ′ | (emit s) ≈C Q′ | (emit s). In both cases we close the diagram up to ≡L . ✷
As a second application of the ‘up to technique’ we prove some desirable congruence
properties of the labelled bisimulation (the proofs are delayed to appendix A.8). Assume
pause.B abbreviates νs present s 0 B for s ∈
/ sig(B). We write B1 ≈L B2 if pause.B1 ≈L
pause.B2 .
Lemma 35 (1) If P ≈L Q then P | (emit s) ≈L Q | (emit s).
(2) The relation ≈L is reflexive and transitive.
(3) If P ≈L Q then νs P ≈L νs Q.
(4) If P1 ≈L P2 then P1 | Q ≈L P2 | Q.
(5) If P ≈L P ′ and B ≈L B ′ then present s P B ≈L present s P ′ B ′ .
The lemma above entails that ≈L is preserved by static contexts. Hence P ≈L Q
implies P ≈C Q. This remark combined with lemma 34 concludes the proof of theorem
28.

6.9

Exploiting confluence

We can easily adapt the trace semantics presented in section 2.5 to the present context. If
P is a program we write (Π for the parallel composition):
I/O

τ

P → P ′ if P | PI ⇒ P ′′ , with PI = Πs∈I s,

P ′′ ↓,

s

O = {s | P ′′ → ·}, and P ′ = ⌊P ′′ ⌋ .

and we associate with P a set of traces tr (P ) as in section 2.5. A general argument shows
that labelled bisimulation is a refinement of trace equivalence.
Proposition 36 If P ≈L Q then tr (P ) = tr (Q).
I/O

I/O

Proof. We observe that if P ≈L Q and P → P ′ then Q → Q′ and P ′ ≈L Q′ . From this
one can show that every trace in tr (P ) is in tr (Q) and conversely.
I/O

s

τ

We recall that P → P ′ means P | PI ⇒ P ′′ , with PI = Πs∈I s, P ′′ ↓, O = {s | P ′′ → ·},
τ
and P ′ = ⌊P ′′ ⌋. First, note that P ≈L Q implies P | PI ≈L Q | PI . If (P | PI ) ⇒ P ′′
24

τ

τ

and P ′′ ↓ then by (B1) Q | PI ⇒ Q1 and P ′′ ≈L Q1 . Moreover, by (B2), Q1 ⇒ Q′′ , Q′′ ↓,
s
s
P ′′ ≈L Q′′ , and P ′ = ⌊P ′′ ⌋ ≈L ⌊Q′′ ⌋ = Q′ . By (B3), if P ′′ → · then Q′′ → ·, and conversely.
I/O

Thus Q → Q′ .

✷

Next, we recast the strong confluence result mentioned in section 3 in the following
terms.
α

α

α

α

Proposition 37 If P →1 P1 and P →2 P2 then either P1 = P2 or ∃ P12 (P1 →2 P12 and P2 →1
P12 ).
We now look at some additional properties that can be derived from the strong confluence proposition 37.
τ

s

s

s

τ

Lemma 38 (1) If P → P1 , P → P2 , and ¬P → · then ∃ P12 P1 → P12 and P2 → P12 .
s

s

τ

(2) If P → P ′ and P → · then P → P ′ .
τ
τ
(3) If P → P1 , P → P2 and P1 ↓ then P1 = P2 .
τ
τ
(4) If P ⇒ P1 , P ⇒ P2 , P1 ↓, and P2 ↓ then P1 = P2 .
I/O1

I/O2

(5) If P → P1 and P → P2 then P1 = P2 and O1 = O2 .
τ

τ

Proof. We just check (5). By (4), if P | PI ⇒ P1′ , P1′ ↓, P | PI ⇒ P2′ , and P2′ ↓ then
P1′ = P2′ . This forces P1 = ⌊P1′ ⌋ = ⌊P2′ ⌋ = P2 and O1 = O2 .
✷
The following proposition states an interesting consequence of confluence.4
Proposition 39 P ⇓L if and only if P ⇓.
Proof. By definition, P ⇓ implies P ⇓L . To show the other direction, suppose P ⇓L and
α
α
let P →1 P1 · · · →n Pn be a sequence of transitions of minimal length leading to a program
Pn such that Pn ↓. We build a sequence of internal transitions τ leading to a suspended
program. First, we notice that the actions αi cannot be emission actions, otherwise a
shorter sequence can be found. Second, we can assume that the last action αn is an
s
τ
internal transition τ . Otherwise, if αn = s then either Pn−1 → · and then Pn−1 → Pn by
s
lemma 38(1) or ¬Pn−1 → · and then Pn−1 ↓ contradicting the minimal length hypothesis.
Let us now look at a sequence of transitions:
s

τ

τ

P → P1 → · · · → Pn
s

n≥2.

(3)

τ

where ¬P → · and ¬P ↓. Then we must have P → P ′ and by lemma 38(1) there is a P1′
s
τ
τ
such that P ′ → P1′ and P1 → P1′ . By the confluence properties and lemma 38(3), P1′ ⇒ Pn
in n − 2 transitions τ . Thus we have the following sequence of transitions:
τ

s

τ

P → P ′ → P1′ ⇒ Pn
4

One can conceive non-deterministic extensions of the language where the proposition fails.

25

(4)

The number of τ transitions that follow the s transition is n − 1 in (3) and n − 2 in (4).
By iterating this reasoning, the input transition s is eventually removed. Moreover, the
argument is extended to a sequence of transitions containing several input actions by simply removing the input actions one after the other proceeding backwards.
✷
In view of proposition 39, the hypothesis P ⇓L can be replaced by the hypothesis P ⇓
in condition (B3). Now consider an alternative definition where the hypothesis P ⇓L is
replaced by the hypothesis P ↓. We refer to this condition as (B3)↓ , call the resulting notion
of bisimulation ↓-labelled bisimulation, and denote with ≈↓L the related largest bisimulation.
Proposition 40 ≈L =≈↓L .
This is a direct consequence of the following lemma whose proof is delayed to appendix
A.9.
Lemma 41 (1) If P ≈L Q then P ≈↓L Q.
(2) The relation ≈↓L is reflexive and transitive.
τ

(3) If P → Q then P ≈L Q, P ≈↓L Q, and tr (P ) = tr (Q).
(4) ≈↓L is a labelled bisimulation.
We rely on this characterisation to show that bisimulation and trace equivalence collapse; an expected property of deterministic systems. To this end, we note the following
properties of trace equivalence whose proof is given in appendix A.10
Lemma 42 (1) If tr (P ) = tr (Q) then tr (P | (emit s)) = tr (Q | (emit s)).
(2) R = {(P, Q) | tr (P ) = tr (Q)} is a labelled bisimulation.
From proposition 36 and lemma 42(2), we derive the collapse of trace and bisimulation
equivalence.
Theorem 43 P ≈L Q if and only if tr (P ) = tr (Q).

7

Conclusion

Motivated by recent developments in reactive programming, we have introduced a revised
definition of the SL model including thread spawning and recursive definitions. The revised
model is still confluent and therefore deterministic. We have proposed a simple static
analysis that entails reactivity in the presence of recursive definitions and characterised
the computational power of the model with and without signal generation. Moreover, we
have identified a tail recursive core language which is built around the present operator and
whose justification comes directly from the basic design principle of the SL model. The
simplification of the model has been instrumental to the development of a compositional
notion of program equivalence. In further investigations, we plan to extend this approach
to a Synchronous Language including data values and name mobility.
26

Acknowledgements
The author is indebted to G. Boudol, F. Boussinot, I. Castellani, and F. Dabrowski for a
number of discussions on the topic of this paper and for suggesting improvements in its
presentation.

References
[1] 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, Bertinoro, NS-05-3 BRICS
Notes Series, August 2005.
[2] R. Amadio, I. Castellani and D. Sangiorgi. On bisimulations for the asynchronous π-calculus. In
Theor. Comput. Sci., 195:291-324, 1998.
[3] R. Amadio, S. Dal-Zilio. Resource control for synchronous cooperative threads. In Proc. CONCUR,
Springer LNCS 3170, 2004.
[4] R. Amadio, F. Dabrowski. Feasible reactivity for synchronous cooperative threads. In Proc. EXPRESS, ENTCS, 2005 (to appear).
[5] G. Berry and G. Gonthier, The Esterel synchronous programming language. Science of computer
programming, 19(2):87–152, 1992.
[6] G. Boudol, ULM, a core programming model for global computing. In Proc. of ESOP, Springer LNCS
2986, 2004.
[7] F. Boussinot. Reactive C: An extension of C to program reactive systems. Software Practice and
Experience, 21(4):401–428, 1991.
[8] F. Boussinot and R. De Simone, The SL Synchronous Language. IEEE Trans. on Software Engineering, 22(4):256–266, 1996.
[9] C. Fournet and G. Gonthier. A hierarchy of equivalences for asynchronous calculi (extended abstract)
In Proc. ICALP, Springer LNCS 1443, 1998.
[10] M. Hennessy and J. Rathke. Bisimulations for a calculus of broadcasting systems. In Theor. Comput.
Sci., 200(1-2):225-260, 1998.
[11] K. Honda and N. Yoshida. On reduction-based process semantics. In Theor. Comput. Sci., 151(2):
437-486, 1995.
[12] G. Kahn. The semantics of a simple language for parallel programming. In Proc. IFIP Congress,
North-Holland, 1974.
[13] L. Mandel and M. Pouzet. ReactiveML, a reactive extension to ML. In Proc. ACM Principles and
Practice of Declarative Programming, 2005.
[14] A. Matos, G. Boudol and I. Castellani. Typing non-inteference for reactive programs. RR-INRIA 5594,
June 2005. Extended abstract presented at the Foundations of Computer Security 2004 workshop.
[15] R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
[16] R. Milner and D. Sangiorgi. Barbed bisimulation. In Proc. ICALP, Springer LNCS 623, 1992.
[17] J. Ousterhout. Why threads are a bad idea (for most purposes). Invited talk at the USENIX Technical
Conference, 1996.

27

[18] K.V.S. Prasad. A calculus of broadcasting systems. In Sci. Comput. Program., 25(2-3): 285-327,
1995.
[19] Reactive Programming, INRIA, Mimosa Project. http://www-sop.inria.fr/mimosa/rp.
[20] M. Serrano, F. Boussinot, and B. Serpette. Scheme fair threads. In Proc. ACM Principles and practice
of declarative programming, 2004.

28

A

Proofs

A.1

Proof of proposition 1

By induction on the structure of T assuming ‘;′ associates to the right. If T = 0 then
clearly no decomposition is possible. If T 6= 0 is a redex then take C = [ ] and observe
that no other context is possible. If T has the shape ∆; T ′ then take C = [ ]; T ′. If T
has the shape (watch s T ′ ) and T ′ 6= 0 then by inductive hypothesis we have a unique
decomposition T ′ = C ′ [∆′ ] and the only possible decomposition for T is obtained by
taking C = (watch s C ′ ) and ∆ = ∆′ . Finally, if T = (watch s T ′ ); T ′′ and T ′ 6= 0 then by
inductive hypothesis we have a unique decomposition T ′ = C ′ [∆′ ] and the only possible
decomposition for T is obtained by taking C = (watch s C ′ ); T ′′ and ∆ = ∆′ .
✷

A.2

Proof of theorem 3

First we notice that the notion of reduction, suspension, and evaluation at the end of an
instant can be defined up to renaming.
Proposition 44 Suppose (P1 , E1 ) =α (P2 , E2 ). Then the following holds.
P ′′

P ′′

1
2
(1) If (P1 , E1 ) →
(P1′ , E1′ ) then (P2 , E2 ) →
(P2′ , E2′ ) and (P1′ ∪ P1′′ , E1′ ) =α (P2′ ∪ P2′′ , E2′ ).
(2) (P1 , E1 ) ↓ if and only if (P2 , E2 ) ↓.
(3) If (P1 , E1 ) ↓ then ⌊P1 ⌋E1 =α ⌊P2 ⌋E2 .

Proof. (1) By case analysis on the reduction.
(2) Suppose Ti = Ci [await si ] for i = 1, 2 and σ is a renaming such that σT1 = T2 and
E1 = E2 ◦ σ. Then check that (T1 , E1 ) ↓ if and only if (T2 , E2 ) ↓.
(3) Suppose (T1 , E1 ) =α (T2 , E2 ) and (T1 , E1 ) ↓. Proceed by induction on the structure of
T1 .
✷
Then we check the strong confluence lemma from which determinism follows.
P ′′

P ′′

1
2
Lemma 45 (strong confluence) If (P, E) →
(P1′ , E1′ ), (P, E) →
(P2′ , E2′ ), and (P1′ ∪

′′

P

′′

′′

′
′
, E12 , P21
, E21 such that (P1′ , E1′ ) →2
P1′′ , E1′ ) 6=α (P2′ ∪ P2′′ , E2′ ) then there exist P 1 , P 2 , P12
P

′′

′′

′′

′
′
′
′
(P12
, E12 ), (P2′ , E2′ ) →1 (P21
, E21 ), and (P12
∪ P1′′ ∪ P 2 , E12 ) =α (P21
∪ P2′′ ∪ P 1 , E21 ).

Proof. It is convenient to work with a pair (P, E) such that all bound names are distinct
′′
′′
and not in dom(E). It is then possible to close the diagram directly taking P 2 = P2′′ , P 1 =
P1′′ , P12 = P21 , E12 = E21 = E1 ∨ E2 , where:

 true if E1 (s) = true or E2 (s) = true
false otherwise, if E1 (s) = false or E2 (s) = false
(E1 ∨ E2 )(s) =

↑
otherwise.
We can then derive the initial statement by repeated application of proposition 44.
29

✷

A.3

Proof of theorem 11

First, it is useful to note the following commutation of substitution and CPS translation.
Lemma 46 [s/x][[T ]](t, τ ) = [[[s/x]T ]](t, τ ), assuming {x} ∩ sig(t, τ ) = ∅.
P

Lemma 47 Suppose T R t, and (T, E) → (T ′ , E ′ ). Then T = C[∆] for some context C
and redex ∆ and exactly one of the following cases arises.
(1) ∆ ::= 0; T ′′ | (watch s 0). Then P = ∅, E = E ′ , and t = [[T ]](0, ǫ) = [[T ′ ]](0, ǫ).
(2) ∆ ::= thread T ′′ . Then P = {|T ′′ |}, E = E ′ , and (t, E) = ([[T ]](0, ǫ), E)
([[T ′ ]](0, ǫ), E).

{|[[T ′′ ]](0,ǫ)|}

→

∅

(3) ∆ ::= emit s | νs T ′′ | A(s). Then P = ∅ and (t, E) = ([[T ]](0, ǫ), E) → ([[T ′ ]](0, ǫ), E ′ ).
∅

(4) ∆ ::= await s and t = [[T ]](0, ǫ). Then P = ∅, E = E ′ , and (t, E) → ([[T ′ ]](0, ǫ), E).
∅

(5) ∆ ::= await s and t = A where A = [[T ]](0, ǫ). Then P = ∅, E = E ′ , and (t, E)(→
∅

) · (→)([[T ′ ]](0, ǫ), E).
Proof. We denote with π1 , π2 the first and second projection, respectively.
(1) If ∆ = 0; T then
[[C[0; T ]]](0, ǫ)
= [[0; T ]]([[C]](0, ǫ)) (by proposition 9)
= [[T ]]([[C]](0, ǫ))
(by CPS definition)
= [[C[T ]]](0, ǫ)
(by proposition 9) .
If ∆ = watch s 0 let (t, τ ) = [[C]](0, ǫ). Then
[[C[watch s 0]]](0, ǫ)
= [[watch s 0]](t, τ )
= [[0]](t, τ · (s, t))
=t
= [[0]](t, τ )
= [[C[0]]](0, ǫ)

(by
(by
(by
(by
(by

proposition 9)
CPS definition)
CPS definition)
CPS definition)
proposition 9) .

(2) We observe:
[[C[thread T ′′ ]]](0, ǫ)
= [[thread T ′′ ]]([[C]](0, ǫ))
(by proposition 9)
= thread [[T ′′ ]](0, ǫ).π1 ([[C]](0, ǫ)) (by CPS definition)
= thread [[T ′′ ]](0, ǫ).[[0]]([[C]](0, ǫ)) (by CPS definition)
{|[[T ′′ ]](0,ǫ)|}

→

[[C[0]]](0, ǫ)

(by (t5 ) and proposition 9)

(3) The cases where ∆ = (emit s) or ∆ = (νs T ) are straightforward. Suppose ∆ = A(s).
Assume (t, τ ) = [[C]](0, ǫ), sig(t, τ ) = {s′ } and A(x) = T with {x} ∩ {s′ } = ∅. We consider
30

the equation A(t,τ ) (x) = [[T ]](t, τ ) where we rely on the convention that the parameters s′
are omitted. Now we have:
[[C[A(s)]]](0, ǫ)
= [[A(s)]]([[C]](0, ǫ))
= A(t,τ ) (s)

(by proposition 9)
(by CPS definition)

∅

→ [s/x, s′ /s′ ][[T ]](t, τ )
= [[[s/x]T ]](t, τ )
(by substitution lemma 46)
= [[[s/x]T ]]([[C]](0, ǫ))
= [[C[[s/x]T ]]](0, ǫ)
(by proposition 9).
(4) We observe:
[[C[await s]]](0, ǫ) = [[await s]]([[C]](0, ǫ)) = present s t b
∅

where t = π1 ([[C]](0, ǫ)) = [[C[0]]](0, ǫ) and (present s t b, E) → (t, E).
(5) First unfold A(s) and then proceed as in case (4).

✷

Thus if T R t and T reduces then t can match the reduction and stay in the relation.
The proofs of the following three lemma 48, 49, and 50 rely on similar arguments. First,
we analyse the situation where t reduces.
p

Lemma 48 Suppose T R t, and (t, E) → (t′ , E ′ ). Then T = C[∆] and exactly one of the
following cases arises.
(1) ∆ ::= await s and t = A where A = [[T ]](0, ǫ). Then p = ∅, E = E ′ and T R t′ .
∅

(2) ∆ ::= await s and t = [[T ]](0, ǫ). Then p = ∅, E = E ′ , and (T, E) → (T ′ , E) with
t′ = [[T ′ ]](0, ǫ).
{|T ′′ |}

(3) ∆ ::= thread T ′′ . Then p = {|[[T ′′ ]](0, ǫ)|}, E = E ′ , and (T, E) → (T ′ , E) with
t′ = [[T ′ ]](0, ǫ).
∅

(4) ∆ ::= emit s | νs T ′′ | A(s). Then p = ∅, t = [[T ]](0, ǫ), and (T, E) → (T ′, E ′ ) with
t′ = [[T ′ ]](0, ǫ).
∅

(5) ∆ ::= 0; T ′′ | (watch s 0). Then p = ∅, E = E ′ , t = [[T ]](0, ǫ) (T, E) → (T ′ , E),
t = [[T ′ ]](0, ǫ), and T ′ is smaller than T .
Thus if T R t and t reduces then T can match the reduction and stay in the relation.
In the worst case, the number of reductions T has to make is proportional to its size. This
is because case (5) shrinks the thread.
Lemma 49 If T R t and (T, E) ↓ then exactly one of the following cases arises.
(1) t = [[T ]](0, ǫ). Then (t, E) ↓.
∅

(2) T = C[await s], t = A, and A = [[T ]](0, ǫ). Then (t, E) → ([[T ]](0, ǫ), E) and
([[T ]](0, ǫ), E) ↓.
31

Thus if T R t and (T, E) is suspended then (t, E) is suspended too possibly up to an
unfolding.
Lemma 50 If T R t and (t, E) ↓ then t = [[T ]](0, ǫ) and exactly one of the following cases
arises.
(1) T = 0 or T = C[await s] and (T, E) ↓.
∅

(2) T = C[∆], ∆ ::= 0; T ′′ | (watch s 0). Then (T, E) → (C[0], E) and t = [[C[0]]](0, ǫ).
Thus if T R t and (t, E) is suspended then (T, E) is suspended too possibly up to the
reduction of redexes 0; T ′′ or (watch s 0). Again the number of these reductions is at most
proportional to the size of T . Next we look at the computation at the end of the instant.
Lemma 51 If T R t, (T, E) ↓, and (t, E) ↓ then ⌊T ⌋E R ⌊t⌋E .
Proof. Exactly one of the following cases arises.
(1) T = t = 0 = ⌊T ⌋E = ⌊t⌋E .
(2) T = C[await s], t = [[T ]](0, ǫ). We have to explicit the structure of t and relate it to the
structure of the context. First, we notice that the context C can be written in the general
form
C = (watch s1 · · · (watch sn [ ]Un+1 )Un · · · )U1
where Ui ::= ǫ | ; Ti so that the presence of Ui is optional. Then we claim that t can be
written as:
t = present s tn+1 (ite s1 t1 · · · (ite sn tn A) · · · ), A = t
where ti is defined inductively as follows:
t0
τ0

= 0,
=
ǫ

[[Ti+1 ]](ti , τi ) if Ui+1 = ; Ti+1
ti
otherwise
= τi · (si+1 , ti+1 )

ti+1 =

for i = 0, . . . , n

τi+1

for i = 0, . . . , n − 1

In particular, we have [[C]](0, ǫ) = (tn+1 , τn ). Now two subcases can arise.
(2.1) E(s1 ) = · · · = E(sn ) = false. Then ⌊T ⌋E = T and ⌊t⌋E = A so that thanks to the
second clause in the definition of R we have ⌊T ⌋E R⌊t⌋E .
(2.2) E(s1 ) = · · · = E(si−1 ) = false and E(si ) = true. Then
⌊T ⌋E = (watch s1 · · · (watch si−1 0 Ui )Ui−1 · · · )U1 , and [[⌊T ⌋E ]](0, ǫ) = ti = ⌊t⌋E .

✷

To summarise, we have shown that the relation R acts as a kind of weak bisimulation
with respect to reduction and suspension and that it is preserved by the computation at
the end of the instant. Note that the relation R is immediately extended to programs
in the source and target language by saying that the source program P is related to the
target program p if there is a bijection i between the threads in P and those in p such that
if i(T ) = t then T R t.
32

Lemma 52 Suppose P R p. Then for every environment E:
(1) If (P, E)(→)∗(P ′, E ′ ) and (P ′ , E ′ ) ↓ then for some p′ (p, E)(→)∗(p′ , E ′ ), (p′ , E ′ ) ↓, and
⌊P ′ ⌋E ′ R ⌊p′ ⌋E ′ .
(2) Vice versa, if (p, E)(→)∗ (p′ , E ′ ) and (p′ , E ′ ) ↓ then for some P ′ (P, E)(→)∗(P ′ , E ′ ),
(p′ , E ′ ) ↓, and ⌊P ′ ⌋E ′ R ⌊p′ ⌋E ′ .
From lemma 52 we derive that if P R p then tr (P ) = tr (p) and in particular that
tr (P ) = tr ([[P ]]) as required.

A.4

Proof of proposition 14

Let X be a finite set of thread identifiers. We define its depth as the length of the longest
descending chain with respect to ≻. Consider an equation. A(x) = T . The function
Call (T, ǫ) implicitly associates a label ℓ ∈ {ǫ, κ} with every occurrence of a thread identifier
in T . Next consider a related equation A(t,τ ) (x) = [[T ]](t, τ ) and an occurrence of a thread
identifier B in T . Two situations may arise: (1) The label associated with the occurrence
of B is κ and then A ≻ B. (2) The label associated with the occurrence of B is ǫ and then
A  B and moreover the index (t′ , τ ′ ) of B in the CPS translation is either (0, ǫ) or (t, τ ).
Then to compute the system of recursive equations associated with the CPS translation
proceed as follows. First, compute the equations of ‘index’ (0, ǫ), i.e., those of the shape
A(0,ǫ) (x) = [[T ]](0, ǫ) and collect all the thread identifiers A(t,τ ) occurring on the right
hand side with an index (t, τ ) different from (0, ǫ). Continue, by computing the equations
A(t,τ ) = [[T ]](t, τ ) for the new indexes (t, τ ). Then collect again the identifiers with new
indexes. At each step the depth of the finite set of thread identifiers with new indexes
decreases. Thus this process terminates with a finite number of recursive equations.
✷

A.5

Proof of theorem 19

We start by describing the simulation of simple deterministic push down automata. The
empty stack is represented by the symbol Z. The stack alphabet has only one symbol S.
A configuration of an automaton is a pair (q, S · · · SZ) composed of a state and a stack,
and its possible transitions are:
(q, w) 7→ (q ′ , Sw)
(q, Sw) 7→(q ′ , w)
(q ′ , w) w = Z
(q, w) 7→
(q ′′ , w) w =
6 Z

(increment)
(decrement)
(test zero)

We introduce as many thread identifiers as states. Each of these thread identifiers has
parameters inc, dec, zero, ack which we omit. Depending on the instructions associated
with the state, we introduce one of the following equations:
q = (emit inc); (await ack ); pause; q ′ (increment)
q = (emit dec); (await ack ); pause; q ′ (decrement)
q = (present zero (pause; q ′ ) q ′′ )
(test zero)
33

Note that the control starts at most one operation per instant and that it waits for the
completion of the operation before proceeding to the following one.
Next we represent the stack. This is similar to what is done, e.g., in CCS [15]. We
abbreviate with s a vector of 5 signals dec, inc, zero, ack , abort. A thread Z depends on
such a vector for interactions on the ‘left’. A thread S (or S+ , Sr , Sl ) depends on a pair of
vectors s, s′ for interactions on the ‘left’and on the ‘right’, respectively.
Z(s)

= (watch abort (emit zero);
(present inc
(emit ack ); pause; (νs′ (thread S(s, s′ ), Z(s′ )))
(thread Z(s))))

S(s, s′ )

= (thread
(watch dec (await inc); pause; (thread S+ (s, s′ ))),
(watch inc (await dec); pause; (thread Sr (s, s′ ))))

S+ (s, s′ ) = (νs′′ (emit ack ); (thread S(s, s′′ ), S(s′′ , s′ )))
Sr (s, s′ )

= (present zero ′ (emit abort ′ ); pause; (emit ack ); Z(s)
(emit dec ′ ); Sl (s, s′ )

Sl (s, s′ )

= (await ack ′ ); pause; (emit ack ); S(s, s′ )

A configuration (q, S · · · SZ) of the automaton is mapped to a program which is essentially
equivalent to: (νs0 , . . . , sn (thread q(s0 ), S(s0 , s1 ), . . . , S(sn−1 , sn ), Z(sn ))). It is not difficult
to check that the program can simulate the transitions of the automata (and this is all
we need to check since the program is deterministic!). The more complex dynamics, is
introduced by the decrement. Roughly, the decrement of a stack represented by the threads
S, S, S, Z goes through the following transformations:
S, S, S, Z → Sr , S, S, Z → Sl , Sr , S, Z → Sl , Sl , Sr , Z → Sl , Sl , Z → Sl , S, Z → S, S, Z
There is a wave from left to right that transforms S into Sl , when the wave meets Z,
it aborts Z, transforms the rightmost S into Z, and produces a wave from right to left
that turns Sl into S again. The simulating program can be put in tail recursive form via
the CPS translation. In particular, note that all recursive calls in the scope of a watch are
under a thread statement that has the effect of resetting the evaluation context. Finally, we
remark that the simulation of deterministic push down automata can be easily generalised
to deterministic two counters machines by simply letting the control operate on two distinct
stacks.
✷

A.6

Proof of proposition 20
s

(1) By induction on the proof of P → P ′ .
34

s

(2) If P → · then P has the shape D[emit s] for a suitable context D built out of restrictions
and parallel compositions. It is easily checked that after a transition the emission emit s
is still observable.
s

(3) By induction on the proof of P → P ′ .

A.7

✷

Proof of lemma 31

Most properties follow by routine verifications. We just highlight some points.
(1) Recalling that P ≡L Q and P ↓ implies Q ↓.
(2) Condition (S1) entails conditions (B1), (B3), and (L2), while condition (S2) (with
(S1)) entails conditions (B2) and (L1).
(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 removed. 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.
(5) Direct diagram chasing.
(6) We reason up to ≡L .
(7) We show {(P1 | Q, P2 | Q) | P1 ≡L P2 } is a strong labelled bisimulation up to ≡L .
s′

Let us focus on condition (S2). Let X = {s′ | (P1 | P2 ) → ·} and let S ′ be the parallel
composition of the emissions (emit s) where s ∈ X. Suppose (P1 | Q | S) ↓. Then we note
that P1 | Q | S ≡L (P1 | S ′ | S) | (Q | S ′ | S) and ⌊P1 | Q | S⌋ ≡L ⌊P1 | S ′ | S⌋ | ⌊Q | S ′ |
S⌋. A similar remark applies to P2 | Q. Then we can conclude by reasoning up to ≡L . ✷

A.8

Proof of lemma 35

(1) We show that the relation R =≈L ∪{( P | (emit s), Q | (emit s) ) | P ≈L Q} is a
labelled bisimulation up to ≡L . We assume P ≈L Q and we analyse the conditions (B1−3)
and (L1 − 2).
τ

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

35

s′

s′

(B3) Suppose P | (emit s) → · and P | (emit s) ⇓L . If s = s′ then Q | (emit s) → · and we
s′

are done. Otherwise, it must be that P → ·. Moreover, P ⇓L . Then P ≈L Q and condition
τ

s′

τ

s′

(B3) imply that Q ⇒ Q′ → ·, and P ≈L Q′ . Hence Q | (emit s) ⇒ Q′ | (emit s) → · and
we can conclude.
(L1) Suppose S = (emit s1 ) | · · · | (emit sn ). Define S ′ = (emit s) | S. Then P ≈L Q and
condition (L1) applied to S ′ allows to conclude.
s′

s′

(L2) Suppose P | (emit s) → P ′ | (emit s). Necessarily P → P ′ . Given P ≈L Q and
s′

condition (L2) two cases may arise: (1) Q ⇒ Q′ and P ′ ≈L Q′ . Then the conclusion is
τ
τ
immediate. (2) Q ⇒ Q′ and P ′ ≈L Q′ | (emit s′ ). Then Q | (emit s) ⇒ Q′ | (emit s) and
we observe that (Q′ | (emit s)) | (emit s′ ) ≡L (Q′ | (emit s′ )) | (emit s) thus closing the
diagram up to ≡L .
(2) It is easily checked that the identity relation is a labelled bisimulation. Reflexivity
follows. As for transitivity, we check that the relation ≈L ◦ ≈L is a labelled bisimulation
up to ≡L .
(B1 − 3, L1) These cases are direct. For (B3), recall proposition 29(2).
s

(L2) Suppose P1 ≈L P2 ≈L P3 and 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′ | (emit s). By P2 ≈L P3 and repeated application of (B1) we derive that P3 ⇒ P3′
and P2′ ≈L P3′ . By property (1) the latter implies that P2′ | (emit s) ≈L P3′ | (emit s) and
τ
s
τ
we combine with P1 ≈L P2′ | (emit s) 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 | (emit s), and moreover P32 | (emit s) ⇒ P3′ | (emit s) with P2′ ≈L P3′ | (emit s).
τ
τ
Two subcases may arise: (i) P32 ⇒ P3′ . Then we have P3 ⇒ P3′ , P2′ ≈L P3′ | (emit s) and we
s
s
can conclude. (ii) P32 ⇒ P3′ . Then we have P3 ⇒ P3′ and P2′ ≈L P3′ | (emit s) ≡L P3′ .
(3) We show that {(νs P, νs Q) | P ≈L Q} is a labelled bisimulation up to ≡L .
τ

τ

(B1) If νs P → P ′′ then P ′′ = νsP ′ and P → P ′ . From P ≈L Q and (B1) we derive
τ
τ
Q ⇒ Q′ and P ′ ≈L Q′ . Then νs Q ⇒ νs Q′ and we conclude.
s′

s′

τ

s′

(B3) If νs P → · (s 6= s′ ) then P → ·. From P ≈L Q and (B3) we derive Q ⇒ Q′ , Q′ → ·,
τ

s′

and P ≈L Q′ . To conclude, note that νs Q ⇒ νs Q′ and νs Q′ → ·.
(L1) Let S = (emit s1 ) | · · · | (emit sn ) with s 6= si for i = 1, . . . , n. If ((νs P ) | S) ↓ then
τ
(P | S) ↓. From P ≈L Q and (L1) we derive (Q | S) ⇒ (Q′ | S), (Q′ | S) ↓, (P | S) ≈L
τ
(Q′ | S), and ⌊P | S⌋ ≈L ⌊Q′ | S⌋. This implies that ((νs Q) | S) ⇒ ((νs Q′ ) | S) and
((νs Q′ ) | S) ↓. We observe that ((νs P ) | S) ≡L νs (P | S), ((νs Q′ ) | S) ≡L νs (Q′ | S),
⌊(νs P ) | S⌋ ≡L νs ⌊P | S⌋, and ⌊(νs Q′ ) | S⌋ ≡L νs ⌊Q′ | S⌋. Then we can close the
diagram up to ≡L .
s′

s′

(L2) Suppose νs P → P ′′ . Then s 6= s′ and P ′′ = νs P ′ with P → P ′. From P ≈L Q
s′

s′

and (L2) two cases may arise. (1) If Q ⇒ Q′ and P ′ ≈L Q′ then νs Q ⇒ νs Q′ and we
36

τ

τ

are done. (2) If Q ⇒ Q′ and P ′ ≈L Q′ | (emit s′ ) then νs Q ⇒ νs Q′ and we note that
νs Q′ | (emit s′ ) ≡L νs (Q′ | (emit s′ )) thus closing the diagram up to ≡L .
(4) We show that R = {(P1 | Q, P2 | Q) | P1 ≈L P2 }∪ ≈L is a labelled bisimulation up to
≡L .
τ

(B1) Suppose (P1 | Q) → P ′ .
(B1)[1] If the τ transition is due to P1 or Q then the corresponding P2 or Q matches the
transition and we are done.
s
s
(B1)[2] Otherwise, suppose P1 → P1′ and Q → Q.
s
τ
(B1)[2.1] If P2 ⇒ P2′ and P1′ ≈L P2′ then (P2 | Q) ⇒ (P2′ | Q) and we are done.
τ
τ
(B1)[2.2] If P2 ⇒ P2′ and P1′ ≈L (P2′ | (emit s)) then (P2 | Q) ⇒ (P2′ | Q) and ((P2′ | Q) |
(emit s)) ≡L ((P2′ | (emit s)) | Q) so that we close the diagram up to ≡L .
s

s

(B1)[3] Otherwise, suppose P1 → P1 and Q → Q′ .
(B1)[3.1] If ¬P1 ⇓L then by lemma 29, ¬(P1 | Q) ⇓L , ¬(P1 | Q′ ) ⇓L , ¬P2 ⇓L , ¬(P2 | Q) ⇓L .
Therefore (P1 | Q′ ) ≈L (P2 | Q).
s

τ

(B1)[3.2] If P1 ⇓L then P2 ⇒ P2′ and P1 ≈L P2′ . Hence (P2 | Q) ⇒ (P2′ | Q′ ) and
(P1 | Q′ ) R (P2′ | Q′ ).
(B3) Suppose (P1 | Q) ⇓L .
s

τ

s

(B3)[1] Suppose P1 → ·. Then P1 ⇓L and by (B3) P2 ⇒ P2′ → · and P1 ≈L P2′ . Thus
τ
s
(P2 | Q) ⇒ (P2′ | Q) → · and we can conclude.
s

s

(B3)[2] Suppose Q →. Then (P2 | Q) → and we are done.
τ

(L1) Suppose (P1 | Q | S) ↓. Then (P1 | S) ↓ and from P1 ≈L P2 we derive (P2 | S) ⇒
s
s
(P2′ | S) ↓ and (P1 | S) ≈L (P2′ | S). In particular, {s | P1 | S → ·} = {s | P2′ | S → ·}. We
τ
can also derive that (P2 | Q | S) ⇒ (P2′ | Q | S), however (P2′ | Q | S) ↓ may fail because of
a synchronisation of P2′ and Q on some signal which is not already in S. Then we consider
s
S ′ as the parallel composition of emissions (emit s) where (P1 | Q) → ·. By lemma 31, we
derive that:
(i ) (P1 | Q | S) ≡L (P1 | S | S ′ ) | (Q | S | S ′ ) and
(ii ) (P2′ | Q | S) ≡L (P2′ | S | S ′ ) | (Q | S | S ′ ) .
We also observe that (P1 | S | S ′ ) ↓. Together with (P1 | S) ≈L (P2′ | S) this implies
τ
by (L1) (P2′ | S | S ′ ) ⇒ (P2′′ | S | S ′ ) ↓, (P1 | S | S ′ ) ≈L (P2′′ | S | S ′ ), and ⌊P1 | S |
S ′ ⌋ ≈L ⌊P2′′ | S | S ′ ⌋. Now it must be that ((P2′′ | S | S ′ ) | (Q | S | S ′ )) ↓ because the
left component already emits all the signals that could be emitted by the right one (and
τ
vice versa). By conditions (S1 − 2) and (ii) we have that (P2′ | Q | S) ⇒ (P2′′′ | Q | S) ↓
and (P2′′′ | Q | S) ≡L (P2′′ | S | S ′ ) | (Q | S | S ′ ). To summarise, we have shown that
τ
(P2 | Q | S) ⇒ (P2′′′ | Q | S) ↓,
(P1 | Q | S) ≡L (P1 | S | S ′ ) | (Q | S | S ′ ) R (P2′′ | S | S ′ ) | (Q | S | S ′ ) ≡L (P2′′′ | Q | S), and
⌊P1 | Q | S⌋ ≡L ⌊P1 | S | S ′ | Q | S | S ′ ⌋ R ⌊P2′′ | S | S ′ | Q | S | S ′ ⌋ ≡L ⌊P2′′′ | Q | S⌋
37

as required by the notion of labelled bisimulation up to ≡L .
s

(L2) Suppose P1 | Q → P1′ | Q.
s
(L2)[1] Suppose P1 → P1′ .
s
(L2)[1.1] If P2 ⇒ P2′ and P1′ ≈L P2′ we are done.
τ
τ
(L2)[1.2] If P1 ⇒ P2′ and P1′ ≈L P2′ | (emit s) then P2 | Q ⇒ P2′ | Q and we note that
(P2′ | Q) | (emit s) ≡L (P2′ | (emit s)) | Q.
s
s
(L2)[2] Suppose Q → Q′ . Then (P2 | Q) → (P2 | Q′ ) and we are done.
(5) Let Q = present s P B and Q′ = present s P ′ B ′ .
τ

(B1) Note that ¬(Q → ·).
s

(B3) Note that ¬(Q → ·).
(L1) Suppose S = emit s1 | · · · | emit sn and that (Q | S) ↓. Then si 6= s for i = 1, . . . , n
and ⌊Q | S⌋ = h|B|i{s1 ,...,sn } . Note that (Q′ | S) ↓ too, and from the hypothesis B ≈L B ′
we derive ⌊Q | S⌋ ≈L ⌊Q′ | S⌋ = h|B|i{s1 ,...,sn } .
s

s

(L2) The transition present s P B → P | (emit s) is matched by present s P ′ B ′ → P ′ |
(emit s). By hypothesis, P ≈L P ′ and by (1), we derive P | (emit s) ≈L P ′ | (emit s). ✷

A.9

Proof lemma 41

(1) Condition (B3)↓ is weaker than condition (B3). Therefore, P ≈L Q implies P ≈↓L Q.
(2) Reflexivity is obvious. For transitivity, as usual, we have to check that ≈↓L ◦ ≈↓L is a
↓-labelled bisimulation. We focus on the new condition (B3)↓ . Suppose P1 ≈↓L P2 ≈↓L P3 ,
s
τ
s
τ
P1 ↓, and P1 → ·. By (B3)↓ , P2 ⇒ P2′ and P2′ → ·. By (B2), P2 ⇒ P2′′, P2′′ ↓, and
s
τ
τ
P1 ≈↓L P2′′ . By confluence, P2′ ⇒ P2′′ and P2′′ → ·. By (B1), P3 ⇒ P3′ and P2′′ ≈↓L P3′ . By
s
τ
s
τ
(B3)↓ , P3′ ⇒ P3′′ , P2′′ ≈↓L P3′′ , and P3′′ → ·. Thus we have that P3 ⇒ P3′′ , P3′′ → ·, and
↓
↓
P1 ≈L P2′′ ≈L P3′′ as required by condition (B3)↓ .
(3) We check that:

τ

τ

R = Id ∪ {(P, Q) | P → Q or Q → P }
τ

is a labelled bisimulation up to ≡L , where Id is the identity relation. Thus P → Q implies
P ≈L Q. By (1), P ≈↓L Q and by proposition 36, tr (P ) = tr (Q).
τ

τ

τ

(B1) Suppose P → P1 . If P → Q then by confluence, either P1 = Q or ∃ P12 P1 →
τ
τ
τ
P12 and Q → P12 . In the first case, Q ⇒ Q and (P1 , Q) ∈ R. In the second case, Q ⇒ P12
τ
τ
and (P1 , P12 ) ∈ R. On the other hand, if Q → P then Q ⇒ P1 .
s

τ

s

τ

(B3) Suppose P ⇓L and P → ·. If P → Q then Q → · and Q ⇒ Q. On the other hand,
τ
τ
if Q → P then Q ⇒ P .
τ
τ
(L1) If P → Q then P | S ↓ is impossible. On the other hand, if Q → P and P | S ↓ then
τ
Q | S ⇒ P | S.
38

s

τ

τ

s

(L2) Suppose P → P1 . If P → Q then either P1 = Q or ∃ P12 P1 → P12 and Q → P12 . In
τ
s
the first case, we have Q ⇒ Q and P1 R Q ≡L Q | (emit s). In the second case, Q ⇒ P12
τ
s
and (P1 , P12 ) ∈ R. On the other hand, if Q → P then Q ⇒ P1 .
(4) Obviously, the critical condition to check is (B3). By proposition 39 we can use the
s
τ
predicate ⇓ rather than the predicate ⇓L . So suppose P1 ≈L Q1 , P1 → ·, P1 ⇒ P2 , and
τ
τ
s
P2 ↓. By (B1), Q1 ⇒ Q2 and P2 ≈↓L Q2 . By (B3)↓ , Q2 ⇒ Q3 , Q3 → ·, and P2 ≈↓L Q3 . By
(3), P1 ≈↓L P2 . By transitivity of ≈↓L , P1 ≈↓L Q3 .
✷

A.10

Proof of lemma 42
I/O

(1) This follows from the remark that P | (emit s) → P ′ if and only if P

I∪{s}/O

→

P ′.

(2) We check the 5 conditions.
τ
τ
(B1) If P → P ′ then tr (P ) = tr (P ′ ), by lemma 41(3). Thus Q ⇒ Q and (P ′, Q) ∈ R.
s

(B3) In view of proposition 40, it is enough to check condition (B3)↓ . If P ↓ and P → ·
∅/O

∅/O

τ

s

then P → ⌊P ⌋ and s ∈ O. Thus Q → Q′ . In particular, Q ⇒ Q′′ , Q′′ →. By lemma
41(3), tr (Q) = tr (Q′′ ). Thus (P, Q′′ ) ∈ R.
I/O

s

τ

s

(L1) If P | S ↓ then P → P ′ where I = {s | S → ·}, P | S ⇒ P ′′ , P ′′ ↓, O = {s | P ′′ → ·},
I/O

τ

and P ′ = ⌊P ′′ ⌋. By (1), tr (P | S) = tr (Q | S). Thus Q → Q′ where Q | S ⇒ Q′′ , Q′′ ↓,
and Q′ = ⌊Q′′ ⌋. Now (P ′′ , Q′′ ), (P ′, Q′ ) ∈ R since by lemma 41(3) tr (P ′′) = tr (P | S) =
tr (Q | S) = tr (Q′′ ).
s
τ
(L2) If P → P ′ then (P | (emit s)) → (P ′ | (emit s)) and by lemma 41(3) tr (P | s) =
tr (P ′ | (emit s)). Moreover, P ′ ≈L (P ′ | (emit s)) thus by proposition 36, tr (P ′ ) = tr (P ′ |
(emit s)). By (1), tr (P | (emit s)) = tr (Q | (emit s)). We can conclude by considering that
τ
Q ⇒ Q and (P ′ , Q | (emit s)) ∈ R since tr (P ′) = tr (P ′ | (emit s)) = tr (P | (emit s)) =
tr (Q | (emit s)).
✷

39

