Fran Cois Fages
email: ffrancois.fages@inria.fr

Paul Ruet
email: ruet@iml.univ-mrs.fr

Sylvain Soliman
email: sylvain.solimang@inria.fr

Linear concurrent constraint programming: operational and phase semantics

In this paper we give a logical semantics for the class CC of concurrent constraint programming languages and for its extension LCC based on linear constraint systems. Besides the characterization in intuitionistic logic of the stores of CC computations, we show that both the stores and the successes of LCC computations can be characterized in intuitionistic linear logic. We illustrate the usefulness of these results by showing with examples how the phase semantics of linear logic can be used to give simple \semantical" proofs of safety properties of LCC programs.

Introduction

Constraint programming is an emerging technology that has been proved very successful for complex system modeling and for solving declaratively combinatorial search problems 14]. The class CLP(X ) of constraint logic programming languages, introduced by Ja ar and Lassez 13], extends logic programming by combining the pure Horn fragment of rst-order logic (FOL) for de ning relations, with a xed decidable FOL language of primitive constraints over some structure X. The logical semantics of logic programming for both successes and nite failures extend smoothly to CLP languages, by considering the consequences in classical logic of both the program and the theory of the structure th(X). This is achieved in pure CLP for various observable properties of the execution: the existence of a successful derivation to a query 13], the set of computed answer constraints 21, 8], nite failures 13], the set of computed constraints with constructive negation 37, 6], etc. For example, computed answer constraints (i.e. nal states of computations) can be observed logically: any computed constraint entails the initial goal (modulo the logical translation of the program P ? and the constraint system C); conversely any constraint c entailing a goal G is covered (again modulo P ? and C) by a nite set of computed constraints c 1 : : : c n , i.e. C `8(c 1 : : : c n ) c). This allows for powerful analysis methods and simple program transformation techniques based on logical equivalences.

The class CC(X ) of Concurrent Constraint programming languages introduced by Saraswat 32] in 1987 arose as a natural combination of constraint logic programming and concurrent logic programming, with the introduction of a synchronization mechanism based on constraint entailment 21]. CC programming is a model of concurrent computation, where agents communicate through a shared store, represented by a constraint, which expresses some partial information on the values of the variables involved in the computation. An agent may add information c to the store (agent tell(c)), or ask the store to entail a given constraint (c ! A). Communication is asynchronous: agents can remain idle, and senders (constraints c) are not blocking.

The synchronization mechanism of CC languages gives an account for the co-routining facilities of implemented CLP systems, like the freeze predicate of Prolog, the delay mechanism of CLP(R) 13], or the constraint propagation schemes of CLP(F D). It also opens, to some extent, constraint programming to a new eld of applications which are traditional in concurrent programming, like reactive systems and protocol speci cations.

From the logic programming tradition however, the operational aspects of CC programming should also be closely connected to a logical semantics for reasoning about programs at di erent levels of abstraction, getting rid of useless details of the execution. The monotonic evolution of the store during CC computations provides CC languages with a simple denotational semantics in which agents are identi ed to closure operators on the semi-lattice of constraints [START_REF] Saraswat | Higher-order linear concurrent constraint programming[END_REF][START_REF] Ja | Constraint logic programming: a survey[END_REF]. Such denotational semantics are used in 5] to obtain a complete calculus for partial correctness assertions where the rules of the proof system mirror the equations of the denotational semantics.

In this article, we explore another route based on Girard's intuitionistic linear logic (ILL) 10]. We review the semantics of CC languages in the logic programming paradigm based on linear logic and we investigate the use of the phase semantics for proving safety properties of CC programs.

Outline of the paper.

Section 2 presents a natural extension of CC languages in this context, namely Linear CC (LCC) where the constraint system is axiomatized in linear logic. LCC is an extension of CC, somewhat similar to 3] or 33], but where constraints are consumed by ask agents without dependency maintenance or recomputation. Linear constraint systems have also been proposed in 34] in a higher-order setting which will not be considered here. From an operational point of view, LCC extends CC in a fundamental way by introducing some forms of imperative programming, particularly useful for reactive systems. Standard CC programs can however be recovered by the usual translation of intuitionistic logic into linear logic 10].

Section 3 settles the basic soundness and completeness results of CC and LCC operational semantics w.r.t. intuitionistic linear logic, relying on 30] and preliminary results from 29]. Results similar to those of this section are part of the folklore on CC languages [START_REF] Lincoln | Decision problems for propositional linear logic[END_REF][START_REF] Saraswat | Defaut timed concurrent constraint programming[END_REF] but have not been published. Here we prove that 1) the stores of CC computations can be characterized in intuitionistic logic, and 2) both the stores and the successes of CC and LCC computations can be characterized in intuitionistic linear logic. Completeness results show that ILL can be used to prove liveness properties of LCC programs, i.e. properties expressing that something good will eventually happen. This is developed for both \may" and \must" properties.

Then we show in section 4.2 how safety properties of CC and LCC programs (i.e. that some derivations never happen) can be proved using the phase semantics of linear logic. The method relies on the soundness theorem of LCC computations w.r.t. linear logic, and on the soundness theorem of linear logic w.r.t. the phase semantics. Completeness results simply say in this context that for various classes of observable properties of the program, if the property holds then such a \phase semantical proof" exists. The method is illustrated with several examples of LCC programs for protocol speci cations.

Related work.

The connection between CC languages and linear logic is based on the logic programming paradigm in a broad sense, that identi es programs-as-formulas and execution-as-proof-search. This paradigm was applied to linear logic with the notion of uniform proofs [START_REF] Mcdowell | Encoding transition systems in sequent calculus[END_REF]12] and focusing proofs 1], and further works on the design of concurrent languages based on proof search in LL 16,[START_REF] Okada | Completeness proofs for linear logic based on the proof search method[END_REF].

However our approach is analytical in that we study an existing programming language CC, and model CC computations in a fragment of LL. On the other hand we model properties of in nite CC computations through the observation of accessible stores which has no counterpart in the uniform proofs approach. Therefore both series of results are quite di erent.

In 22] it is shown how intuitionistic logic and linear logic can be used to encode transition systems in various ways. Particularly interesting is the augmentation of these logics with a proof theoretical treatment of de nitions that makes it possible to reason about both \may" properties and \must" properties in a symetrical way within a single translation of programs.

We shall not adopt this approach however, in order to stay in the framework of intuitionistic and linear theories.

Recently, phase semantics has gained interest in its applications to cut elimination 25], complexity of provability and decidability 17] (see 18] for a survey). Section 4.2 presents a new eld of application of the phase semantics, yet unexplored though quite natural in the paradigm of concurrent logic programming.

CC operational semantics

In this paper, a set of variables is denoted by X, Y ,..., the set of free variables occurring in a formula A is denoted by fv(A), a sequence of variables is denoted by x, A t=x] denotes the formula A in which the free occurrences of variables x have been replaced by terms t (with the usual renaming of bound variables for avoiding variable clashes).

For a set S, S ? denotes the set of nite sequences of elements in S. For a transition relation !, ! ? denotes the transitive and re exive closure of !.

CC

De nition 2.1 (Intuitionistic constraint system) A constraint system is a pair (C; `C), where:

C is a set of formulas (the constraints) built from a set V of variables, a set of function and relation symbols, with logical operators: 1 (true), the conjunction ^and the existential quanti er 9; C is assumed to be closed by renaming, conjunction and existential quanti cation;

C is a subset of C C, which de nes the non-logical axioms of the constraint system. Instead of (c; d) 2 C , we write c C d. `C is the least subset of C ? C containing C and closed by the rules of intuitionistic logic (IL) for 1, ^and 9:

; c `c ; c `d `c `d `1 `c ; 1 `c ; d; d `c ; d `c `c ; d `c `c `9xc ; c `d x 6 2 fv( ; d) ; 9xc `d `c1 `c2 `c1 ^c2 ; c 1 `c ; c 1 ^c2 `c ; c 2 `c ; c 1 ^c2 `c
In the following, c; d; e : : : will denote constraints. Note that the intuitionistic logical framework (rather than the classical one) is not essential, it is simply su cient, taking into account that the constraints are only built from conjunctions and existential quanti cations.

De nition 2.2 (Agents) The syntax of CC agents is given by the following grammar: A ::= p(x) j tell(c) j (A k A) j A + A j 9xA j 8x(c ! A) where k stands for parallel composition, + for non-deterministic choice, 9 for variable hiding and ! for blocking ask. The atomic agents p(x) : : : are called process calls or procedure calls, we assume that the arguments in the sequence x are all distinct variables.

Traditionally, the ask agents in CC are not written with a universal quanti er 32]. The reason is perhaps that in the Herbrand domain, a CC(H) ask agent, like for example 8y; z(x = y; z] ! A(x; y; z)) for decomposing a list x, can be written without a universal quanti er, by duplicating the constraint in the guard and in the body of the ask: (9y; z x = yjz]) ! 9y; z (tell(x = yjz]) k A(x; y; z)). This programming trick is rather cumbersome however and does not generalize to every constraint domain nor to linear constraint systems. Therefore we shall not adopt it in this paper, and we shall make explicit the universal quanti cation of variables in ask agents.

Recursion is obtained by declarations:

De nition 2.3 (Declarations) The syntax of declarations is given by the following grammar: D ::= j p(x) = A j D; D The set of declarations of a CC program, denoted by D, is the closure by variable renaming of a set of declarations given for distinct procedure names p.

De nition 2.4 (Programs) A program D:A is a declaration D together with an initial agent A.

CC programs are parameterized by a constraint system. In general the constraint system C will be implicit in our presentation, both in the transition system and the constraint entailment relation. Similarly the set of declarations D will be kept implicit.

We make the usual hypothesis that in a declaration p(x) = A, all the free variables occurring in A occur in x. Notice that this is exactly the meaning associated with the Horn clauses in the logic programming languages: the local variables in a clause, that are free in the body but have no occurrence in the head, are considered (implicitly in the syntax, explicitly in the semantics) as existentially quanti ed in the body (because they are universally quanti ed in the clause).

For example, a Prolog-like program for concatenating two lists L1 and L2 in L3 will be written with the CC(H) declaration (over the Herbrand constraint system) append(L1; L2; L3) = (tell(L1 = ]) k tell(L2 = L3))+ 9E; L; R(tell(L1 = EjL]) k tell(L3 = EjR]) k append(L; L2; R)) while a directional program for concatening two input lists L1 and L2 into an output list L3 will be written in CC(H) with the declaration app(L1; L2; L3) = (L1 = ] ! tell(L2 = L3))+ 8E; L(L1 = EjL] ! 9R(tell(L3 = EjR]) k app(L; L2; R)))

The operational semantics is de ned on con gurations (rather than agents) where the store is distinguished from agents: De nition 2.5 (Con gurations) A con guration is a triple (X; c; A), where c is a constraint called the store, A is an agent or ; if empty, and X is a set of variables, called the hidden variables of c and A.

The operational semantics is de ned by a transition system which does not take into account speci c evaluation strategies. The transitions system is given in the style of the CHAM 2] (see also 28]). We thus distinguish a congruence relation between syntactic elements from the very transition relation between con gurations.

De nition 2.6 (Congruence) The structural congruence is the least congruence satisfying the rules of table 1.

C-Equivalence

c a`C d c d -Conversion z 6 2 fv(A) 9yA 9zA z=y] Parallel composition A k B B k A A k (B k C) (A k B) k C Table 1: Structural congruence
The axioms of associativity and commutativity for parallel composition provide agents with a structure of multiset. From now on, by a slight abuse of notation, we will identify the agent of a con guration to the multiset of its subagents in parallel composition. We will write ; ; :::

for multisets of agents in con gurations. Congruence is extended to multisets of agents in the obvious way: 0 i = fA 1 ; : : : ; A n g, 0 = fA 0 1 ; : : : ; A 0 n g and 8i = 1; : : : ; n, A i A 0 i . Two con gurations are said congruent, (X; c; ) (X 0 ; c 0 ; 0 ), when the sets X and X 0 are equal, the constraints c and c 0 are C-equivalent, and the multisets of agents and 0 are congruent. The agents and declarations without + and 8 are called deterministic. This name is justi ed by the following proposition: Proposition 2.9 (Con uence 35]) For any deterministic con guration with deterministic declarations, if ! CC 1 and ! CC 2 , then there exists a deterministic con guration 0 such that 1 ! CC 0 and 2 ! CC 0 .

Another property of CC programs is that the execution is extensive (constraints are only added to the store during execution) and monotonic: Proposition 2. As usual, the precise operational semantics depends on the choice of observables. We shall consider accessible stores, success stores and suspensions: De nition 2.12 (Observables) The store of a con guration (X; c; ) is the constraint 9Xc. We will say that 9Xd is an accessible store from the agent A and the initial store c, if there exists a multiset of formulas such that (;; c; A) ! CC (X; d; ).

A success store (resp. a success) for an agent A and an initial store c is a constraint 9Xd (resp. a con guration (X; d; ;)) such that (;; c; A) ! CC (X; d; ;).

A terminal con guration for A and initial store c is a con guration (X; d; d 1 ! A 1 ; : : : ; d n ! A n ) such that n 0, (;; c; A) ! CC (X; d; d 1 ! A 1 ; : : : ; d n ! A n ) and for no i, d `C d i . The store 9Xd is called a suspension if the con guration isn't a success (i.e. n > 0).

It is easy to see that, by the monotonicity and extensivity properties of CC programs, the operational behavior of CC programs under these observables is completely characterized by their behavior on agents with an empty initial store. Namely the accessible stores from A with initial store c are the conjunctions of c and of the accessible stores from A k (tell c) with the empty initial store (prop. 2.11), the success stores from A with c are the success stores of A k tell(c) with the empty initial store, and similarly for suspensions. Therefore the operational semantics can be de ned with the empty initial store (i.e. the constraint true noted 1):

De nition 2.13 (Operational semantics)

O store CC (C; D:A) = f9Xd 2 C j for some con guration ; (;; 1; A) ! CC (X; d; )g O term CC (C; D:A) = f9Xd 2 C j for some ; (;; 1; A) ! CC (X; d; ) 6 ! CC g O success CC (C; D:A) = f9Xd 2 C j (;; 1; A) ! CC (X; d; ;)g Remark on non-determinism.

In the transition system, we have adopted the blind-choice rule: the non-deterministic agent A + B can behave either like A or like B. Replacing the blind choice rule (also called "internal choice") by the rules for the one-step guarded choice (also called "external choice"): whereas the second derivation is not accepted by the one-step choice. It is worth noting however that the set of successes, as well as the set of accessible stores remain the same under both interpretations. For the sake of simplicity we have not explicitly treated here all forms of nondeterminism, but the results presented in this paper remain valid as long as only accessible stores and successes are observed.

Proposition 2.14 Let O store CC 0 and O success CC 0 denote the operational semantics de ned above with the one-step guarded choice rules instead of the blind choice rules. Let A be a CC agent, we have:

O store CC (C; D:A) = O store CC 0 (C; D:A) and O success CC (C; D:A) = O success CC 0 (C; D:A) Proof. Obvious induction: let ! CC 0 be the transition relation with the one-step guarded choice rules, consider a ! CC derivation, it diverges from a ! CC 0 derivation when it stops after a transition with the blind choice rule, but then: 1) the observed store has not changed, and 2) the terminal con guration is not a success.

The monotonicity and extensivity properties provide CC with a denotational semantics, where the agents are seen as closure operators on the semi-lattice of constraints [START_REF] Saraswat | Higher-order linear concurrent constraint programming[END_REF][START_REF] Ja | Constraint logic programming: a survey[END_REF]. In this paper however, we shall also be concerned with a variant of CC languages where constraints are formulas in linear logic 10] and where extensivity is dropped.

Linear CC

Roughly speaking, there are two reasons to consider linear constraints:

{ on one hand, as we shall see in section 3.2, linear logic enables the characterization of ner observables than intuitionistic logic, and is therefore a natural semantics for CC;

{ on the other hand, variants of CC, where the constraints can be consumed by ask agents and thus removed from the store, have been introduced by Saraswat and Lincoln 34], then further studied in 3, 38]: these variants enhance signi cantly the expressive power of CC (see the examples of communication protocol programs in section 2.2.3) and the constraints are naturally modeled as formulas of linear logic.

In this section we present such a version, LCC, and give a translation from CC into LCC respecting the transition system, so that LCC is a re nement of CC, and the logical characterization that we will make on the operational behavior of LCC is also correct for CC.

Syntax

As for CC, we de ne the constraint systems, the agents, the con gurations and the transition system. The essential di erence with CC is that constraints are formulas of linear logic and that communication (the ask rule) consumes information.

De nition 2.15 (Linear constraint system) A linear constraint system is a pair (C; `C), where:

C is a set of formulas (the linear constraints) built from a set V of variables, a set of function and relation symbols, with logical operators: the multiplicative conjunction , its neutral element 1, the existential quanti er 9, the exponential connective ! and the constant >;

C is a subset of C C which de nes the non-logical axioms of the constraint system. `C is the least subset of C ? C containing C and closed by the following rules (fv(A) denotes the set of free variables occurring in A):

c `c ; c `d `c ; `d `1 `> `c ; 1 `c ; c 1 ; c 2 `c ; c 1 c 2 `c `c1 `c2 ; `c1 c 2 `c t=x] `9xc ; c `d x 6 2 fv( ; d) ; 9xc `d ; c `d ; !c `d ! `d ! `!d `d ; !c `d ; !c; !c `d ; !c `d
These are the rules of intuitionistic linear logic (ILL) for 1, , 9 and ! (see appendix A).

Note that the intuitionistic constraint systems of the previous section can be recovered by writing all constraints under a !, as in the usual translation of intuitionistic logic into linear logic 10]. We have chosen to limit the use of ! to constraints only, because the usual replication operator of process calculi (like the -calculus 24], where it is also noted !) does not have the same behavior as the exponential connective: it allows replication (!A ! LCC (!A k!A)) but not erasing (!A 6 ! LCC ;).

In general, linear constraints are not erasable in the sense that d 6 `1. One de nes the following subsumption preorder between linear constraints:

De nition 2. [START_REF] Jagadeesan | Angelic non-determinism in concurrent constraint programming[END_REF] The subsumption preorder > is de ned by: c > d i c `C d >.

Recall that > is the additive true constant which is neutral for & (see the appendix), the axiom for > is `>, hence c > d i there exists some formula A s.t. c `C d A.

The de nition of LCC agents, declarations and con gurations is the same as in CC (section 2.1), and we assume again very naturally that in a declaration p(x) = A, all the free variables occurring in A have a free occurrence in p(x), and that in a relation c C d, all the free variables occurring in d have a free occurrence in c.

De nition 2.17 The structural congruence is the same as for CC (De nition 2.7). The transition relation ! LCC is de ned by the same rules as for CC (De nition 2.7), except for LinearTell and LinearAsk which replace Tell and Ask: The calculus is intrinsically non-deterministic, even without the choice operator + nor the 8, since several constraints can satisfy the condition of the LinearAsk rule with di erent residual stores for d. Of particular interest in this context are the synchronization constraints which are roughly linear atomic constraints without non logical axioms 31]. An ask with a synchronization constraint without 8 amounts to simple multiset manipulations and is thus deterministic. We shall see examples of this in section 2.2.3 with communication protocol programs.

Because constraints are linear formulas, we must slightly modify the de nition of terminal stores and suspensions.

De nition 2.18 (Observables) The successes are de ned as in CC.

A store accessible from A and the initial store c is a constraint e such that there exist a constraint d and a multiset of agents such that (;; c; A) ! LCC (;; d; ) and d > e.

A terminal store for A with initial store c is a con guration (X; d; d 1 ! A 1 ; : : : , d n ! A n ) such that n 0, (;; c; A) ! LCC (X; d; d 1 ! A 1 ; : : : ; d n ! A n ) and for no i, d > d i . The store 9Xd is called a suspension if the con guration isn't a success (i.e. if n > 0).

An agent A with initial store c suspends with the store d on the constraints d 1 ; :::; d n , if there exist a suspension for A and c of the form (X; d; d 1 ! A 1 ; : : : ; d n ! A n ).

One major breakthrough in the expressive power of LCC is due to the loss of extensivity, i.e. the ability to express by LCC agents non monotonic evolutions of the store, where constraints can be added and then consumed by linear ask operations. It is worth noting however that the monotonicity of transitions is still preserved in LCC: Proposition 2.19 (Monotonicity) If (X; c; ) ! LCC (Y ; d; ), then for every multiset of agents and every constraint e with fv(e; ) \ (Y fv(d; ) X fv(c; ), (X; c e; ; ) ! LCC (Y ; d e; ; ). As in the previous section, the observable properties of LCC computations from an empty initial store su ce to recover the properties of LCC computations from an arbitrary initial store. The argument is the same for the observation of successes and terminal stores, but is somewhat more tricky for the observation of accessible stores1 : Proposition 2.20 Let C be a constraint system, and C 0 be the constraint system obtained by adding a new constraint token d to C. The LCC languages are a re nement of usual CC languages. Indeed the extensivity of CC can simply be restored with the exponential connective ! of linear logic, allowing replication of hypotheses and thus avoiding constraint consumption during an application of the ask rule:

De nition 2.22 Let (C; C ) be a constraint system. We de ne the translation of (C; C ), which is the linear constraint system (C ; C ), as follows, at the same time as the translation of CC agents to LCC agents:

c =!c, if c is an atomic constraint (c ^d) = c d (9xc) = 9xc tell(c) = tell(c ) p(x) = p(x) (A k B) = A k B (A + B) = A + B (8x(c ! A)) = 8x(c ! A ) (9xA) = 9xA C = fc j c 2 Cg.
The entailment relation C is de ned by: c C d i c C d .

The relation `C is obtained from C by the rules of linear logic for 1, !, and 9.

The translation of a CC con guration (X; c; ) is the LCC con guration (X; c ; ).

For constraints, the above translation is a well-known translation of intuitionistic logic into linear logic 10, p.81], hence: The above translation is correct w.r.t. the observation of the stores and of the successes of a CC computation (case (i) and (ii) of the proposition 2.24).

Example of LCC program

A classical benchmark of expressiveness for concurrent languages is the dining philosophers: N philosophers are sitting around a table and alternate thinking and eating. Each one of them has a fork on his right, and thus also on his left, and needs these two forks to eat (the chop-sticks version may be more realistic).

As suggested in 3], this problem has an extremely simple solution in LCC.

The atomic constraints are: fork(I), eat(I,N) for I,N2 N, and N=M, N6 =M for N,M 2 N. The linear constraint system in this example is thus a combination of (the translation of) standard equality constraints over (N; +), and of linear constraints tokens fork and eat with no other non-logical axioms than the equality axiom schema: c(x) !(x = ỹ) c(ỹ) for any constraint predicate c. For example, an execution with initial agent init(5) will install the philosophers and the forks in parallel composition, and the (in nite) sequence of stores along an execution path will contain various eating periods for the philosophers according to the scheduling of agents in parallel composition.

It is worth noting that unlike in a classical CC program, the imperative data structures are encoded directly with linear constraints, instead of streams 32], and that unlike the Linda version of 4] there is no need for introducing \tickets", as the guard in the ask can be the tensor product of both forks. This program enjoys safety and liveness properties: two adjacent philosophers cannot eat at the same time, and at least one philosopher can eat.

A proof of safety of this program is given in section 4, using the phase semantics of linear logic.

3 Logical semantics Proof. By induction on and ! CC .

For parallel composition, -conversion and C-equivalence, it is immediate. For hiding, 9x(A ^B) a`A ^9xB and 9xA a`A if x 6 2 fv(A).

For tell, congruence and procedure calls, it is immediate.

For ask, just note that c ^8x(d

) A) `c ^A t=ỹ] if c C d t=ỹ], qed.
The converse is true for the observation of stores. Let = (X; c; ) be a deterministic CC con guration, and be a constraint or a procedure call. ! stands for:

if is a constraint: \there exists a con guration (Y ; d; ), such that 9Y d `C and ! CC (Y ; d; )", if is a procedure call: \there exists a con guration (Y ; d; ; ), such that fv( ) \ Y = ; and ! CC (Y ; d; ; )". Lemma 3.3 Let and be two deterministic CC con gurations such that y = y , and a constraint or a procedure call. ! i ! .

Proof. We prove the lemma by induction on the formula y = y .

If y = y is atomic, it is clear.

If y = y = 8x(c ) A y ), with c a constraint and A an agent, then and are necessarily both equal to (;; 1; 8x(c ! A)). Proof. We prove the result for multisets of agents. We prove that if A 1 y ; : : : ; A n y `IL(C;D) , where the A i 's are agents and is either a constraint or a procedure call, then (;; 1; A 1 ; : : : ; A n ) ! . This is su cient to conclude: indeed let (X; c; ) be a deterministic CC con guration, and be a constraint or a procedure call. Note that (X; c; ) y = 9X(tell(c) k ) y . Therefore if (X; c; ) y `IL(C;D) , then (X; 1; tell(c); )) (;; 1; 9X(tell(c) k )) ! . But (X; 1; tell(c); )) y = (X; c; )) y . So by lemma 3.3 we will conclude (X; c; )) ! .

Let us proceed by induction on a sequent calculus proof of A 1 y ; : : : ; A n y `IL(C;D) , where the A i 's are agents and is either a constraint or a procedure call. We shall consider, without loss of generality, that in the left introduction of 8 and of ) are always consecutive (if it is not the case, it is well-known that the rules can be permuted to obtain such a proof, see for instance 9]) we will thus group them as a single rule. First remark that this induction is meaningful. Indeed the only cuts which cannot be eliminated in a proof by the cut-elimination theorem of intuitionistic logic bear on non-logical axioms, so that they are of one of the following forms: `p p ` ` `e e `f `f p ` ; ` ; p ` e `f ; f ` ; e ` Hence the application of the cut rule introduces sequents in which the new formula on the right is always either a constraint or a procedure call. On the other hand the formulas to the left remain sub-formulas of translations of agents or constraints or procedure calls, so they are agents. (Note that the induction hypothesis requires the result not only for constraints, but also for procedure calls.)

Each logical rule simulates a CC transition rule.

is an axiom: one uses the re exivity of ! CC in the case of a logical axiom, the rule procedure calls for an axiom p `q; the case of an axiom d `C e is trivial. ends with a cut: the possible cases are the ones enumerated above. Let The other case, when p is a constraint, is immediate. The other cases, where the axiom is the left premise, are similar.

ends with a left introduction of 1: note that (;; 1; ; tell(1)) ! CC (;; 1; ). By induction hypothesis, (;; 1; ) ! thus (;; 1; ; tell(1) ! , qed. ends with a weakening: y ` y ; A y ` By induction hypothesis, (;; 1; ) ! , thus (;; 1; A; ) ! thanks to the monotonicity of ! CC (proposition 2.11). ends with a contraction: y ; A y ; A y ` y ; A y ` By induction hypothesis, (;; 1; A; A; ) ! . In this sequence of transitions, some steps activate some occurrence of A, some others activate a sub-agent of . The important point is that for the deterministic agent A, the next transition in which it can further be active (in other words the next action that it can perform) is determined (no +). One can thus assume that in the above execution, each time one activates a sub-agent of an occurrence of A, the same transition with the other occurrence is performed just the next moment, it is of course possible thanks to proposition 2.9. Now starting from the con guration (;; 1; A; ), one simulates the above execution by applying the same transitions to subagents of and \contracting" the pairs of transitions for the sub-agents of A: one applies the rule to one of the two copies, always the same one. One then obtains an execution (;; 1; A; ) ! . ends with: y ; A y ; B y ` y ; A y ^By ` By induction hypothesis, (;; 1; A; B; ) ! . If A y and B y are constraints, there is a priori an ambiguity regarding the agent C whose translation is A y ^By : C can be tell(A ^B) or tell(A) k tell(B)). However, as the two con gurations have the same translation as (;; 1; A; B; ), according to lemma 3.3, (;; 1; C; ) ! . ends with: y ` y ` y ; y ` ^ ^ is not atomic, so and are constraints. The result is now immediate: starting from the con guration (;; 1; ; ), one just joins the two executions (;; 1; ) ! and (;; 1; ) ! end to end.

ends with a right introduction of 9 (in case is a constraint): immediate.

ends with:

y ; A y ` x 6 2 fv( ; ) y ; 9xA y ` By induction hypothesis, (;; 1; A; ) ! . As x 6 2 fv( ), (;; 1; 9xA; ) (fxg; 1; A; ), and moreover x 6 2 fv( ), so by lemma 3.3, (;; 1; 9xA; ) ! , qed. ends with (thanks to the preliminary remark on the permutability of rules): y ; A y t=x] ` y `c t=x] y ; y ; c t=x] ) A y t=x] ` y ; y ; 8x(c ) A y ) ` L store (C; D:A) = # O store CC (C; D:A) Proof. One inclusion is obvious by applying the previous theorem, it is just the de nition of an accessible store, the other is a direct consequence of theorem 3.2.

The characterization of stores for non-deterministic con gurations is not obvious in the framework of intuitionistic logic: indeed on one hand the simple idea of translating the choice operator + by disjunction _ requires to modify the operational semantics of + (e.g. for soundness, because A _ B 6 `A), and on the other hand the idea of translating + by conjunction preserves the soundness, but not the characterization of stores because, for instance, the store c ^d is not accessible from the con guration (;; 1; tell(c) + tell(d)).

It is possible for the observation of some must properties, i.e. properties that are true in all possible non-deterministic con gurations, like the stores entailed in all branches of the computation, as shown here in theorem 3.15. However we shall see in the next section in the more general framework of linear CC that a logical characterization of both must and may properties is possible in linear logic w.r.t. both successes and accessible stores.

Characterizing CC and LCC stores and successes in intuitionistic linear logic

The observation of stores is important, however it represents only one aspect of the operational behavior of CC programs. Consider the following three programs :

p(x) = x 1 p(x) = x 1 k p(x) p(x) = x 1 k (false ! A):
They de ne the same stores (x 1), thus they are equivalent w.r.t. the observation of stores, whereas the rst one terminates on a success, the second one loops and the third one suspends.

As is shown by the following counter-examples, neither the successes nor the suspensions are characterizable in intuitionistic logic: a: In general it is false that A a B (where B is a success store or a suspension) implies (;; 1; A) ! LCC (;; 1; B). The obstacle is the structural rule of (left) weakening: `B ; A `B Girard's linear logic 10] is a re nement of the contraction and weakening rules of usual logic. It seems therefore natural to interpret CC programs in linear logic.

Let us x a linear constraint system (C; C ) and a set of declarations D. De nition 3.6 LCC agents are translated into linear logic formulas in the following way:

tell(c) z = c p(x) z = p(x) 8ỹ(c ! A) z = 8ỹ (c ( A z ) (A k B) z = A z B z (A + B) z = A z & B z (9xA) z = 9xA z
If is the multiset of agents (A 1 : : : A n ), de ne z = A z 1 A z n . If = ; then z = 1. The translation (X; c; ) z of a con guration is the formula 9X(c z ). Conversely, one can characterize the observation of successes, even in presence of the operator of explicit choice +: Notation: Let = (X; c; ) be an LCC con guration, and be a constraint or a procedure call. o ! Proof. Again the proof is essentially the same as in intuitionistic logic, the di erence between and amounts to non performed tell's, or to tell(c d) vs tell(c) k tell(d). Lemma 3.9 Let (;; 1; ) be an LCC con guration and be a constraint or a procedure call such that (;; 1; ) o ! . Let x be a variable such that x 6 2 fv( ), then (fxg; 1; ) o ! Proof. Let be the agents obtained by replacing all existentially quanti ed occurrences of x in by a fresh variable z. We have (;; 1; ) (;; 1; ) thus (;; 1; ) o ! .

If is a constraint then (;; 1; ) ! (Y ; d; ;) with 9Y d `C . One can then show by an easy induction on this derivation that (fxg; 1; ) ! (fxg Y ; d; ;) (the only non-trivial case is the use of the Hiding rule, but as x has no bounded occurrence in , the same rule can be used in the derivation for (fxg Y ; d; ;)). As x 6 2 fv( ) we get 9x9Y d `C so (fxg; 1; ) o ! . If is a procedure call we also get (fxg; 1; ) o ! in the same manner. The result then follows from the observation that (fxg; 1; ) (fxg; 1; ).

Lemma 3.10 Let = (X; c; ) be an LCC con guration, and be a constraint or a procedure call.

If z `ILL(C;D) , then o ! .

Proof. The result is proved for multisets of agents:

if A 1 z ; : : : ; A n z `ILL(C;D) , then (;; 1; A 1 ; : : :

; A n ) o ! .
This is su cient to conclude: indeed let (X; c; ) be a con guration, and be a constraint or a procedure call. Note that (X; c; ) z = 9X(tell(c) k ) z . Therefore if (X; c; ) z `ILL(C;D) , then (X; 1; tell(c); )) (;; 1; 9X(tell(c) k )) o ! . But (X; 1; tell(c); )) z = (X; c; )) z . So according to lemma 3.8, (X; c; ) o ! .

The proof proceeds by induction on a sequent calculus proof of A z 1 ; : : : ; A z n ` . We shall consider, without loss of generality, that in the left introduction of 8 and of ( are always consecutive (if it is not the case, the rules can be permuted to obtain such a proof, see for instance 20], noting that !, that is the only case of unpermutability with 8, appears only in the constraint part and thus not below a (), we will thus group them as a single rule, so that each logical rule simulates an LCC transition rule.

is an axiom: one uses the re exivity of ! in the case of a logical axiom, the rule for procedure calls for an axiom p `q; the case of an axiom d `C e is trivial.

ends with a cut. The only cuts which cannot be eliminated in a proof by the cut elimination theorem of linear logic bear on non-logical axioms, let us consider for instance a cut with procedure declaration: By induction hypothesis, (;; 1; ) o ! p, i.e. there exists a con guration (Y ; d; p) such that fv(p) \ Y = ;, 9Y d `C 1 and (;; 1; ) ! (Y ; d; p). Thus (;; 1; ) ! (Y ; d; ); fv( ) \ Y = ; as fv( ) fv(p). If is a procedure call, it is nished. If is a constraint c, then (;; 1; ) ! (Y ; d c; ;), fv(c) \ Y = ; and 9Y d c `C c, qed.

The other case, when p is a constraint, is immediate. The other cases, where the axiom is the left premise, are similar. ends with a left introduction of 1: note that (;; 1; ; tell(1)) ! (;; 1; ). By induction hypothesis, (;; 1; ) o ! thus (;; 1; ; tell(1)) o ! , qed. ends with: z ; A z ; B z ` z ; A z B z ` By induction hypothesis, (;; 1; A; B; ) o ! . If A z and B z are constraints, there is a priori an ambiguity on the agent C whose translation is A z B z : it can be tell(A B) or tell(A) k tell(B)). However, as the two con gurations have the same translation as (;; 1; A; B; ), according to lemma 3.8, (;; 1; C; ) o ! . ends with: z ` z ` z ; z ` is not atomic, so and are constraints. The result is now immediate: starting from the con guration (;; 1; ; ), one just joins the two executions (;; 1; ) o ! and (;; 1; ) o ! end to end. ends with: z ; A z ` z ; A z & B z ` By induction hypothesis, (;; 1; A; ) o ! , Now (;; 1; A+B; ) ! (;; 1; A; ), therefore (;; 1; A + B; ) o ! . ends with a right introduction of 9 (in case is a constraint): immediate. ends with: z ; A z ` z ; 9xA z ` x 6 2 fv( ; ) By induction hypothesis, (;; 1; A; ) o ! . As x 6 2 fv( ), (;; 1; 9xA; ) ! (fxg; 1; A; ), and moreover x 6 2 fv( ), so by lemma 3.9, (;; 1; 9xA; ) o ! , qed. ends with (thanks to the preliminary remark on the permutability of rules): z ; A z t=x] ` z `c t=x] z ; z ; (c t=x] ( A z t=x]) ` z ; z ; 8x(c ( A z ) `

; c ` z ; !c ` It is clear, just recall that !c `c.
ends with a promotion: in that case all the formulas are necessarily constraints, therefore it is immediate.

ends with a weakening: z ` z ; !c ` with c a constraint. By induction hypothesis, (;; 1; ) o ! , so (;; 1; tell(!c); ) o ! (one performs the tell, noting that !c `C 1). ends with a contraction: Let, for a set S of linear constraints, + S = fc 2 C j 9d 2 S; d > cg.

Theorem 3.12 (Observation of stores) Let A be an LCC agent and c be a linear constraint. De ne LL store (C; D:A) = fc 2 CjA z `ILL(C;D) c >g. We have LL store (C; D:A) =+ O store LCC (C; D:A): Proof. Simply use theorem 3.11, above the right introduction of the tensor connective in c > and note that the property is preserved by left introduction rules.

Thanks to the translation of CC into LCC (proposition 2.24), this characterization of stores and successes in linear logic holds also for CC.

Must properties

So far we have been concerned with \May" properties of LCC programs, i.e. properties that stand for some branch of the derivation tree. \Must" properties, i.e. properties that are true on all branches of the derivation tree, are also to be considered, for instance when looking at liveness properties. We show that \must" stores and \must" successes can be characterized logically using disjunction. The operational semantics has to be adapted to multisets of con gurations, called frontiers, which keep track of all the alternatives in the derivation tree. For the sake of simplicity however, we will not handle the possible source of non-determinism due to the (linear) ask operations with the universal quanti er. The \must" properties modelized in this section are thus relative to the choice operator not to the indeterminism coming from the linear ask (which can be made deterministic as remarked above if only classical and synchronization constraints are used in guards).

Frontier calculus

A frontier is a multiset of con gurations, noted h 1 ; ; n i where each i is a con guration (X i ; c i ; i ). The structural congruence on con gurations is kept unchanged. The transition relation ! LCC is extended to a transition relation =) LCC on frontiers in the obvious way, the only di erence being for the non-deterministic choice. The frontier transition relation =) LCC is de ned as the least relation satisfying the rules in table 3. LinearTell h(X; c; tell(d); ); i =) LCC h(X; c d; ); i LinearAsk c `C d e t=ỹ] h(X; c; 8ỹ(e ! A); ); i =) LCC h(X; d; A t=ỹ]; ); i Procedure calls (p(ỹ) = A) 2 P h(X; c; p(ỹ); ); i =) LCC h(X; c; A; ); i (X; c; ) (X 0 ; c 0 ; 0 ) =) LCC (Y 0 ; d 0 ; 0 ) (Y ; d; ) h(X; c; ); i =) LCC h(Y ; d; ); i Blind choice h(X; c; A + B; ); i =) LCC h(X; c; A; ); (X; c; B; ); i Compared to lemma 3.4, there is just an additional induction step: yy ; A yy ` yy ; B yy ` yy ; A yy _ B yy ` By induction hypothesis, (;; 1; A; ) =) and (;; 1; B; ) =) . Now (;; 1; A + B; ) =) h(;; 1; A; ); (;; 1; B; )i, and therefore (;; 1; A + B; ) =) , qed.

As usual, the other inclusion is a direct consequence of the soundness theorem. Theorem 3.16 (Observation of frontier stores and successes in ILL) Let A be an LCC agent de ne LL 00 store (C; D:A) = fc 2 C j A zz `ILL(C;D) c >g and LL 00 success (C; D:A) = fc 2 C j A zz `ILL(C;D) cg we have: LL 00 store (C; D:A) =+ O store LCC 00 (C; D:A) LL 00 success (C; D:A) =# O success LCC 00 (C; D:A) Proof. For the rst inclusion, we rst prove the result for successes, for stores we apply the same argument as in the proof of theorem 3.12. Proceed by induction on a proof of A zz `ILL(C;D) c as in lemma 3.10. The only di erence with the proof of lemma 3.10 is the following induction step: Phase semantics is the natural provability semantics of linear logic 10]. It will also be useful for proving safety properties of CC programs, through the links between linear logic and CC. We only need here a fragment of intuitionistic linear logic ( , & and (, which correspond respectively to the parallel, choice and blocking ask operators, as shown in section 3.2). Nevertheless it is simpler to recall Okada's de nition of the phase semantics for full intuitionistic LL 25] and to extend it to constants (1, 0, >).

The de nition of formulas and the sequent calculus are recalled in appendix A.

De nition 4.1 A phase space P = (P; ; 1; F) is a commutative monoid (P; ; 1) together with a set F of subsets of P, whose elements are called facts, satisfying the following closure properties: { F is closed under arbitrary intersection, { for all A P, for all F 2 F, the set fx 2 P : 8a 2 A; a x 2 Fg is a fact of F, noted A ( F.

As we shall see, facts correspond to ILL formulas and thus to LCC agents (cf. section 3.2).

Note that facts are closed under linear implication (. Here are a few noticeable facts: the greatest fact > = P, the smallest fact 0, and 1= T fF 2 F : 1 2 Fg.

A parametric fact A is a total function from V to F assigning to each variable x a fact A(x).

Any fact can be seen as a constant parametric fact, and any operation de ned on facts can be extended to parametric facts: (A ? B)(x) = A(x) ? B(x).

Let A; B be (parametric) facts, de ne the following facts: 9 a phase space P, a valuation , and an element a 2 ((X; c; ) y ) such that a 6 2 ((Y ; d; ) y ):

A & B = A \ B; A B = \ fF 2 F : A B Fg; A B = \ fF 2 F : A B Fg; 9xA = \ fF 2 F : ( x2V A (
This proposition allows to reduce the problem of proving safety properties of CC programs, i.e. proving the non-existence of some derivation, to an existence problem: nding a phase structure, an interpretation and a counter-example for the above inclusion, or even, only proving their existence. Note that only soundness theorems are used, the second part of the correspondence (completeness) gives a certain certitude that when looking for a semantical proof of a true safety property, it exists!

Example 1 -Dining philosophers

As shown in section 2.2 the dining philosophers problem can easily be encoded in LCC. Let us try to prove, for instance, that this encoding satis es the safety property that it does not allow two philosophers to eat with the same fork at the same time, independently of the number of philosophers.

i) Reformulating the property. We rst have to express that we don't want two neighbors to eat together in a safety property of the above form: 8N; 8I; 8c; 8A; (;; 1; init(N)) Y ! LCC (;; eat(I); eat(I+1 mod N); c; A)

From the corollary, it is enough to show: 8N; 8I; 9P; 9 ; 9x 2 (init(N)); x 6 2 (eat(I) eat(I+1 mod N) >) iv) Counter-example. As (init(N)) = fx 1;n y 1;n g we must prove: x 1;n y 1;n 6 2 (eat(I,N) eat(I+1 mod N,N) >) = fx 2 N : 9a 2 N; x = e i;n e i+1modn;n ag.

First we show by induction that: x 1;n y 1;n = f 1 : : : f n p 1 : : : p n And then proceed Ad absurdum: if x 1;n y 1;n = e i;n e i+1modn;n a then f i+1modn x 1;n y 1;n = e i;n e i+1modn;n a f i+1modn = f 1 : : : f i 1 f i+3 : : : f n p 1 : : : p i 1 p i+2 : : : p n e i;n e i+1modn;n hence, simplifying we get a f i+1modn = f 1 : : : f i 1 f i+3 : : : f n p 1 : : : p i 1 p i+2 : : : p n which is impossible (prime factors decomposition: f i+1modn appears on the left hand of = but not on the right hand, a product of prime numbers), qed.

Remark:

{ It is worth noting that, although a similar soundness theorem holds for the translation of agents into intuitionistic logic (IL), if we use that translation instead of ILL we will not be able to prove anything because from philosopher(I) ^fork(I) ^fork(I+1) `eat(I,N) and philosopher(I+1) ^fork(I+1) ^fork(I+2) `eat(I+1,N)we can infer philosopher(I)^philosopher(I+1)^fork(I)^fork(I+1)^fork(I+2) `eat(I,N)^eat(I+1,N).

{ The phase structure might seem unnatural, but in this case it can be simply considered as the free commutative monoid built on the atomic constraints of the program, interpreted as singletons, and generated by the equalities coming from the non-logical axioms (i.e. inclusions between singletons). Such a singleton-based phase structure cannot always be used however.

For instance with the following program: P = tell(d), Q = c ! P, a singleton-based phase structure does not allow one to prove that c is not accessible from P, i.e. P 6 `c >, as we can deduce (P) = c (Q) from the second declaration.

Example 2 -Producer/Consumer

The producer/consumer protocol with m producers and k consumers communicating via a bu er of size n can be encoded in LCC as follows:

P = dem ! (pro k P) C = pro ! (dem k C) init = dem n k P m k C k
Let us prove, with the same phase structure as above, that this protocol, encoded this way, is deadlock free, and safe (the number of units consumed is always less than the number of units produced).

Deadlock Freeness

The rst task is to state this safety property in the form (X; c; ) Y ! LCC (Y ; d; ). One can easily see that a deadlock may only occur if there is, either no P left, or no C left, or nothing to consume (dem and pro). i) We thus want to prove init Y ! LCC dem n 0 k P m 0 k C k 0 k pro l 0 , with either n 0 = l 0 = 0 or m 0 = 0 or k 0 = 0.

ii) Let us now consider the structure P = N, F = P(N), and O = f;; f1gg, it is obviously a phase structure.

iii) Let us de ne the following valuation:

(dem) = f5g (pro) = f5g (P) = f2g (C) = f3g (init) = f2 m 3 k 5 n g

We have to check the correctness of :

8p 1 2 (P); 9p 2 2 (P); dem p 1 = pro p 2 , hence (P) (body of P).

The same for C, and (init) = (body of init).

iv) Instead of exhibiting a counter-example, we will again prove Ab absurdum that the inclusion (init) (dem n 0 k P m 0 k C k 0 k pro l 0 ) is impossible. Suppose (init) f5 n 0 2 m 0 3 k 0 5 l 0 g Comparing the power of 5, 3 and 2, anything else than: n 0 + l 0 = n and m 0 = m and k 0 = k is impossible, and therefore if there is a deadlock (n 0 + l 0 = 0 6 = n, or m 0 = 0 6 = m, or k 0 = 0 6 = k) (init) is not a subset of its interpretation and thus init does not reduce into it, qed.

Safety

In order to check that there are never more units consumed than units produced, the encoding must be slightly modi ed to make this information directly observable: This kind of modi cation, namely adding an \oracle" to observe the property of interest, is commonly seen in other veri cation techniques, for instance when adding a separate automaton in model checking.

i) We want to prove: init Y ! LCC dem n 0 k pro l 0 k P m k C k k np=np 0 k nc=nc 0 with nc 0 > np 0 .

ii) Once again we can use a quite simple structure, P = Q; F = P(Q); O = f;; f1gg. iii) And the following valuation:

(dem) = f6g (pro) = f3g (P) = f5g (C) = f7g

(np=X) = f2 x g (nc=X) = f2 x g (init) = f2 n 3 n 5 m 7 k g This valuation is correct: 9d = 2 s.t. dem p = pro p d and 8x; 2 x d = 2 x+1 hence (P) (body of P). iv) Now, It su ces to remark that nc 0 > np 0 and (init) f6 n 0 3 l 0 5 m 7 k 2 np 0 2 nc 0 g would imply l 0 < 0, which is impossible, qed.

Example 3 -Mutual exclusion

There is no \;" (sequentiality operator) in the syntax, but it can be added without losing the soundness properties by translating it as \ " (similarly, the guarded choice can be translated as \ & "). The following example of mutual exclusion with semaphores shows an example of LCC + \;" program on which one can prove safety properties: P i = sem ! cs k A ; (cs ! sem k P i ) init = sem k P 1 k k P N i) We want to prove that the two critical sections cs cannot take place at the same time: 8B; init Y ! LCC cs k cs k B i.e. init z 6 `cs cs >.

ii, iii, iv) The structure P = N and the valuation (sem) = (cs) = (init) = f2g and (A) = (P i ) = f1g are correct. The proof of existence of a counter-example (again ab absurdum) is trivial. This handling of \;", or of the guarded choice, may be quite surprising and is of course not general. It shows that although these operators have no simple logical interpretation, it is nevertheless sometimes possible to capture their operational behavior in the statement of the property. In the previous example it was enough to show 8B; init Y ! LCC cs k cs k B because we know that A is over when we remove cs from the store; showing 8B; init Y ! LCC A k A k B would not be possible by interpreting \;" as \ ".

Conclusion and perspectives

Building upon the close correspondence between CC executions and proof search in LL, we have shown that the semantics of provability (not of proofs) in LL provides an interesting level of abstraction for reasoning about CC programs, getting rid of unnecessary execution details. In particular we have shown that various safety properties of simple protocol CC programs could be proved directly, simply by exhibiting a phase space and an interpretation of the program in which the property holds.

These results open also a lot of questions, for instance on the shape of the simplest phase spaces for proving a given safety property, and on the possibility of automating such \semantical" proofs in a somewhat similar way to model checking. Preliminary results on counter phase model generation methods can be found in 26].

The method can be generalized to handle more safety properties of LCC programs. In particular the characterization of LCC suspensions 31] in the non-commutative logic of the second author 30], can be used to prove deadlock properties using non-commutative phase spaces.

The extension { induced by the logic { of CC languages to linear constraint systems is also interesting to study in its own right as it reconciles declarative programming with some form of imperative programming. We have shown this on simple examples for protocol speci cation. As another example, the rational reconstruction of CLP(FD) constraint propagators by CC agents given in 11] can be extended in LCC to cover the propagation algorithms of global constraints which use imperative (backtrackable) data structures 36]. Such a logical reconstruction with LCC of constraint solvers can thus be more faithful to current constraint programming practice.

(

  X; c; A; ) ! CC (Y ; d; ) (X; c; A + B; ) ! CC (Y ; d; ) and (X; c; B; ) ! CC (Y ; d; ) (X; c; A + B; ) ! CC (Y ; d; ) . would obviously change the suspensions of a program. For instance, let = (;; c; (c ! tell(1))+ (d ! tell(1))) with c 6 `C d, then for the blind choice, has two possible derivations: ! CC (;; c; c ! tell(1)) ! CC (;; c; tell(1)) ! CC (;; c; ;) and ! CC (;; c; d ! tell(1)) 6 ! CC ,

  LinearTell (X; c; tell(d); ) ! LCC (X; c d; ) LinearAsk c `C d e t=ỹ] (X; c; 8ỹ(e ! A); ) ! LCC (X; d; A t=ỹ]; )

  Proposition 2.23 Let c and d be constraints in C: c`Cd i c `C d .We now check that the translations of con gurations have the expected behavior: Proposition 2.24 Let (X; c; ) and (Y ; d; ) be CC con gurations: (i) (X; c; ) (Y ; d; ) i (X; c ; ) (Y ; d ; ); (ii) if (X; c; ) ! CC (Y ; d; ) then (X; c ; ) ! LCC (Y ; d ; ); (iii) if (X; c ; ) ! LCC (Y ; d ; ) then (X; c; ) ! CC (Y ; e; ), with e `C d. Proof. (i) is evident. For (ii), we proceed by induction on ! CC , the only interesting case is the ask rule: we suppose (X; c; 8ỹ(d ! A); ) ! CC (X; c; A t=ỹ]; ); using the c `C d t=ỹ] relation. We thus have c `C c ^d t=ỹ], and from proposition 2.23, c `C (c ^d t=ỹ]) = c d t=ỹ] . As a consequence (X; c ; 8ỹ(d ! A ); ) ! LCC (X; c ; A t=ỹ]; ); qed. For (iii), we proceed by induction on ! LCC . The only interesting case is again the ask rule: we suppose (X; c ; 8ỹ(d ! A ); ) ! LCC (X; e ; A t=ỹ]; ); using the relation c `C d t=ỹ] e = (d ^e) . Thus from the proposition 2.23, c `C d t=ỹ] ^e `C d t=ỹ], hence (X; c; 8ỹ(d ! A); ) ! CC (X; c; A t=ỹ]; ); and c `C e, qed.

  mod N) ! (tell(eat(I,N)) k eat(I,N) ! (tell(fork(I) fork(I+1 mod N)) k philosopher(I,N))). recphilo(M,P) = M 6 = P ! (philosopher(M,P) k tell(fork(M)) k recphilo(M+1,P)) k M = P ! (philosopher(M,P) k tell(fork(M))). init(N) = recphilo(1,N).

3. 1

 1 Characterizing CC stores in intuitionistic logic Let us x a constraint system (C; C ) and a set of declarations D. De nition 3.1 Deterministic CC agents are translated into intuitionistic formulas in the following way: tell(c) y = c p(x) y = p(x) (9xA) y = 9xA y (8x(c ! A)) y = 8x(c ) A y ) (A k B) y = A y ^By If is the multiset of agents (A 1 : : : A n ), one de nes y = A y 1 ^ ^Ay n . If = ; then y = 1. The translation (X; c; ) y of a con guration is the formula 9X(c ^ y ). IL(C,D) denotes the deduction system obtained by adding to IL: the non-logical axiom c `d for every c C d in C , the non-logical axiom p(x) `Ay for every declaration 3 p(x) = A in D. a`denotes logical equivalence. Theorem 3.2 (Soundness) Let (X; c; ) and (Y ; d; ) be deterministic CC con gurations. If (X; c; ) (Y ; d; ) then (X; c; ) y a`I L(C;D) (Y ; d; ) y . If (X; c; ) ! CC (Y ; d; ) then (X; c; ) y `IL(C;D) (Y ; d; ) y .

  If y = y = 9xA y , then the only two possibilities for and are (fxg Y ; c; ) and (;; 1; 9x9Y (tell(c) k )). One implication is thus obvious and the other one a simple corollary of the monotonicity property 2.19.If y = y = A y ^By , then the four possibilities for and are: (;; 1; ; ) (with y = A y and y = B y ), (;; 1; A k B), (;; c; B) (if A y = c, a constraint, i.e. A = c or A = tell(c)) and (;; c ^d; ;) (if A y = c and B y = d, constraints). The induction is useful only in the rst case, and the result is evident. Lemma 3.4 Let = (X; c; ) be a deterministic CC con guration, and be a constraint or a procedure call.If y `IL(C;D) , then ! .

  For instance c ! d a d but c ! d suspends in the empty store, and thus does not reduce to the success d. In the case where B is a suspension, for instance d k (c ! d) with d not implying c, note that d a d ^(c ! d) but tell(d) doesn't reduce to that suspension. `: One has similar problems with `. We have d ^(c ) A) `d whereas d k (c ! A) suspends as soon as d 6 `c. Besides d ^(d ) e) `d ) e, but d k (d ! e) has a success (d ^e) and does not suspend. a`: Similarly, for the equivalence a`, let us suppose that d does not imply c, and let us consider the following equivalence: d^(c ) d) a`d. One cannot conclude anything about the operational behavior of the agents tell(d) and d k (c ! d).

  ILL(C,D) denotes the deduction system obtained by adding to ILL: the non-logical axiom c `d for every c C d in C , the non-logical axiom p(x) `Az for every declaration 4 p(x) = A in D. Theorem 3.7 (Soundness) Let (X; c; ) and (Y ; d; ) be LCC con gurations. If (X; c; ) (Y ; d; ) then (X; c; ) z a`I LL(C;D) (Y ; d; ) z . If (X; c; ) ! LCC (Y ; d; ) then (X; c; ) z `ILL(C;D) (Y ; d; ) z . Proof. The proof is essentially the same as in intuitionistic logic. Note that for the operator of choice + translated by the additive conjunction & , A & B `A and A & B `B.

  z ; !c; !c ` z ; !c ` with c a constraint. By induction hypothesis, (;; 1; tell(!c); tell(!c); ) o ! . Obviously having two occurrences of the agent tell(!c) changes nothing because !c !c a`!c. Therefore (;; 1; tell(!c); ) o ! holds as well. Theorem 3.11 (Observation of successes) Let A be an LCC agent and c be a linear constraint. De ne LL success (C; D:A) = fc 2 CjA z `ILL(C;D) cg. We have LL success (C; D:A) =# O success LCC (C; D:A): Proof. Evident by applying the previous lemma to the con guration (;; 1; A).

  tell(c) yy = c p(x) yy = p(x) (9xA) yy = 9xA yy (8x(c ! A)) yy = 8x(c ) A yy ) (A k B) yy = A yy ^Byy h 1 ; ; n i zz = ( 1 ) zz( n ) zz (A + B) zz = A zz B zz tell(c) zz = c p(x) zz = p(x) (9xA) zz = 9xA zz (8x(c ! A)) zz = 8x(c ( A zz ) (A k B) zz = A zz B zzThe soundness of the translation is proved by a simple induction: Theorem 3.14 (Soundness of frontier transitions) Let and be two frontiers. If =) CC then yy `IL(C;D) yy . If =) LCC then zz `ILL(C;D) zz . The converse doesn't hold in general because some logical deductions have no operational counterpart, like for example weakening in IL, or A (c ( B) `ILL c ( (A B) in ILL, see 31]. Nevertheless completeness holds for the observation of CC frontier stores in IL, and for the observation of both successes and frontier stores in ILL. Theorem 3.15 (Observation of frontier stores in IL) Let A be a CC agent, de ne L 00 store (C; D:A) = fc 2 C j A yy `IL(C;D) cg we have: L 00 store (C; D:A) =# O store CC 00 (C; D:A) Proof. One inclusion is shown by induction on a proof of A y `IL(C;D) c as in lemma 3.4.

P

  = dem ! (pro k P k 8X (np=X ! np=X+1)) C = pro ! (dem k C k 8X (nc=X ! nc=X+1)) init = dem n k P m k C k k np=0 k nc=0

  Now, for a set S of constraints, let us note # S = fc 2 C j 9d 2 S; d `C cg, we get: Theorem 3.5 (Observation of deterministic stores) Let A be a deterministic CC agent, de ne L store (C; D:A) = fc 2 C j A y `IL(C;D) cg we have:

	By induction hypothesis, (;; 1; ) ! c t=x], i.e. there exists a con guration (Y ; d; ), such that d `C c t=x] and (;; 1; ) ! CC (Y ; d; ). Thus (;; 1; 8x(c ! A); ) ! CC (Y ; d; 8x(c ! A);

) ! CC (Y ; d; A t=x]; ). Therefore, (;; 1; 8x(c ! A); ; ) ! CC (Y ; d; A t=x]; ; ). Moreover by induction hypothesis, (;; 1; A t=x]; ) ! , whence (;; 1; 8x(c ! A); ; ) ! .

  is a procedure call: \there exists a con guration (Y ; d; ), such that fv( ) \ Y = ;, 9Y d `C 1 and ! LCC (Y ; d; )".Lemma 3.8 Let and be two con gurations LCC such that z = z , and be a constraint

	or a procedure call. o ! i o ! .
	stands for:
	if is a constraint: \there exists a con guration (Y ; d; ;), such that 9Y d `C and ! LCC (Y ; d; ;)",

if

Table 3 :

 3 LCC frontier transition relationThe frontier transition relation =) CC is de ned similarly with Tell and Ask rules instead of the LinearTell and LinearAsk rules. Now the operational semantics for must properties is de ned as follows:

	De nition 3.13 (Frontier operational semantics) O store CC 00 (C; D:A) = fc 2 C j (;; 1; A) =) CC h(X 1 ; d 1 ; 1 ); ; (X n ; d n ; n )i, 9X 1 d 1 `C c; : : : ; 9X n d n `C cg O store LCC 00 (C; D:A) = fc 2 C j (;; 1; A) =) LCC h(X 1 ; d 1 ; 1 ); ; (X n ; d n ; n )i; 9X 1 d 1 `C c; : : : ; 9X n d n `C cg O success LCC 00 (C; D:A) = fc 2 C j (;; 1; A) =) LCC h(X 1 ; d 1 ; ;); ; (X n ; d n ; ;)i, 9X 1 d 1 `C c; : : : ; 9X n d n `C cg
	3.3.2 Logical semantics.
	The translation y (resp. z) of CC (resp. LCC) con gurations into intuitionistic (resp. linear) formulas is changed for disjunctive agents and extended to frontiers in the obvious way:
	h 1 ; ; n i yy = ( 1 ) yy _ _ ( n ) yy (A + B) yy = A yy _ B yy

  Proving safety properties of LCC programs with the phase semanticsUsing the phase semantics presented above we will now prove safety properties of CC programs. We use the soundness of the translation from LCC into ILL and so require, either to translate CC programs into LCC or to write programs directly in LCC.

	4.2 The theorem 4.5 of soundness of the phase semantics w.r.t. ILL is:
	`ILL A implies 8P; ; P; j = ( `A):
	It can easily be extended to ILL C;D by imposing to any valuation to satisfy the inclusions coming from the non-logical axioms (the axiom c `d imposes (c) (d)). By contrapositive we get:
	9P; ; s.t. P; 6 j = ( `A) implies 6 `ILL C;D A;
	which is equivalent to:
	9P; ; s.t. ( ) 6 (A) implies 6 `ILL C;D A:
	As the contrapositive of the theorem 3.7 of soundness from LCC to ILL C;D is:
	(X; c; )
			x)) Fg;
	8xA =	\ fF 2 F : ( x2V \	A(x)) Fg:

y 6 `ILL C;D (Y ; d; ) y implies (X; c; ) Y ! LCC (Y ; d; ) We have: Proposition 4.7 To prove a safety property of the kind: (X; c; ) Y ! LCC (Y ; d; ), it is enough to show that:

As an alternative, we could have de ned the operational semantics of LCC programs with arbitrary initial stores, the generalization of the results is straightforward.

Note that an encoding with c d instead of c d d would not allow us to decide whether 1 is an accessible store or not.

Translating CC declarations with a logical equivalence instead of an implication would preserve both soundness and completeness results of this section, but the intermediate lemmas need be generalized in order to take into account the foldings of procedure declarations (i.e. replacing a formula by the procedure it de nes) that would become possible in the logic, although they have no operational counterpart.

Here again the CC declarations could be translated with an equivalence instead of an implication without a ecting the main soundness and completeness theorems of this section.

z `p p ` z `

Acknowledgments

We are particularly grateful to Dale Miller, Catuscia Palamidessi Vijay Saraswat and Rajeev Gor e for fruitful discussions on this work, as well as to the anonymoous referees for their comments.

De nition 4.2 An enriched phase space is a phase space (P; ; 1; F) together with a subset O of F, whose elements are called open facts, such that: { O is closed under arbitrary (in particular there is a greatest open fact), { 1 is the greatest open fact, { O is closed under nite , { is idempotent on O (if A 2 O then A A = A).

!A is de ned as the greatest open fact contained in A.

The set of facts has been provided with operators corresponding to ILL connectives (and therefore to LCC operators), we now translate formulas into facts.

De nition 4.3 Given an enriched phase space, a valuation is a mapping from atomic formulas to facts such that (>) = >, (1) = 1 and (0) = 0.

The interpretation (A) (resp. ( )) of a formula A (resp. of a context ) is de ned inductively in the obvious way:

( ) = 1 if is empty: Sequents are interpreted as follows: ( `A) = ( ) ( (A). This brings one to de ning a notion of validity: De nition 4.4 (Validity) De ne: P, j = ( `A) i 1 2 ( `A), i.e. ( ) (A), P j = ( `A) i for every valuation : P, j = ( `A), j = ( `A) i for every phase space P: P j = ( `A).

This semantics of ILL formulas enjoys the following main properties: Theorem 4.5 (Soundness 10, 25]) If there is a sequent calculus proof of `A then j = ( À). where > is the usual constant of linear logic that means \anything" and so can replace c and A for any c and any A.

ii) Phase space. Consider the following structure P:

N (with it's usual product and unit) is the monoid,

It is de nitely a phase structure.

iii) Valuation. We need to de ne a valuation on fork(I), eat(I,N), N=M, N6 =M, philosopher(I,N), recphilo(M,P) and init(N). We must not forget to check that the conditions coming from the declarations (non-logical axioms which translate into compulsory inclusions) of philosopher(I,N), recphilo(M,P) and init(N) are satis ed.

Let us de ne as follows:

(fork(I)) = ff i g (eat(I,N)) = fe i;n g (philosopher(I,N)) = fp i g (recphilo(M,P)) = fx m;p y m;p g (init(N)) = fx 1;n y 1;n g

where the indices (i; m; n; p) are the canonical interpretation of the corresponding integer variables, f i and p i are distinct prime numbers, and e i ; x m;p and y m;p are de ned as follows: e i;n = f i f i+1modn p i x m;p = 1 if m = p; p m f m x m+1;p y m+1;p otherwise. y m;p = p m f m if m = p; 1 otherwise. The conditions coming from the declarations are: { 8i; fp i g E i;n where E i;n = (body of philosopher(I,N)) { 8m; 8p; fx m;p y m;p g F m;p where F m;p = (body of recphilo(M,P)) { 8n; fx 1;n y 1;n g (body of init(N)).

One can easily notice that the third condition is implied by the second one. Remembering that an agent A ! LCC B ! LCC C ! LCC D is interpreted as fx 2 N : 8y 2 (A); 8z 2 (B); 8t 2 (C); 9u 2 (D); x y z t = ug, we can deduce: E i;n = fx 2 N : 9y 2 G i;n ; f i+1modn f i x = e i;n yg with G i;n = fy 2 N : e i;n y = f i f i+1modn p i g (y represents an element of the interpretation of the part eat(I,N) ! (tell(fork(I) fork(I+1 mod N)) k philosopher(I,N)) in the I th philosopher). Now, observe that the rst condition 8i; fp i g E i;n reduces to showing that G i;n is non-empty, which is true as 1 2 G i;n . The second condition on F m;p is veri ed with a simple induction on x m;p and y m;p which have been so de ned on purpose. The valuation is thus correct.

A Appendix: Intuitionistic linear sequent calculus De nition A.1 (Intuitionistic formulas) The intuitionistic formulas are built from atoms p; q; : : : with: { the multiplicative connectives: (tensor) and implication (, { the additive connectives: & (with) and (plus), { the exponential connective ! (of course or bang), { the constants: multiplicative 1 and ?, and additive > and 0, { the quanti ers: universal 8 and existential 9. De nition A.2 (Intuitionistic sequents) The sequents are of the form `A or `, where A is a formula and is a multiset of formulas.

The sequent calculus is given by the following rules:

Axiom -Cut