Roberto M Amadio

A synchronous π-calculus

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.

Introduction

Concurrent and/or distributed systems are usually classified according to two main parameters (see, e.g., [START_REF] Lamport | Distributed computing: models and methods[END_REF]): 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 [START_REF] Lynch | Distributed algorithms[END_REF][START_REF] Tel | Introduction to distributed algorithms[END_REF] and comparing the algorithms for basic problems such as leader election, minimum spanning tree, consensus,. . . in the synchronous and asynchronous case. In [START_REF] Lynch | Distributed algorithms[END_REF][START_REF] Tel | Introduction to distributed algorithms[END_REF], 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 [START_REF] Hopcroft | Introduction to automata theory, languages, and computation[END_REF]: 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 [START_REF] Milner | Calculi for synchrony and asynchrony[END_REF] and Meije [START_REF] Austry | Algèbre de processus et synchronisation[END_REF] 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 [START_REF] Boussinot | The SL synchronous language[END_REF]. Threads in the SL model interact through signals as opposed to channels. A cooperative scheduling (as opposed to pre-emptive, see [START_REF] Ousterhout | Why threads are a bad idea (for most purposes)[END_REF]) is sometimes considered, though this is not quite a compulsory choice and it is not followed here. This 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 [START_REF] Amadio | Reactive programming, revisited[END_REF] for a discussion of the applications and implementation techniques).

The SL model can be regarded as a relaxation of the Esterel model [START_REF] Berry | The Esterel synchronous programming language[END_REF] 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 [START_REF] Boussinot | Reactive C: An extension of C to program reactive systems[END_REF][START_REF]Reactive programming[END_REF][START_REF] Serrano | Scheme fair threads[END_REF][START_REF] Mandel | ReactiveML, a reactive extension to ML[END_REF]). For instance, the Reactive ML language [START_REF] Mandel | ReactiveML, a reactive extension to ML[END_REF] 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. [START_REF] Saraswat | Timed default concurrent constraint programming[END_REF] 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 [START_REF] Milner | A calculus of mobile processes, parts 1-2[END_REF] and its relatives can be regarded as typical abstract models of asynchronous concurrent programming while various languages such as Lustre [START_REF] Caspi | LUSTRE: a declarative language for programming synchronous systems[END_REF], Esterel [START_REF] Berry | The Esterel synchronous programming language[END_REF], and SL [START_REF] Boussinot | The SL synchronous language[END_REF] 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 [START_REF] Amadio | The SL synchronous language, revisited[END_REF], 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 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 spi). 1 Our contribution is to show that the notion of bisimulation equivalence introduced in [START_REF] Amadio | The SL synchronous language, revisited[END_REF] 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 [START_REF] Honda | On reduction-based process semantics[END_REF]. 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 [START_REF] Honda | On reduction-based process semantics[END_REF][START_REF] Amadio | On bisimulations for the asynchronous π-calculus[END_REF][START_REF] Fournet | A hierarchy of equivalences for asynchronous calculi (extended abstract)[END_REF]], Prasad's calculus of broadcasting systems [START_REF] Prasad | A calculus of broadcasting systems[END_REF][START_REF] Hennessy | Bisimulations for a calculus of broadcasting systems[END_REF], and the ambient calculus [START_REF] Merro | Behavioral theory for mobile ambients[END_REF], 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 [START_REF] Mandel | ReactiveML, a reactive extension to ML[END_REF], reactivity [START_REF] Amadio | Resource control for synchronous cooperative threads[END_REF], and non-interference [START_REF] Matos | Typing non-inteference for reactive programs. RR-INRIA 5594[END_REF].

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.

The Sπ-calculus

Programs P, Q, . . . in the Sπ-calculus are defined as follows:

P ::= 0 | | A(e) | | se | | s(x).P, K | | [s 1 = s 2 ]P 1 , P 2 | | [u ¤ p]P 1 , P 2 | | νs P | | P 1 | P 2 K ::= A(r)
We use the notation m for a vector m 1 , . . . , m n , 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 v 1 , . . . , v n have been emitted on the signal s in the current instant then s(x).P, K evolves nondeterministically into [v i /x]P for some v i ([ / ] is our notation for substitution). On the other hand, if no value is emitted then the continuation K is evaluated at the end of the instant. [s 1 = s 2 ]P 1 , P 2 is the usual matching function of the π-calculus that runs P 1 if s 1 = s 2 and P 2 , otherwise. Here both s 1 and s 2 are free. [u ¤ p]P 1 , P 2 , 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 σP 1 if σ is the result of matching u against p, and P 2 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 . (P 1 | P 2 ) runs in parallel P 1 and P 2 . 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. 2The definition of program relies on the following syntactic categories: 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).

Sig ::= s | | t | | • • • (signal names) Var ::= Sig | | x | | y | | z | | • • • (variables) Cnst ::= * | | nil | | cons | | c | | d | | • • • (constructors) Val ::= Sig | | Cnst(

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 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 (t 1 , t 2 ) → t meaning that it waits two arguments of type t 1 and t 2 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,. . .

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 match(v, p) = σ if dom(σ) = FV (p), σ(p) = v ↑ otherwise
To appreciate the difference, assume s = s ′ and consider P = [s = s ′ ]P 1 , P 2 and

P ′ = [[s] ¤ [s ′ ]]P 1 , P 2 .
In the first case, P reduces to P 2 while in the second case, P ′ reduces to [s/s ′ ]P 1 . Indeed, in the first case s ′ is a constant while in the second case it is a bound variable.

Informal reduction semantics

Assume v 1 = v 2 are two distinct values and consider the following program in Sπ:

P = ν s 1 , s 2 ( s 1 v 1 | s 1 v 2 | s 1 (x). (s 1 (y). (s 2 (z). A(x, y) , B(!s 1 )) , 0) , 0 )
If we forget about the underlined parts and we regard s 1 , s 2 as channel names then P could also be viewed as a π-calculus process. In this case, P would reduce to

P 1 = νs 1 , s 2 (s 2 (z).A(σ(x), σ(y))
where σ is a substitution such that σ(x), σ(y) ∈ {v 1 , v 2 } and σ(x) = σ(y). In Sπ, signals persist within the instant and P reduces to

P 2 = νs 1 , s 2 (s 1 v 1 | s 1 v 2 | (s 2 (z).A(σ(x), σ(y)), B(!s 1 )))
where

σ(x), σ(y) ∈ {v 1 , v 2 }.
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 1 , = sig 2 , = ind 1 , = ind 2 , and rec in the following Table 1), and by adding the rule:

sv | s(x).P, K → sv | [v/x]P
What happens next? In the π-calculus, P 1 is deadlocked and no further computation is possible. In the Sπ-calculus, the fact that no further computation is possible in P 2 is detected and marks the end of the current instant. Then an additional computation represented by the relation → moves P 2 to the following instant:

P 2 → P ′ 2 = νs 1 , s 2 B(ℓ) where ℓ ∈ {[v 1 ; v 2 ], [v 2 ; v 1 ]}.
Thus at the end of the instant, a dereferenced signal such as !s 1 becomes a list of (distinct) values emitted on s 1 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.

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 → 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)

The rules (= ind 1 ) and (= ind 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 α = τ 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.

(out) sv sv → sv (in) s(x).P, K sv → [v/x]P | sv (par) P 1 α → P ′ 1 bn(α) ∩ fn(P 2 ) = ∅ P 1 | P 2 α → P ′ 1 | P 2 (synch) P 1 νt sv → P ′ 1 P 2 sv → P ′ 2 {t} ∩ fn(P 2 ) = ∅ P 1 | P 2 τ → νt (P ′ 1 | P ′ 2 ) (ν) P α → P ′ t / ∈ n(α) νt P α → νt P ′ (ν ex ) P νt sv → P ′ t ′ = s t ′ ∈ n(v)\{t} νt ′ P (νt ′ ,t)sv → P ′ (= sig 1 ) [s = s]P 1 , P 2 τ → P 1 (= sig 2 ) s 1 = s 2 [s 1 = s 2 ]P 1 , P 2 τ → P 2 (= ind 1 ) match(v, p) = σ [v ¤ p]P 1 , P 2 τ → σP 1 (= ind 2 ) match(v, p) =↑ [v ¤ p]P 1 , P 2 τ → P 2 (rec) A(x) = P A(v) τ → [v/x]P Table 1: Labelled transition system during an instant (0) 0 ∅,V -→ 0 (out) v occurs in V (s) sv [{v}/s],V -→ 0 (in) s / ∈ dom(V ) s(x).P, K ∅,V -→ V (K) (par) P i E i ,V -→ P ′ i i = 1, 2 (P 1 | P 2 ) E 1 ∪E 2 ,V -→ (P ′ 1 | P ′ 2 ) (ν) P E,V ′ -→ P ′ V ′ (s) -E(s) V [[]/s] = V ′ [[]/s] νs P E[∅/s],V -→ νs P ′ P E,V -→ P ′ V -E P → 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 →. 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 -M and say that v represents M if M = {v 1 , . . . , v n } 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 -E if V (s) -E(s) for every signal name s. We also write dom(V ) for {s | V (s) = []}. 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 → at the end of the instant, we rely on an auxiliary judgement P E,V -→ 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:

νs 1 (s 1 (x).0, A(!s 2 ) | s 2 v 3 ) | (s 2 v 2 | s 1 v 1 ) E,V -→ νs 1 (A(V (s 2 )) | 0) | (0 | 0) where E = [{v 1 }/s 1 , {v 2 , v 3 }/s 2 ] and, e.g., V = [[v 1 ]/s 1 , [v 3 ; v 2 ]/s 2 ].

Derived operators

We introduce some derived operators and some abbreviations. The calculi with pure signals considered in [START_REF] Boussinot | The SL synchronous language[END_REF][START_REF] Amadio | Reactive programming, revisited[END_REF][START_REF] Amadio | The SL synchronous language, revisited[END_REF] can be recovered by assuming that all signals have type Sig [START_REF] Amadio | The SL synchronous language, revisited[END_REF]. In 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,

P 1 ⊕ P 2 = νs (s(x)[x ¤ 0]P 1 , P 2 | 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 = {s 1 , . . . , s n } then [x / ∈ X]P is coded as [x = s 1 ]0, (• • • , [x = s n ]0, P • • • ).
3. v = c(p 1 , . . . , p n ). 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 = νs 1 , s 2 c(s 1 , c(s ′ 3 , s 2 , s 1 ), s ′ 3 )] {s ′ 3 ,s ′ 4 } P we write [x ¤ c(s 1 , c(s ′′ 3 , s 2 , s 1 ), s ′′ 3 )][s ′′ 3 = s ′ 3 ][s 1 / ∈ {s ′ 3 , s ′ 4 }][s 2 / ∈ {s ′ 3 , s ′ 4 }][s 1 = s 2 ]P .
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 s 1 , s 2 , and s ′′ 3 are bound in P .

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

Comparison with CBS and the timed π-calculus

In the calculus of broadcasting systems (CBS, [START_REF] Prasad | A calculus of broadcasting systems[END_REF]), 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 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 [START_REF] Berger | Congruence for two timed asynchronous π-calculi[END_REF] includes a primitive timer t 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.

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 ′ ↓ ) (weak suspension) P ⇓ L if ∃ α 1 , P 1 . . . , α n , P n ( P α 1 → P 1 • • • αn → P n , n ≥ 0, and P n ↓ ) (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 ′ ). (L2) If P νt sv → P ′ , P ⇓ L , {t} ∩ fn(Q) = ∅ then ∃ Q ′ (Q νt sv ⇒ Q ′ and P ′ R Q ′ ). (L3) If P sv → P ′ then ∃ Q ′ ( ( Q sv ⇒ Q ′ and P ′ R Q ′ ) or ( Q τ ⇒ Q ′ and P ′ R (Q ′ | sv) ) ). (L4) If S = s 1 v 1 | • • • | s n v n , n ≥ 0, P ′ = (P | S) ↓, and P ′ → P ′′ then ∃ Q ′ , Q ′′ ( (Q | S) τ ⇒ Q ′ , Q ′ ↓, P ′ R Q ′ , Q ′ → 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 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 (s 1 ⊕ s 2 ) ⊕ s 3 from the program s 1 ⊕ (s 2 ⊕ s 3 ). 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 [START_REF] Amadio | On bisimulations for the asynchronous π-calculus[END_REF]). 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 = s 1 v 1 | • • • | s n v n in this condition.
Consider the programs:

P = s 1 .0, A(!s 2 ) Q = s 1 .0, A([]) A(l) = [l ¤ []]0, s 3 Then P ↓, Q ↓, P → A([]), and Q → A([])
. However, if we plug P and Q in the context [•] | s 2 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).

Admittedly, the definition of labelled bisimulation is technical and following previous work [START_REF] Honda | On reduction-based process semantics[END_REF][START_REF] Amadio | On bisimulations for the asynchronous π-calculus[END_REF][START_REF] Fournet | A hierarchy of equivalences for asynchronous calculi (extended abstract)[END_REF], we seek its justification through suitable notions of barbed and contextual bisimulation.

Definition 4 (commitment) We write P ց s if P νt sv → • 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 → P ′′ then ∃ Q ′ , Q ′′ (Q τ ⇒ Q ′ , Q ′ ↓, P R Q ′ , Q ′ → 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. [START_REF] Honda | On reduction-based process semantics[END_REF][START_REF] Fournet | A hierarchy of equivalences for asynchronous calculi (extended abstract)[END_REF]).

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 when-

ever 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.

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 [START_REF] Castellani | Testing theories for asynchronous languages[END_REF][START_REF] Boreale | Trace and testing equivalence on asynchronous processes[END_REF] (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 [START_REF] Sangiorgi | A theory of bisimulation for the π-calculus[END_REF] to the present language. Third, one could plead for reduction congruence [START_REF] Milner | Barbed bisimulation[END_REF] rather than for contextual bisimulation and then try to see whether the two concepts coincide following [START_REF] Fournet | A hierarchy of equivalences for asynchronous calculi (extended abstract)[END_REF]. We refer to the literature for standard arguments concerning bisimulation vs. testing semantics (e.g., [START_REF] Milner | Communication and concurrency[END_REF]), early vs. open bisimulation (e.g., [START_REF] Sangiorgi | A theory of bisimulation for the π-calculus[END_REF]), and contextual vs. reduction bisimulation (e.g., [START_REF] Fournet | A hierarchy of equivalences for asynchronous calculi (extended abstract)[END_REF]).

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 P 0 α 1 → P 1 • • • αn → P n and P n ↓.
We build Q by induction on n. If n = 0 we can take Q = 0. Otherwise, suppose n > 0. By inductive hypothesis, there is Q 1 such that (P 1 | Q 1 ) ⇓. We proceed by case analysis on the first action α 1 . (α 1 = τ ) Then we can take

Q = Q 1 and (P 0 | Q) τ → (P 1 | Q 1 ). (α 1 = sv) Let Q = (Q 1 | sv). We have (P 0 | Q) τ → (P 1 | Q 1 | sv). Since P 1 sv → P 1 , we observe that (P 1 | Q 1 ) ⇓ implies (P 1 | Q 1 | sv) ⇓. (α 1 = νt sv) We distinguish three subcases. 1. If α 1 = st then define Q = s(t).Q 1 and observe that (P 0 | Q) τ → (P 1 | Q 1 ). 2. If α 1 = νt st then define again Q = s(t).Q 1 and observe that (i) (P 0 | Q) τ → νt (P 1 | Q 1 ) and (ii) (P 1 | Q 1 ) ⇓ implies νt (P 1 | Q 1 ) ⇓.
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)]Q 1 , 0 where x, t ′′ / ∈ FV (Q 1 ) and observe that: (i) (P 0 | Q) τ ⇒ νt (P 1 | Q 1 ) and (ii) (P 1 | Q 1 ) ⇓ implies νt (P 1 | Q 1 ) ⇓. For instance, if P 0 νt sc(t,t ′ ) → P 1 then we take Q = s(x).[x ¤ c(t, t ′′ )]Q 1 , 0 with x, t ′′ / ∈ FV (Q 1 ). (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 → Q 1 • • • αn → Q n with Q n ↓.
Show by induction on n that P ⇓ L . P

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.

(

) If P ≈ L Q and P ⇓ L then Q ⇓ L . 2
Proof.

(1) First we note that ¬P ⇓ L and P (2) Suppose P 0 ≈ L Q 0 and P 0 ⇓ L . We proceed by induction on the length n of the shortest sequence of transitions to a suspended program: P 0

α 1 → • • • αn → P n and P n ↓. If n = 0 then by (L4), Q 0 τ ⇒ Q ′ and Q ′ ↓. Thus Q 0 ⇓ L . If n > 0 then we analyse the first action α 1 . (α 1 = τ ) By (L1), Q 0 τ ⇒ Q 1 and P 1 ≈ L Q 1 . By inductive hypothesis Q 1 ⇓ L and therefore Q 0 ⇓ L . (α 1 = νt sv) By (L2), since P 0 ⇓ L , we have Q 0 νt sv ⇒ Q 1 and P 1 ≈ L Q 1 . By inductive hypothesis, Q 1 ⇓ L . Thus Q 0 ⇓ L . (α 1 = sv) According to (L3) we have two subcases. If Q 0 sv ⇒ Q 1 and P 1 ≈ L Q 1 then we reason as in the previous case. If Q 0 τ ⇒ Q 1 and P 1 ≈ L (Q 1 | sv) then by inductive hypothesis (Q 1 | sv) ⇓ L . By proposition 9, if (Q 1 | sv) ⇓ L then Q 1 ⇓ L . Thus Q 0 ⇓ L . P
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 = (s 1 | (s 2 ⊕ s 3 )) and Q = (s 1 | s 2 ) ⊕ (s 1 | s 3
). 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 ≈ ⇓ B Q (and therefore P ≈ ⇓ L Q). To see the latter, observe that P ց s 1 and that to match this commitment Q must choose between s 2 and s 3 .

• Let (t, t ′ ) abbreviate [t; t ′ ] and s → 0, Ω abbreviate s(x).[x ¤ 0]0, Ω. Consider:

P 1 = νt, t ′ (s(t, t ′ ) | (t.s 1 ⊕ t.s 2 ) | Q) P 2 = νt, t ′ (((s(t, t ′ ) | (t.s 1 )) ⊕ (s(t, t ′ ) | (t.s 2 ))) | Q) Q = t ′ → 0, Ω | t ′ 1
Note that P 1 , P 2 ⇓ L but ¬P 1 , P 2 ⇓. 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 P 1 ≈ ⇓ L P 2 . However, P 1 ≈ L P 2 . To see this, notice that P 1 ց s and that to match this commitment, P 2 has to resolve first the internal choice between s 1 and s 2 . A variant of this example where we remove the input prefix t. before the emissions s

i , i = 1, 2, shows that ≈ B is strictly included in ≈ ⇓ B . ( 2
| R) τ ⇒ νt, t ′ (s(t, t ′ ) | (t.s 1 ⊕ t.s 2 ) | Q | t | t ′ 0) ≡ P ′ 1
To match this move, suppose (P 2 | R) τ ⇒ P ′ 2 . Now P ′ 2 must be able to suspend while losing the possibility of committing on s 3 . Hence, there must be a synchronisation on s between P 2 and R. In turn, this synchronisation forces P 2 to choose between s 1 and s 2 . Suppose, e.g., (P 2 | R) chooses s 1 , then in a following move P ′ 1 chooses s 2 and becomes:

νt, t ′ (s(t, t ′ ) | s 2 | 0 | t | t ′ 0 | t ′ 1)
which is suspended and commits on s 2 . The program P ′ 2 cannot match this move. P 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.

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 = (s 1 v 1 | • • • | s n v n ), n ≥ 0 and (P | S) → P ′ implies (P | S) R (Q | S) and ∃ Q ′ (Q → 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) ↓. P

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 .

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, P 1 | (P 2 | P 3 ) ≡ L (P 1 | P 2 ) | P 3 , (P 1 | P 2 ) ≡ L (P 2 | P 1 ), νs 1 , s 2 P ≡ L νs 2 , s 1 P νs P 1 | P 2 ≡ L νs (P 1 | P 2 ) if s / ∈ fn(P 2 ). ( 4
) If P ≡ L Q then (P | S) ≡ L (Q | S) where S = (P 1 | • • • | P n ) and P i = 0 or P i = s i v i , 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 ↓.

( (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. (2) Follows directly from [START_REF] Amadio | The SL synchronous language, revisited[END_REF]. P

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 P 1 ≈ L P 2 and σ is an injective renaming then σP 1 ≈ L σP 2 .

(2) If P 1 ≈ L P 2 then (P 1 | sv) ≈ L (P 2 | sv).

(3) The relation ≈ L is reflexive and transitive.

(4) If P 1 ≈ L P 2 then νs P 1 ≈ L νs P 2 and (P 1 | Q) ≈ L (P 2 | Q).

Proof.

(1) By propositions 17(1) and 15.

(2) We show that the relation R =≈ L ∪{( P 1 | sv, P 2 | sv ) | P 1 ≈ L P 2 } is a labelled bisimulation up to ≡ L . We assume P 1 ≈ L P 2 and we analyse the conditions (L1 -4). by a series of reductions where first R interacts with O to learn the names t 1 . . . , t n , then it interacts with P 1 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 P 1 . 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 b i , c i are observable.

  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 .

α→

  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 . (L3) If P sv → 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.

( 4 )

 4 ) 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. Show that {(P | S, Q | S) | P ≡ L Q} is a strong labelled bisimulation where S is defined as in the statement. PThe following proposition summarizes the properties of the output transition. Proposition 18 (emission) (1) If P νt sv → P ′ then P ≡ L νt (sv | P ′′ ) and P ′ ≡ L (sv | P ′′ ).

( 2 )

 2 If P νt sv → P ′ then P ⇓ L if and only if P ′ ⇓ L . Proof. (1) In deriving P νt sv → 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.

By proposition 9 ,

 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 . P Remark 19 By proposition 18[START_REF] Amadio | Reactive programming, revisited[END_REF], 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.

(→ (P ′ 1 | 1 sv → P ′ 1 .

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

  Next, we decompose this series of reductions in several steps and analyse how the program νt (P 2 | O) | R may match them according to the definition of contextual bisimulation. Suppose firstνt (P 1 | O) | R τ ⇒ νt 1 (νt 2 , . . . , t n (P 1 | O) | (c 1 ⊕ a 2 (t 2 ) • • • ))The reduced program cannot commit on b 1 while it can commit on c 1 . If νt (P 2 | O) | R has to match this reduction, then R must necessarily perform the input action and stop at the same point of the control (c 1 ⊕ a 2 (t 2 ) • • • ). By this communication, the scope of the restricted name t 1 is extruded to R. The program O is composed only of emissions and therefore it cannot change. The program P 2 may perform some internal actions but it cannot interact with O and R.If we repeat this argument n times, we conclude that νt(P 1 | O) | 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 [v 1 ; . . . ; v n ] for the list of values cons(v 1 , . . . , cons(v n , 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).

	Val , . . . , Val )	(values v, v ′ , . . .)
	Pat ::= Var | | Cnst(Pat, . . . , Pat)	(patterns p, p ′ , . . .)
	Exp ::= Pat	(expressions e, e ′ , . . .)
	Rexp ::=!Sig | | Var | | Cnst(Rexp, . . . , Rexp) (exp. with dereferenciation r, r ′ , . . .)

  ) It is well known that barbed bisimulation is not preserved by parallel composition. For instance, s.s 1 ≈ B s.s 2 , but (s.s 1 | s) ≈ B (s.s 2 | s) if s 1 = s 2 . To show that ≈ ↓ L and ≈ ⇓ Lare not preserved by parallel composition consider again the programs P 1 and P 2 above in parallel with:R = s(t, t ′ ).((t | t ′ 0) ⊕ (t | t ′ 0 | s 3 ))where s(t, t ′ ).P abbreviates s(x).[x ¤ [t; t ′ ]]P, 0. Remark that (P 1

S for synchronous as in SCCS[START_REF] Milner | Communication and concurrency[END_REF] and SL[START_REF] Boussinot | The SL synchronous language[END_REF]. 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.

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.

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.

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.

* Partially supported by ANR-06-SETI-010-02.

This may happen because either P 1 or Q perform a τ action or because P 1 and Q synchronise. We consider the various situations that may occur.

We have two subcases. (L1) [4.1] Suppose ¬P 1 ⇓ L . By propositions 9 and 11, ¬νt

Also assume t = t 1 , t 2 and t ′ = t 1 , t 3 up to reordering so that the emission extrudes exactly the names t 1 among the names in t. We have two subcases depending which component performs the action.

where S Q is the parallel composition of emissions and I Q is the parallel composition of receptions. Thus we have:

where in particular, we have that

By the hypothesis P 1 ≈ L P 2 and (L4) we derive that: (i

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, t

The only possibility for an internal transition is that an emission in P ′′ 2 enables a reception in I Q but this contradicts the hypothesis that νt, t

. Therefore, we have that

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. P

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.

(

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)

Proof. We denote with a i , b i , c i , . . . 'fresh' signal names not occurring in the programs under consideration. We will rely on the signal names a i to extrude the scope of some signal names and on the signal names b i , c i to monitor the internal transitions of the programs. We define a relation R:

where:

By definition, if P 1 ≈ C P 2 then P 1 R P 2 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:

• 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 P 1 ⊕ P 2 reduces to either P 1 or P 2 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 = a 1 t 1 | • • • | a n t n and a = a 1 , . . . , a n , we will repeatedly use a program R(a)[P ] which is defined as follows:

Next we assume

for some t, O, and consider the conditions (L1 -4).

(L1) Suppose P 1

Note however that O cannot interact with P 2 and its derivatives because the signal names a do not occur in (P 1 | P 2 ). Hence it must be that P 2

Then by definition of the relation R, we derive that

where

Now we have: [START_REF] Amadio | Reactive programming, revisited[END_REF] Suppose P 1 ⇓ L . In this case, the commitments are observable. We define

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.


Bernard Bourgine

Nicolas Pedron

Eric Lavie

Eric Lavie Building

Building piezometric maps: contribution of geostatistical tools

come   L'archive ouverte pluridisciplinaire

Building piezometric maps: contribution of geostatistical tools

Bernard BOURGINE 1 , Nicolas PEDRON 1 & Eric LAVIE 2 1 BRGM (French Geological Survey) B.P. 6009 -45060 Orléans Cedex 2, Franceb.bourgine@brgm.fr; n.pedron@brgm.fr 2 Région Aquitaine -14 rue François de Sourdis -33077 Bordeaux -France. e.lavie@aquitaine.fr

Abstract:

The work presented has been carried out in the framework of an agreement entitled « Groundwater management in Aquitaine Region », signed between BRGM and Aquitaine Region for the 2008-2013 period, and financially supported by the Adour Garonne Water Agency.

This work aims at setting tools and procedures in order to facilitate the production of piezometric maps of the various aquifers of the Aquitanian Basin, using appropriate interpolation technique. The objective is also to propose as repeatable as possible workflows in order to facilitate and standardize the work, from data control to the final map.

Thus BRGM tested on two deep aquifers how geostatistical tools could be applied in order to answer to Aquitaine Region demand concerning :

-best practices for the construction of piezometric maps, as a function of available data and hydrogeological context, with computation of error maps, applying standard geostatistical techniques as well as more advanced ones, -optimisation of piezometer monitoring network, -production of a report showing how these methods can be applied on some « study cases », to be used by hydrogeologists in charge of building or using piezometric maps and not familiar with geostatistical tools.

Various geostatistical tools were tested and compared on two aquifers (a confined aquifer and an unconfined one) :

-standard (co)kriging including or not a polynomial drift, -kriging with an external drift based either on the result of an hydrodynamic flow model or on other variables like a smoothed topography, -co-kriging with partial derivatives in order to take into account boundary conditions and/or hydrogeological constraints like groundwater divide, -cross-validation procedures to identify anomalous data or to optimize the monitoring network.

Except for kriging with partial derivatives, for which few applications are reported in the literature, this paper presents « standard » geostatistical tools. It shows the interest of introducing more geostatistics in construction of piezometric maps, a domain where geostatistics is less widely used compared to other domains like mineral industry. Consecutive to this study the Department of Gironde (main Department of Aquitaine Region) started producing annual piezometric maps using geostatistical techniques. These maps and their associated kriging standard deviation are built using external drift kriging and are delivered on their web site. Geostatistics can help hydrogeologist to produce piezometric maps, but expertise of the hydrogeologist is essential to introduce appropriate calculation parameters and to validate the result.

Keywords:

Piezometric maps, kriging with partial derivatives, boundary conditions