Moreno Falaschi
email: moreno.falaschi@unisi.it

Carlos Olarte
email: carlosolarte@javerianacali.edu.co

Catuscia Palamidessi
email: catuscia@lix.polytechnique.fr

Interpretation of Temporal Concurrent Constraint Programs

Keywords: Timed Concurrent Constraint Programming, Process Calculi, Abstract Interpretation, Denotational Semantics, Reactive Systems

come   L'archive ouverte pluridisciplinaire

Introduction

Concurrent Constraint Programming (ccp) [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF][START_REF] Saraswat | Concurrent Constraint Programming[END_REF] has emerged as a simple but powerful paradigm for concurrency tied to logic that extends and subsumes both concurrent logic programming [START_REF] Shapiro | The family of concurrent logic programming languages[END_REF]) and constraint logic programming [START_REF] Jaffar | Constraint logic programming[END_REF]. The ccp model combines the traditional operational view of process calculi with a declarative one based upon logic. This combination allows ccp to benefit from the large body of reasoning techniques of both process calculi and logic. In fact, ccp-based calculi have successfully been used in the modeling and verification of several concurrent scenarios such as biological, security, timed, reactive and stochastic systems [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]Olarte and Valencia 2008b;Nielsen et al. 2002a;[START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF][START_REF] Jagadeesan | Timed constraint programming: a declarative approach to usage control[END_REF]) (see a survey in [START_REF] Olarte | Models and emerging trends of concurrent constraint programming[END_REF])).

In the ccp model, agents interact by telling and asking pieces of information (constraints ) on a shared store of partial information. The type of constraints that agents can tell and ask is parametric in an underlying constraint system. This makes ccp a flexible model able to adapt to different application domains.

The ccp model has been extended to consider the execution of processes along time intervals or time-units. In tccp (de Boer et al. 2000), the notion of time is identified with the time needed to ask and tell information to the store. In this model, the information in the store is carried through the time-units. On the other hand, in Timed ccp (tcc) [START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF]), stores are not automatically transferred between time-units. This way, computations during a time-unit proceed monotonically but outputs of two different time-units are not supposed to be related to each other. More precisely, computations in tcc take place in bursts of activity at a rate controlled by the environment. In this model, the environment provides a stimulus (input) in the form of a constraint. Then the system, after a finite number of internal reductions, outputs the final store (a constraint) and waits for the next interaction with the environment. This view of reactive computation is akin to synchronous languages such as Esterel [START_REF] Berry | The Esterel synchronous programming language: Design, semantics, implementation[END_REF] where the system reacts continuously with the environment at a rate controlled by the environment. Hence, these languages allow to program safety critical applications as control systems, for which it is fundamental to provide tools aiming at helping to develop correct, secure, and efficient programs.

Universal tcc (Olarte and Valencia 2008b) (utcc), adds to tcc the expressiveness needed for mobility. Here we understand mobility as the ability to communicate private names (or variables) much like in the ⇡-calculus [START_REF] Milner | A calculus of mobile processes, Parts Ia n dI I[END_REF]). Roughly, a tcc ask process when c do P executes the process P only if the constraint c can be entailed from the store. This idea is generalized in utcc by a parametric ask that executes P [ t/x] when the constraint c[ t/x] is entailed from the store. Hence the variables in x act as formal parameters of the ask operator. This simple change allowed to widen the spectrum of application of ccp-based languages to scenarios such as verification of security protocols (Olarte and Valencia 2008b) and service oriented computing [START_REF] López | Towards a unified framework for declarative structured communications[END_REF]).

Several domains and frameworks (e.g., [START_REF] Cousot | Abstract Interpretation and Applications to Logic Programs[END_REF][START_REF] Armstrong | Two classes of Boolean functions for dependency analysis[END_REF][START_REF] Codish | Sharing and groundness dependencies in logic programs[END_REF]) ) have been proposed for the analysis of logic programs.

The particular characteristics of timed ccp programs pose additional difficulties for the development of such tools in this language. Namely, the concurrent, timed nature of the language, and the synchronization mechanisms based on entailment of constraints (blocking asks). Aiming at statically analyzing utcc as well as tcc programs, we have to consider the additional technical issues due to the infinite internal computations generated by parametric asks as we shall explain later.

We develop here a compositional semantics for tcc and utcc that allows us to describe the behavior of programs and collects all concrete information needed to properly abstract the properties of interest. This semantics is based on closure operators over sequences of constraints along the lines of [START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF]). We show that parametric asks in utcc of the form (abs x ; c) P can be neatly characterized as closure operators. This characterization is shown to be somehow dual to the semantics for the local operator (local x ) P that restricts the variables in x to be local to P . We prove the semantics to be fully abstract w.r.t. the operational semantics for a significant fragment of the calculus.

We also propose an abstract semantics which approximates the concrete one. Our framework is formalized by abstract interpretation techniques and is parametric w.r.t. the abstract domain. It allows us to exploit the work done for developing abstract domains for logic programs. Moreover, we can make new analyses for reactive and mobile systems, thus widening the reasoning techniques available for tcc and utcc, such as type systems [START_REF] Hildebrandt | Types for secure pattern matching with local knowledge in universal concurrent constraint programming[END_REF], logical characterizations [START_REF] Mendler | A logical view of concurrent constraint programming[END_REF]Nielsen et al. 2002a;Olarte and Valencia 2008b) and semantics [START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF][START_REF] De Boer | Nondeterminism and infinite computations in constraint programming[END_REF]Nielsen et al. 2002a).

The abstraction we propose proceeds in two-levels. First, we approximate the constraint system leading to an abstract constraint system. We give the sufficient conditions which have to be satisfied for ensuring the soundness of the abstraction. Next, to obtain efficient analyses, we abstract the infinite sequences of (abstract) constraints obtained from the previous step. Our semantics is then computable and compositional. Thus, it allows us to master the complexity of the data-flow analyses. Moreover, the abstraction over-approximates the concrete semantics, thus preserving safety properties.

To the best of our knowledge, this is the first attempt to propose a compositional semantics and an abstract interpretation framework for a language adhering to the above-mentioned characteristics of utcc. Hence we can develop analyses for several applications of utcc or its sub-calculus tcc (see e.g., [START_REF] Olarte | Models and emerging trends of concurrent constraint programming[END_REF])).

In particular, we instantiate our framework in three different scenarios. The first one presents an abstraction of a cryptographic constraint system. We use the abstract semantics to bound the number of messages that a spy may generate, in order to exhibit a secrecy flaw in a security protocol written in utcc. The second one tailors an abstract domain for groundness and type dependency analysis in logic programming to perform a groundness analysis of a tcc program. This analysis is proven useful to derive a property of a control system specified in tcc. Finally, we present an analysis that may show that a tcc program is suspension free. This analysis can be used later for optimizing compilation or for debugging purposes.

The ideas of this paper stem mainly from the works of the authors in [START_REF] De Boer | Nondeterminism and infinite computations in constraint programming[END_REF]Falaschi et al. 1997a;Falaschi et al. 1997b;Nielsen et al. 2002a;Olarte and Valencia 2008a) to give semantic characterization of ccp calculi and from the works in (Falaschi et al. 1993;Codish et al. 1994;Falaschi et al. 1997a;[START_REF] Zaffanella | Abstracting synchronization in concurrent constraint programming[END_REF]Falaschi et al. 2007) to provide abstract interpretation frameworks to analyze concurrent logic-based languages. A preliminary short version of this paper without proofs was published in (Falaschi et al. 2009). In this paper we give many more examples and explanations. We also refine several technical details and present full proofs. Furthermore, we develop a new application for analyzing suspension-free tcc programs.

The rest of the paper is organized as follows. Section 2 recalls the notion of constraint system and the operational semantics of tcc and utcc. In Section 3 we develop the denotational semantics based on sequences of constraints. Next, in Section 4, we study the abstract interpretation framework for tcc and utcc programs. The three instances and the applications of the framework are presented in Section 5. Section 6 concludes.

Preliminaries

Process calculi based on the ccp paradigm are parametric in a constraint system specifying the basic constraints agents can tell and ask. These constraints represent a piece of (partial) information upon which processes may act. The constraint system hence provides a signature from which constraints can be built. Furthermore, the constraint system provides an entailment relation (`)s p e c i f y i n g inter-dependencies between constraints. Intuitively, c `d means that the information d can be deduced from the information represented by c. For example, x>60 `x>42.

Here we consider an abstract definition of constraint systems as cylindric algebras as in [START_REF] De Boer | Nondeterminism and infinite computations in constraint programming[END_REF]. The notion of constraint system as first-order formulas [START_REF] Smolka | A foundation for higher-order concurrent constraint programming[END_REF]Nielsen et al. 2002a;Olarte and Valencia 2008b) can be seen as an instance of this definition. All results of this paper still hold, of course, when more concrete systems are considered.

Definition 1 (Constraint System) A cylindric constraint system is a structure C = hC, , t, t, f, Var , 9,Di s.t.
-hC, , t, t, fi is a lattice with t the lub operation (representing the logical and ), and t, f the least and the greatest elements in C respectively (representing true and false).

(c)  c. (2) If c  d then 9x(c) 9 x(d). (3) 9x(c t9x(d)) ⇠ = 9x(c) t9x(d). (4) 9x9y(c) ⇠ = 9y9x(c). (5) For an increasing chain c 1 <c 2 <c 3 ..., 9x F i c i ⇠ = F i 9x(c i ). -For each x, y 2 Var , the constraint d xy 2 D is a diagonal element and it satisfies: (1) d xx ⇠ = t. (2) If z is different from x, y then d xy ⇠ = 9z(d xz t d zy ). (3) If x is different from y then c  d xy t9x(c t d xy ).
The cylindrification operators model a sort of existential quantification, helpful for hiding information. We shall use fv (c)={x 2 Var|9x(c) 6 ⇠ = c} to denote the set of free variables that occur in c.I fx occurs in c and x 6 2 fv (c), we say that x is bound in c.W eu s ebv (c) to denote the set of bound variables in c.

Properties (1) to (4) are standard. Property ( 5) is shown to be required in [START_REF] De Boer | Nondeterminism and infinite computations in constraint programming[END_REF] to establish the semantic adequacy of ccp languages when infinite computations are considered. Here, the continuity of the semantic operator in Section 3 relies on the continuity of 9 (see Proposition 2). Below we give some examples on the requirements to satisfy this property in the context of different constraint systems.

The diagonal element d xy can be thought of as the equality x = y. Properties (1) to ( 3) are standard and they allow us to define substitutions of the form [t/x] required, for instance, to represent the substitution of formal and actual parameters in procedure call. We shall give a formal definition of them in Notation 2.

Let us give some examples of constraint systems. The finite domain constraint system (FD) [START_REF] Hentenryck | Design, implementation, and evaluation of the constraint language cc(fd)[END_REF]) assumes variables to range over finite domains and, in addition to equality, one may have predicates that restrict the possible values of a variable to some finite set, for instance x<42.

The Herbrand constraint system H consists of a first-order language with equality. The entailment relation is the one we expect from equality, for instance, f (x, y)= f (g(a),z) must entail x = g(a) and y = z. H may contain non-compact elements to represent the limit of infinite chains. To see this, let s be the successor constructor, 9y(x = s(s n (y))) be denoted as the constraint gt(x, n)( i . e . ,x>n ) and {gt(x, n)} n be the ascending chain gt(x, 0) < gt(x, 1) < •••. We note that 9x(gt(x, n)) = t for any n and then, F {9x(gt(x, n))} n = t. Property (5) in Definition 1 dictates that 9x F {gt(x, n)} n must be equal to t (i.e., there exists an x which is greater than any n). For that, we need a constraint, e.g., inf(x) (a non-compact element), to be the limit F {gt(x, n)} n . We know that inf(x) `gt(x, n) for any n and then, F {gt(x, n)} n = inf(x) and 9x(inf(x)) = t as wanted. A similar phenomenon arises in the definition of constraint system as Scott information systems in [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]). There, constraints are represented as finite subsets of tokens (elementary constraints) built from a given set D. The entailment is similar to that in Definition 1 but restricted to compact elements, i.e., a constraint can be entailed only from a finite set of elementary constraints. Moreover, 9 is extended to be a continuous function, thus satisfying Property (5) in Definition 1. Hence, the Herbrand constraint system in [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]) considers also a non-compact element (different from f) to be the limit of the chain {gt(x, n)} n . Now consider the Kahn constraint system underlying data-flow languages where equality is assumed along with the constant nil (the empty list), the predicate nempty(x)(x is not nil ), and the functions first(x) (the first element of x), rest(x) (x without its first element) and cons(x, y) (the concatenation of x and y). If we consider the Kahn constraint system in [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF], the constraint c defined as {first(tail n (x)) = first(tail n (y)) | n ≥ 0} does not entail {x = y} since the entailment relation is defined only on compact elements. In Definition 1, we are free to decide if c is different or not from x = y. If we equate them, the constraint x = y is not longer a compact element and then, one has to be careful to only use a compact version of "=" in programs (see Definition 2). A similar situation occurs with the Rational Interval Constraint System [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]) and the constraints {x 2 [0, 1+1/n] | n ≥ 0} and x 2 [0,1].

All in all many different constraint systems satisfy Definition 1. Nevertheless, one has to be careful since the constraint systems might not be the same as what is naively expected due to the presence of non-compact elements.

We conclude this section by setting some notation and conventions about terms, sequences of constraints, substitutions and diagonal elements. We first lift the relation  and the cylindrification operator to sequences of constraints.

Notation 1 (Sequences of Constraints)

We denote by C ! (resp. C ⇤ ) the set of infinite (resp. finite) sequences of constraints with typical elements w, w 0 ,s,s 0 ,....W eu s eW, W 0 ,S,S 0 to range over subsets of C ! or C ⇤ .W eu s ec ! to denote the sequence c.c.c.... The length of s is denoted by |s| and the empty sequence by ✏.T h ei-th element in s is denoted by s(i). We write s  s 0 iff |s|| s 0 | and for all i 2{ 1,...,|s|}, s 0 (i) `s(i). If |s| = |s 0 | and for all i 2{ 1,...,|s|} it holds s(i) ⇠ = s 0 (i), we shall write s ⇠ = s 0 .G i v e nas e q u e n c e of variables x ,w i t h9x (c) we mean 9x 1 9x 2 ...9x n (c) and with 9x (s) we mean the pointwise application of the cylindrification operator to the constraints in s.

We shall assume that the diagonal element d xy is interpreted as the equality x = y. Furthermore, following [START_REF] Giacobazzi | Generalized semantics and abstract interpretation for constraint logic programs[END_REF], we extend the use of d xy to consider terms as in d xt . More precisely,

Convention 1 (Diagonal elements)

We assume that the constraint system under consideration contains an equality theory. Then, diagonal elements d xy can be thought of as formulas of the form x = y. We shall use indistinguishably both notations. Given a variable x and a term t (i.e., a variable, constant or n-place function of n terms symbol), we shall use d xt to denote the equality x = t. Similarly, given a sequence of distinct variables x and a sequence of terms t,i f|x Finally, we set the notation for substitutions.

| = | t| = n then d x t denotes the constraint F 1in x i = t i . If |x | = | t| =0t h e nd x t = t.
Notation 2 (Admissible substitutions) Let x be a sequence of pairwise distinct variables and t be a sequence of terms s.

Reactive Systems and Timed CCP

Reactive systems [START_REF] Berry | The Esterel synchronous programming language: Design, semantics, implementation[END_REF] are those that react continuously with their environment at a rate controlled by the environment. For example, a controller or a signal-processing system, receives a stimulus (input) from the environment. It computes an output and then, waits for the next interaction with the environment.

In the ccp model, the shared store of constraints grows monotonically, i.e., agents cannot drop information (constraints) from it. Then, a system that changes the state of a variable as in "signal = on" and "signal = off " leads to an inconsistent store.

Timed ccp (tcc) [START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF]) extends ccp for reactive systems. Time is conceptually divided into time intervals (or time-units). In a particular time interval, a ccp process P gets an input c from the environment, it executes with this input as the initial store, and when it reaches its resting point, it outputs the resulting store d to the environment. The resting point determines also a residual process Q which is then executed in the next time-unit. The resulting store d is not automatically transferred to the next time-unit. This way, computations during a time-unit proceed monotonically but outputs of two different time-units are not supposed to be related to each other. Therefore, the variable signal in the example above may change its value when passing from one time-unit to the next one.

Definition 2 (tcc Processes)

The set Proc of tcc processes is built from the syntax

P, Q := skip | tell(c) | when c do P | P k Q | (local x ) P | next P | unless c next P | p( t)
where c is a compact element of the underlying constraint system. Let D be a set of process declarations of the form p(x ):-P .Atcc program takes the form D. P .W e assume D to have a unique process definition for every process name, and recursive calls to be guarded by a next process.

The process skip does nothing thus representing inaction. The process tell(c) adds c to the store in the current time interval making it available to the other processes. The process when c do P asks if c can be deduced from the store. If so, it behaves as P . In other case, it remains blocked until the store contains at least as much information as c. The parallel composition of P and Q is denoted by P k Q. Given a set of indexes I = {1,. The process next P is a unit-delay that executes P in the next time-unit. The time-out unless c next P is also a unit-delay, but P is executed in the next timeunit if and only if c is not entailed by the final store at the current time interval. We use next n P as a shorthand for next ...next P ,w i t hnext repeated n times.

We extend the definition of free variables to processes as follows: fv (skip)=;; fv (tell(c)) = fv (c); fv (when

c do Q)=fv (c)[fv (Q); fv (unless c next Q)=fv (c)[ fv (Q); fv (Q k Q 0 )=fv (Q)[fv (Q 0 ); fv ((local x ) Q)=fv (Q)\x ; fv (next Q)=fv (Q); fv (p( t)) = vars( t)
w h e r evars( t) is the set of variables occurring in t. A variable x is bound in P if x occurs in P and x/ 2 fv (P ). We use bv (P ) to denote the set of bound variables in P .

Assume a (recursive) process definition p(x ):-P where fv (P ) ✓ x . The call p( t)r e d u c e st oP [ t/x]. Recursive calls in P are assumed to be guarded by a next process to avoid non-terminating sequences of recursive calls during a time-unit (see [START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF]Nielsen et al. 2002a)).

In the forthcoming sections we shall use the idiom ! P defined as follows:

Notation 3 (Replication)

The replication of P , denoted as ! P , is a short hand for a call to a process definition bang P () :-P k next bang P (). Hence, ! P means P k next P k next 2 P....

Mobile behavior and utcc

As we have shown, interaction of tcc processes is asynchronous as communication takes place through the shared store of partial information. Similar to other formalisms, by defining local (or private) variables, tcc processes specify boundaries in the interface they offer to interact with each other. Once these interfaces are established, there are few mechanisms to modify them. This is not the case e.g., in the ⇡-calculus [START_REF] Milner | A calculus of mobile processes, Parts Ia n dI I[END_REF] where processes can change their communication patterns by exchanging their private names. The following example illustrates the limitation of ask processes to communicate values and local variables.

Example 1

Let out(•) be a constraint and let P = when out(x) do R be a system that must react when receiving a stimulus (i.e., an input) of the form out(n) for n>0. We notice that P in a store out(42) does not execute R since out(42) 6 `out(x).

The key point in the previous example is that x is a free-variable and hence, it does not act as a formal parameter (or place holder) for every term t such that out(t) is entailed by the store.

In (Olarte and Valencia 2008b), tcc is extended for mobile reactive systems leading to universal timed ccp (utcc). To model mobile behavior, utcc replaces the ask operation when c do P with a parametric ask construction, namely (abs x ; c) P . This process can be viewed as a λ-abstraction of the process P on the variables x under the constraint (or with the guard ) c. Intuitively, for all admissible substitution [ t/x] s.t. the current store entails c[ t/x], the process (abs x ; c) P performs P [ t/x]. For example, (abs x; out(x)) R in a store entailing both out(z) and out(42) executes R[42/x] and R[z/x].

Definition 3 (utcc Processes and Programs)

The utcc processes and programs result from replacing in Definition 2 the expression when c do P with (abs x ; c) P where the variables in x are pairwise distinct.

When |x | =0w ew r i t ewhen c do P instead of (abs ✏; c) P . Furthermore, the process (abs x ; c) P binds x in P and c. We thus extend accordingly the sets fv (•) and bv (•) of free and bound variables.

From a programming point of view, we can see the variables x in the abstraction (abs x ; c) P as the formal parameters of P . In fact, the utcc calculus was introduced in (Olarte and Valencia 2008b) with replication (! P ) and without process definitions since replication and abstractions are enough to encode recursion. Here we add process definitions to properly deal with tcc programs with recursion which are more expressive than those without it (see (Nielsen et al. 2002b)) and we omit replication to avoid redundancy in the set of operators (see Notation 3). We thus could have dispensed with the next-guarded restriction in Definition 2 for utcc programs. Nevertheless, in order to give a unified presentation of the forthcoming results, we assume that utcc programs adhere also to that restriction. We conclude with an example of mobile behavior where a process P sends a local variable to Q. Then, both processes can communicate through the shared variable.

Example 2 (Scope extrusion) Assume two components P and Q of a system such that P creates a local variable that must be shared with Q. This system can be modeled as

P =( local x)(tell(out(x)) k P 0 ) Q =( abs z; out(z)) Q 0
We shall show later that the parallel composition of P and Q evolves to a process of the form P 0 k Q 0 [x/z]w h e r eP 0 and Q 0 share the local variable x created by P .

Then, any information produced by P 0 on x can be seen by Q 0 and vice versa.

Operational Semantics (SOS)

We take inspiration on the structural operational semantics (SOS) for linear ccp in (Fages et [START_REF] Boreale | Symbolic trace analysis of cryptographic protocols[END_REF][START_REF] Haemmerlé | Closures and modules within linear logic concurrent constraint programming[END_REF]) to define the behavior of processes.

We consider transitions between configurations of the form hx ; P ; ci where c is a constraint representing the current store, P a process and x is a set of distinct variables representing the bound (local) variables of c and P . We shall use γ, γ 0 ,.

P k Q ⌘ Q k P ; and (4) P k (Q k R) ⌘ (P k Q) k R.
The congruence relation ⌘ is extended to configurations by decreeing that hx ; P ; ci⌘ hỹ ;

Q; di iff (local x ) P ⌘ (local ỹ ) Q and 9x (c) ⇠ = 9ỹ (d).
Transitions are given by the relations -! and =) in Figure 1. The internal transition hx ; P ; ci-!hx 0 ; P 0 ; c 0 i should be read as "P with store c reduces, in one internal step, to P 0 with store c 0 ". We shall use -! ⇤ as the reflexive and transitive closure of -! .I fγ -! γ 0 and γ 0 ⌘ γ 00 we write γ -!⌘ γ 00 . Similarly for -! ⇤ .

; P 0 ; c 0 i⌘hỹ ; Q 0 ; c 00 i RCALL p(x ):-P 2D adm(x , t) ⌦ x ; p( t); d ↵ -! ⌦ x ; P [ t/x]; d ↵ RUNL d `c hx ; unless c next P ; di-!hx ; skip; di Observable Transition ROBS h;; P ; ci-! ⇤ hx ; Q; di 6 -! P (c,9x (d)) ==== ) (local x ) F (Q)
where F(P) = 8 < : The rules in Figure 1 are easily seen to realize the operational intuitions given in Section 2.1. As clarified below, the seemingly missing rule for a next process is given by R OBS . Before explaining such rules, let us introduce the following notation needed for R STRVAR .

F (skip)=F ((abs x ; c; D) Q)=skip F (P1 k P2)=F (P1) k F (P2) F (next Q)=F (unless c next Q)=Q

Notation 4 (Normal Form)

We observe that the store c in a configuration takes the form 9x 1 (d 1 ) t ... t9x n (d n ) where each x i may be an empty set of variables. The normal form of c, notation nf (c), is the constraint obtained by renaming the variables in c such that for all i, j 2 1..n,i fi 6 = j then the variables in x i do not occur neither bound nor free in d j . It is easy to see that c ⇠ = nf (c).

-R TELL says that the process tell(c) adds c to the current store d (via the lub operator of the constraint system) and then evolves into skip.

-R PAR says that if P may evolve into P 0 , this reduction also takes place when running in parallel with Q.

-Theprocess(local ỹ ) Q adds ỹ to the local variables of the configuration and then evolves into Q. The side conditions of the rule R LOC guarantee that Q runs with a different set of variables from those in the store and those used by other processes.

-We extend the transition relation to consider processes of the form (abs ỹ ; c; E) Q where E is a set of diagonal elements. If E is empty, we write (abs ỹ ; c) Q instead of (abs ỹ ; c; ;) Q.Ifd entails c[ t/ỹ], then P [ t/ỹ]isexecuted(RuleR ABS ). Moreover, the abstraction persists in the current time interval to allow other potential replacements of ỹ in P . Notice that E is augmented with d ỹ t and the side condition E 6 d ỹ t prevents executing P [ t/ỹ] again. The process P [ t/ỹ] is obtained by equating ỹ and t and then, hiding the information about ỹ ,i . e . ,( local ỹ )(!tell(d ỹ t) k P ).

-R u l eR STRVAR allows us to open the scope of existentially quantified constraints in the store (see Example 3 below). If γ reduces to γ 0 using this rule then γ ⌘ γ 0 .

-RuleR STR says that one can use the structural congruence on processes to continue a derivation (e.g., to do alpha conversion). It is worth noticing that we do not allow in this rule to transform the store via the relation ⌘ on configurations and then, via ⇠ = on constraints. We shall discuss the reasons behind this choice in Example 3.

-What we observe from p( t)i sP [ t/x] where the formal parameters are substituted by the actual parameter (Rule R CALL ).

-S i n c et h ep r o c e s sP = unless c next Q executes Q in the next time-unit only if the final store at the current time-unit does not entail c,intheruleR UNL P evolves into skip if the current store d entails c.

For the observable transition relation, rule R OBS says that an observable transition from P labeled with (c, 9x (d)) is obtained from a terminating sequence of internal transitions from h;; P ; ci to hx ; Q; di.T h ep r o c e s st ob ee x e c u t e di nt h e next time interval is (local x ) F (Q) (the "future" of Q). F (Q) is obtained by removing from Q the abs processes that could not be executed and by "unfolding" the sub-terms within next and unless expressions. Notice that the output of a process hides the local variables (9x (d)) and those variables are also hidden in the next time-unit ((local x ) F (Q)).

Now we are ready to show that processes in Example 2 evolve into a configuration where a (local) variable can be communicated and shared.

Example 3 (Scope Extrusion and Structural Rules)

Let P and Q be as in Example 2. In the following we show the evolution of the process P k Q starting from the store 9w(out(w)):

1 h;; P k Q; 9w(out(w))i-! ⇤ h{x}; tell(out(x)) k P 0 k Q; 9w(out(w))i 2 -! ⇤ h{x}; P 0 k Q; 9w(out(w)) t out(x)i 3 -! ⇤ h{x, w}; P 0 k Q; out(w) t out(x)i 4 -! ⇤ h{x, w}; P 0 k Q 1 k Q 0 [w/z]; out(w) t out(x)i 5 -! ⇤ h{x, w}; P 0 k Q 2 k Q 0 [w/z] k Q 0 [x/z]; out(w) t out(x)i where Q 1 =( abs z; out(z); {d wz }) Q 0 and Q 2 =( abs z; out(z); {d wz ,d xz }) Q 0 .
Observe that P 0 and Q 0 [x/z] share the local variable x created by P . The derivation from line 2 to line 3 uses the Rule R STRVAR to open the scope of w in the store 9w(out(w)). Let c 1 = 9w(out(w)) t out(x) (store in line 2) and c 2 = out(x). We know that c 1 ⇠ = c 2 . As we said before, Rule R STR allows us to replace structural congruent processes (⌘) but it does not modify the store via the relation ⇠ = on constraints. The reason is that if we replace c 1 in line 2 with c 2 , then we will not observe the execution of Q 0 [w/x].

Observables and Behavior

In this section we study the input-output behavior of programs and we show that such relation is a function. More precisely, we show that the input-output relation is a (partial) upper closure operator. Then, we characterize the behavior of a process by the sequences of constraints such that the process cannot add any information to them. We shall call this behavior the strongest postcondition. This relation is fundamental to later develop the denotational semantics for tcc and utcc programs.

Next lemma states some fundamental properties of the internal relation. The proof follows from simple induction on the inference γ -! γ 0 .

Lemma 1 (Properties of -! ) Assume that hx ; P ; ci-!hx 0 ; Q; di.T h e n ,x ✓ x 0 . Furthermore: 1. (Internal Extensiveness): 9x 0 (d) `9x (c), i.e., the store can only be augmented.

(Internal Potentiality)

: If e `c and d `e then hx ; P ; ei -!⌘ hx 0 ; Q; di,i . e . ,a stronger store triggers more internal transitions. 4. (Internal Restartability): hx ; P ; di -!⌘ hx 0 ; Q; di.

Input-Output Behavior

Recall that tcc and utcc allows for the modeling of reactive systems where processes react according to the stimuli (input) from the environment. We define the behavior of a process P as the relation of its outputs under the influence of a sequence of inputs (constraints) from the environment. Before formalizing this idea, it is worth noticing that unlike tcc, some utcc processes may exhibit infinitely many internal reductions during a time-unit due to the abs operator.

Example 4 (Infinite Behavior ) Consider a constant symbol "a", a function symbol f , a unary predicate (constraint) c(•) and let Q =(abs x; c(x)) tell(c(f (x))). Operationally, Q in a store c(a) engages in an infinite sequence of internal transitions producing the constraints c(f (a)), c(f (f (a))), c(f (f (f (a)))) and so on.

The above behavior will arise, for instance, in applications to security as those in Section 5.1. We shall see that the model of the attacker may generate infinitely many messages (constraints) if we do not restrict the length of the messages (i.e., the number of nested applications of f ).

Definition 5 (Input-Output Behavior ) Let s = c 1 .c 2 ...c n , s 0 = c 0 1 .c 0 2 ...c 0 n (resp. w = c 1 .c 2 ..., w 0 = c 0 1 .c 0 2 ...)b efi n i t e( r e s p . infinite) sequences of constraints. If P = P 1 (c1,c 0 1 ) ==== ) P 2 (c2,c 0 2 ) ==== ) ...P n (cn,c 0 n ) ==== ) P n+1 (resp. P = P 1 (c1,c 0 1 ) ==== ) P 2 (c2,c 0 2 ) ==== ) ... ),w ew r i t eP (s,s 0 ) ==== ) (resp. P (w,w 0 )
==== ) ! ). We define the input-output behavior of P as io(P )=io fin (P ) [ io inf (P )w h e r e io fin (P )={(s,

s 0 ) | P (s,s 0 ) ==== )} for s, s 0 2C ⇤ io inf (P )={(w, w 0 ) | P (w,w 0 ) ==== ) ! } for w, w 0 2C !
We recall that the observable transition ( ====)) is defined through a finite number of internal transitions (rule R OBS in Figure 1). Hence, it may be the case that for some utcc processes (e.g., Q in Example 4), io inf = ;. For this reason, we distinguish finite and infinite sequences in the input-output behavior relation. We notice that if w 2 io inf (P ) then any finite prefix of w belongs to io fin (P ). We shall call well-terminated the processes which do not exhibit infinite internal behavior.

Definition 6 (Well-termination) The process P is said to be well-terminated w.r.t. an infinite sequence w if there exists w 0 2C ! s.t. (w, w 0 ) 2 io inf (P ).

Note that tcc processes are well-terminated since recursive calls must be next guarded. The fragment of well-terminated utcc processes has been shown to be a meaningful one. For instance, in (Olarte and Valencia 2008a) the authors show that such fragment is enough to encode Turing-powerful formalisms and [START_REF] López | Towards a unified framework for declarative structured communications[END_REF] shows the use of this fragment in the declarative interpretation of languages for structured communications.

We conclude here by showing that the utcc calculus is deterministic. The result follows from Lemma 1 (see Appendix A).

Theorem 1 (Determinism) Let s, w and w 0 be (possibly infinite) sequences of constraints. If both (s, w), (s, w 0 ) 2 io(P )t h e nw ⇠ = w 0 .

Closure Properties and Strongest Postcondition

The unless operator is the only construct in the language that exhibits nonmonotonic input-output behavior in the following sense: Let P = unless c next Q and s  s 0 .I f( s, w), (s 0 ,w 0 ) 2 io(P ), it may be the case that w 6  w 0 . For example, take Q = tell(d), s = t ! and s 0 = c. t ! . The reader can verify that w = t .d. t ! , w 0 = c. t ! and then, w 6  w 0 .

Definition 7 (Monotonic Processes)

We say that P is a monotonic process if it does not have occurrences of unless processes. Similarly, the program D.P is monotonic if P and all P i in a process definition p i (x ):-P i are monotonic. Now we show that io(P )i sapartial upper closure operator, i.e., it is a function satisfying extensiveness and idempotence. Furthermore, if P is monotonic, io(P ) is a closure operator satisfying additionally monotonicity. The proof of this result follows from Lemma 1 (see details in Appendix A).

Lemma 2 (Closure Properties) Let P be a process. Then, io(P ) is a function. Furthermore, io(P ) is a partial upper closure operator, namely it satisfies: Extensiveness:I f( s, s 0 ) 2 io(P )t h e ns  s 0 . Idempotence:I f( s, s 0 ) 2 io(P )t h e n( s 0 ,s 0 ) 2 io(P ).

Moreover, if P is monotonic, then:

Monotonicity:I f( s 1 ,s 0 1 ) 2 io(P ), (s 2 ,s 0
2 ) 2 io(P ) and s 1  s 2 ,t h e ns 0 1  s 0 2 .

A pleasant property of closure operators is that they are uniquely determined by their set of fixpoints, here called the strongest postcondition.

Definition 8 (Strongest Postcondition) Given a utcc process P , the strongest postcondition of P , denoted by sp(P ), is defined as the set {s 2C ! [C ⇤ | (s, s) 2 io(P )}.

Intuitively, s 2 sp(P )iffP under input s cannot add any information whatsoever, i.e. s is a quiescent sequence for P . We can also think of sp(P ) as the set of sequences that P can output under the influence of an arbitrary environment. Therefore, proving whether P satisfies a given property A, in the presence of any environment, reduces to proving whether sp(P ) is a subset of the set of sequences (outputs) satisfying the property A. Recall that io(P )=io fin (P ) [ io inf (P ). Therefore, the sequences in sp(P ) can be finite or infinite.

We conclude here by showing that for the monotonic fragment, the input-output behavior can be retrieved from the strongest postcondition. The proof of this result follows straightforward from Lemma 2 and it can be found in Appendix A.

Theorem 2

Let min be the minimum function w.r.t. the order induced by  and P be a monotonic process. Then, (s, s 0 ) 2 io(P )i ffs 0 = min(sp(P ) \{w | s  w}).

A Denotational model for TCC and UTCC

As we explained before, the strongest postcondition relation fully captures the behavior of a process considering any possible output under an arbitrary environment. In this section we develop a denotational model for the strongest postcondition. The semantics is compositional and it is the basis for the abstract interpretation framework that we develop in Section 4.

Our semantics is built on the closure operator semantics for ccp and tcc in [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF][START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF][START_REF] De Boer | Proving concurrent constraint programs correct[END_REF]Nielsen et al. 2002a). Unlike the denotational semantics for utcc in (Olarte and Valencia 2008a), our semantics is more appropriate for the data-flow analysis due to its simpler domain based on sequences of constraints instead of sequences of temporal formulas. In Section 6 we elaborate more on the differences between both semantics.

Roughly speaking, the semantics is based on a continuous immediate consequence operator T D , which computes in a bottom-up fashion the interpretation of each process definition p(x ):-P in D. Such an interpretation is given in terms of the set of the quiescent sequences for p(x ).

Assume a utcc program D.P . We shall denote the set of process names with their formal parameters in D as ProcHeads. We shall call Interpretations the set of functions in the domain ProcHeads !P (C ! ). We shall define the semantics as a function [[•]] I :( ProcHeads !P (C ! )) ! (Proc !P (C ! )) which given an interpretation I, associates to each process a set of sequences of constraints.

Before defining the semantics, we introduce the following notation. Furthermore, given a set of sequences of constraints S ✓C ! ,w ed e fi n e :

DSKIP [[ skip]]

I = C ! DTELL [[ tell(c)]]I = "c.C ! DASK [[ when c do P ]] I = "c.C ! [ ("c.C ! \ [[ P ]] I ) DABS [[ ( abs x ; c) P ]] I = 88 x ([[when c do P ]] I ) DPAR [[ P k Q]] I =[ [ P ]] I \ [[ Q]] I DLOC [[ ( local x ) P ]] I = 99 x ([[P ]] I ) DNEXT [[ next P ]] I = C.[[ P ]] I DUNL [[ unless c next P ]] I = "c.[[ P ]] I [" c.C ! DCALL [[ p( t)]]I = I(p( t))
9 9 x (S)={s 2C ! | there exists s 0 2 S s.t. 9x (s) ⇠ = 9x (s 0 )} 8 8 x (S)={9ỹ (s) 2 S | ỹ ✓ Var ,s 2 S and for all s 0 2C ! , if 9x (s) ⇠ = 9x (s 0 ), d !
x t  s 0 and adm(x , t)t h e ns 0 2 S} The operators above are used to define the semantic equations in Figure 2 and explained in the following. Recall that [ [P ]] I aims at capturing the strongest postcondition (or quiescent sequences) of P , i.e. those sequences s such that P under input s cannot add any information whatsoever. The process skip cannot add any information to any sequence and hence, its denotation is C ! (Equation D SKIP ). The sequences to which tell(c) cannot add information are those whose first element entails c, i.e., the upward closure of c (Equation D TELL ). If neither P nor Q can add any information to s,t h e ns is quiescent for

P k Q. (Equation D PAR ).
We say that s is an x -variant of s 0 if 9x (s) ⇠ = 9x (s 0 ), i.e., s and s 0 differ only on the information about x . Let S = 9 9 x (S 0 ). We note that s 2 S if there is an x -variant s 0 of s in S 0 . Therefore, a sequence s is quiescent for Q =( local x ) P if there exists an x -variant s 0 of s s.t. s 0 is quiescent for P . Hence, if P cannot add any information to s 0 then Q cannot add any information to s (Equation D LOC ).

The process next P has no influence on the first element of a sequence. Hence if s is quiescent for P then c.s is quiescent for next P for any c 2C(Equation D NEXT ). Recall that the process Q = unless c next P executes P in the next time interval if and only if the guard c cannot be deduced from the store in the current time-unit. Then, a sequence d.s is quiescent for Q if either s is quiescent for P or d entails c (Equation D UNL ). This equation can be equivalently written as C.

[[ P ]] I [" c.C ! .
Recall that the interpretation I maps process names to sequences of constraints. Then, the meaning of p( t) is directly given by the interpretation I (Rule D CALL ).

Let Q = when c do P .As e q u e n c ed.s is quiescent for Q if d does not entail c. 4) and (5).

Compositional Semantics

We choose as semantic domain

E =(E, v c )w h e r eE = {X | X 2P(C ! ) and f ! 2 X} and X v c Y iff X ◆ Y .
The bottom of E is then C ! (the set of all the sequences) and the top element is the singleton {f ! } (recall that f is the greatest element in (C, )). Given two interpretations I 1 and I 2 ,w ew r i t eI 1 v c I 2 iff for all p, I 1 (p) v c I 2 (p).

Definition 9 (Concrete Semantics) Let [[•]] I be defined as in Figure 2. The semantics of a program D.P is the least fixpoint of the continuous operator:

T D (I)(p( t)) = [[Q[ t/x]]] I if p(x ):-Q 2D
We shall use [ [P ]] t o r e p r e s e n t [ [ P ]] lfp(T D ) .

In the following we prove some fundamental properties of the semantic operator T D , namely, monotonicity and continuity. Before that, we shall show that 8 8 is a closure operator and it is continuous on the domain E. 8 is continuous on (E, v c ).

Proof

The proofs of (1),( 2) and ( 3) are straightforward from the definition of 8 8 x .T h e proof of (4) proceeds as follows. Assume a non-empty ascending chain S 1 v c S 2 v c S 3 v c .... Lubs in E correspond to set intersection. We shall prove that I1 : p !"outa(x).C ! \C . "outa(y).C ! i.e., p !"outa(x). "outa(y).C ! q !8 8z(A.C ! ) \C .I?(q)i . e . ,q !8 8z(A).I?(q)

r !C ! \C ! = C ! I2 : p ! I1(p)
q !8 8z(A.C ! ) \C .I1(q)i . e . ,q !8 8z(A). 88

z(A.C ! ) \C .C.C ! r ! I1(p) \ I1(q) ... I! : p ! I1(p) q !8 8z(A). 88 z(A). 88 z(A)... r ! I!(p) \ I!(q)
Fig. 3: Semantics of the processes in Example 6.

A 1 ="(out a (z) t out b (z)), A 2 = "out a (z) and A = A 1 [ A 2 .
F I i = F Ii [[ P ]] Ii (Continuity).

Proof

Monotonicity follows easily by induction on the structure of P and it implies the the "w c " part of continuity. As for the part "v c " we proceed by induction on the structure of P . The interesting cases are those of the local and the abstraction operator. For P =( local x ) Q, by inductive hypothesis we know that [ [Q]]

F I i v c F Ii [[ Q]] Ii .
Since9 (and therefore 9 9 ) is continuous (see Property (5) in Definition 1), we conclude 9 9

x ([[Q]] F I i ) v c F Ii 9 9 x ([[Q]] Ii ).
The result for P =( abs x ; c) Q follows similarly from the continuity of 8 8 (Lemma 3).

Example 6 (Computing the semantics) Assume two constraints out a (•) and out b (•), intuitively representing outputs of names on two different channels a and b. Let D be the following procedure definitions

D = p() :-tell(out a (x)) k next tell(out a (y)) q() :-(abs z; out a (z)) (tell(out b (z))) k next q() r() :-p() k q()
The procedure p() outputs on channel a the variables x and y in the first and second time-units respectively. The procedure q() resends on channel b every message received on channel a. The computation of [[r()]] can be found in Figure 3. Let s 2 [[ r()]]. Then, it must be the case that s 2 [[ p()]] and then, s(1) `out a (x) and s(2) `out a (y). Since r 2 [[ q()]], for i ≥ 1, if s(i) `out a (t)t h e ns(i) `out b (t) for any term t. Hence, s(1) `out b (x) and s(2) `out b (y).

Semantic Correspondence

In this section we prove the soundness and completeness of the semantics.

Proof

Assume that hx ; P ; di-! ⇤ hx 0 ; P 0 ; d 0 i 6 -!, 9x (d) ⇠ = 9x 0 (d 0 ). We shall prove that 9x (d). 9 9 x 0 ([[F (P 0))]] ✓9 9x ([ [P ]]). We proceed by induction on the lexicographical order on the length of the internal derivation and the structure of P ,w h e r et h e predominant component is the length of the derivation. We present the interesting cases. The others can be found in Appendix B.

Case P = Q k S. Assume a derivation for Q = Q 1 and S = S 1 of the form hz ; Q k S, di-! ⇤ hz [ x 1 [ ỹ 1 ; Q 1 k S 1 ,c 1 t e 1 i -! ⇤ hz [ x i [ ỹ j ; Q i k S j ,c i t e j i -! ⇤ hz [ x m [ ỹ n ; Q m k S n ; c m t e n i 6 -! such that for i>0, each Q i+1 (resp. S i+1
) is an evolution of Q i (resp. S i ); x i (resp. ỹ j ) are the variables added by Q (resp. S); and c i (resp e j ) is the information added by Q (resp. S). We assume by alpha-conversion that x m \ ỹ n = ;. We know that 9z (d) ⇠ = 9z , x m ,ỹ n (c m t e n ) and from R PAR we can derive:

hz [ ỹ n ; Q; d t e n i-! ⇤ ⌘h z [ x m [ ỹ n ; Q m ,c m t e n i 6 -! and hz [ x m ; S; d t c m i-! ⇤ ⌘h z [ x m [ ỹ n ; S n ,c m t e n i 6 -!
By (structural) inductive hypothesis, we know that 9z , ỹ n (dte n ). 9

9 z , x m ,ỹ n [[ F (Q m )]] ✓ 9 9 z , ỹ n ([[Q]]) and also 9z , x m (d t c m ). 9 9 z , ỹ n ,x m [[ F (S n )]] ✓9 9z , x m ([[S]]). We note that 9 9 x ([[P ]] \ [[ Q]] ) = 9 9 x ([[P ]] ) \ [[ Q]] i f x \ fv (Q)=;
(see Proposition 7 in Appendix D). Hence, from the fact that x m \ fv (S n )=ỹ n \ fv (Q m )=;, we conclude:

9z (d). 9 9 z , x m ,ỹ n ([[F (Q m )]] \ [[ F (S n )]]) ✓9 9z ([[Q]] \ [[ S]] ) Case P =(abs x ; c) Q.
From the rule R ABS , we can show that

hỹ ; P ; di-! ⇤ hỹ 1 ; P 1 k Q 1 1 [ t1 /x]; d 1 i -! ⇤ hỹ 2 ; P 2 k Q 2 1 [ t1 /x] k Q 1 2 [ t2 /x]; d 2 i -! ⇤ hỹ 3 ; P 3 k Q 3 1 [ t1 /x] k Q 2 2 [ t2 /x] k Q 1 3 [ t3 /x]; d 3 i -! ⇤ ••• -! ⇤ hỹ n ; P n k Q m1 1 [ t1 /x] k Q m2 2 [ t2 /x] k Q m3 3 [ t3 /x] k•••kQ mn n [ tn /x]; d n i where P n takes the form (abs x ; c; E n ) Q, E n = {d x t1 ,...,d x tn } and 9ỹ (d) ⇠ = 9ỹ n (d n ).
Hence, there is a derivation (shorter than that for P ) for each d x ti 2 E n :

hỹ i ; Q 1 i [ ti /x]; d i i-! ⇤ ⌘hỹ 0 i ; Q mi i [ ti /x]; d 0 i i 6 -! with Q[ ti /x]=Q 1 i [ ti /x] and 9ỹ i (d i ) ⇠ = 9ỹ 0 i (d 0 i ). Therefore, by inductive hypothesis, 9ỹ i (d i ). 9 9 ỹ 0 i [[ F (Q mi i [ ti /x])]] ✓9 9 ỹ i [[ Q[ ti /x]]
] for all d x ti 2 E n . We assume, by alpha conversion, that the variables added for each Q j i are distinct and then, their intersection is empty. Furthermore, we note that 9ỹ (d) ⇠ = 9ỹ 1 (d 1 ). Since F (P n )=skip, we then conclude:

9ỹ (d). 9 9 ỹ n [[ F (P n k Y d x ti 2En Q mi i [ ti /x])]] ✓9 9ỹ [[ Y d x ti 2En Q[ ti /x])]] Let d.s 29 9ỹ [[ Q d x ti 2En Q[ ti /x])]].
Q mi i [ ti /x])]] ✓9 9ỹ 8 8 x [[ ( when c do Q)]]
Case P = p( t). Assume that p(x ):-Q 2D. We can verify that

hỹ ; p( t); di-!hỹ ; Q[ t/x]; di-! ⇤ hỹ 0 ; Q 0 ; d 0 i 6 -! where 9ỹ 0 (d 0 ) ⇠ = 9ỹ (d). By induction 9ỹ (d). 9 9 ỹ 0 [[ F (Q 0 )]] ✓9 9ỹ [[ Q[ t/x]]] and we con- clude 9ỹ (d). 9 9 ỹ [[ F (Q 0 )]] ✓9 9ỹ [[ p( t)]].
The previous lemma allows us to prove the soundness of the semantics.

1 ; c 1 i-! ⇤ hx i ; P i ; c i i-! ⇤ hx n ; P n ; c n i-! ⇤ ••• . Then, F 9x i (c i )  d.

Proof

Recall that procedure calls must be next guarded.

P ; ci-! ⇤ h{x 1 , ••• ,x i }; P i ; out(x 1 ) t•••tout(x i ) t out(w)i-! ⇤ h{x 1 , ••• ,x i , ••• ,x n }; P n ; out(x 1 ) t•••tout(x n ) t out(w)i-! ⇤ •••
At any step of the computation, the observable store is out(w) t

F i21..n 9x i out(x i )
which is equivalent to out(w). Note also that out(w

).C ! 2 [[ P ]] .
For the converse of Theorem 3, we have similar technical problems as in the case of tcc, namely: the combination of the local operator with the unless constructor. Thus, similarly to tcc, completeness is verified only for the fragment of utcc where there are no occurrences of unless processes in the body of local processes. The reader may refer (de Boer et al. 1995;Nielsen et al. 2002a) for counterexamples showing that [ [P ]] 6 ✓ sp(P )w h e nP is not locally independent.

Definition 10 (Locally Independent Fragment) Let D.P be a program where D contains process definitions of the form p i (x ):-P i . We say that D.P is locally independent if for each process of the form (local x ; c) Q in P and P i it holds that (1) Q does not have occurrences of unless processes; and

(2) if Q calls to p j (x ), then P j satisfies also conditions (1) and (2).

Proof

Assume that P is locally independent, d.s 2 [ [ P ]] and there is a derivation of the form hx ; P ; di-! ⇤ hx 0 ; P 0 ; d 0 i 6 -!. We shall prove that 9x (d) ⇠ = 9x 0 (d 0 ) and s 2 9 9 x 0 [[ F (P 0 )]]. We proceed by induction on the lexicographical order on the length of the internal derivation (-! ⇤ ) and the structure of P , where the predominant component is the length of the derivation. The locally independent condition is used for the case P =( local x ; c) Q. We only present the interesting cases. The others can be found in Appendix B.

; Q k S, di-! ⇤ ⌘hz [ x 0 [ ỹ 0 ; Q 0 k S 0 ; d 0 t d 00 t c t ei 6 -! We note that 9 9 x ([[P ]] \[[ Q]] ) = 9 9 x ([[P ]] ) \[[ Q]] i f x \fv (Q)=; (see Proposition 7 in Appendix D). Since F (Q 0 k S 0 )=F (Q 0 ) k F (S 0 ) and x 0 \ fv (S 0 )=ỹ 0 \ fv (Q 0 )=;, we conclude s 29 9z , x 0 ,ỹ 0 ([[F (Q 0 k R 0 )]]).
Case P =(abs x ; c) Q.B yu s i n gt h er u l eR ABS we can show that:

hx ; P ; di-! ⇤ hỹ 1 ; P 1 k Q 1 1 [ t1 /x]; d 1 1 i -! ⇤ hỹ 2 ; P 2 k Q 2 1 [ t1 /x] k Q 1 2 [ t2 /x]; d 2 1 t d 1 2 i -! ⇤ hỹ 3 ; P 3 k Q 3 1 [ t1 /x] k Q 2 2 [ t2 /x] k Q 1 3 [ t3 /x]; d 3 1 t d 2 2 t d 1 3 i -! ⇤ ••• -! ⇤ hỹ n ; P n k Q m1 1 [ t1 /x] k•••kQ mn n [ tn /x];
Q j i [ ti /x]. Note that Q[ ti /x]=Q 1 i [ ti /x].
There is a derivation (shorter than that for P ) for each d x ti 2 E n of the form

hỹ i ; Q 1 i [ ti /x]; d i i-! ⇤ ⌘hỹ 0 i ; Q mi i [ ti /x]; d mi i i 6 -! Since d.s 2 [[ P ]], by Proposition 1 we know that d.s 2 [[ Q 1 i [ ti /x]]
] and by induction,

9ỹ i (d i ) ⇠ = 9ỹ 0 i (d mi i ).
Furthermore, it must be the case that s 29 9ỹ 0

i [[ F (Q mi i [ ti /x])]]. Let e be the constraint 9ỹ n (d m1 1 t ... t d mn n ). Given that 9ỹ i (d i ) ⇠ = 9ỹ 0 i (d mi i ), we have 9x (d) ⇠ = e. Furthermore, given that F (P n )=skip: (abs x ; c) Q (d,e) ==== ) (local ỹ n ) F 0 @ Y d x ti 2En Q mi i [ ti /x] 1 A Since s 29 9ỹ 0 i [[ F (Q mi i [ ti /x])]] for all d x ti 2 E n , we conclude s 29 9ỹ n [[ F ( Y d x ti 2En Q mi i [ ti /x])]] Case P =(local x ) Q. By
Q; d 0 i-! ⇤ hỹ 0 ; Q 0 ; d 00 i 6 -! and 9ỹ (d 0 ) ⇠ = 9ỹ 0 (d 00 ) and s 0 29 9ỹ 0 [[ F (Q 0 )]].
We assume by alpha conversion that x \ ỹ = ;. Consider now the following derivation:

hỹ ;(local x ) Q; di-!hx [ ỹ ; Q; di-! ⇤ hỹ 00 ; Q 00 ,ci 6 -!
where x [ ỹ ✓ ỹ 00 . We know that d 0 `d and by monotonicity, we have 9ỹ 0 (d 00 ) 9ỹ 00 (c) and then, d 0 `9ỹ 00 (c). We then conclude 9ỹ (d) `9ỹ 00 (c). Since

s 0 29 9ỹ 0 [[ F (Q 0 )]] then s 29 9x 9 9 ỹ 0 [[ F (Q 0 )]].
Nevertheless, notice that in the above derivation of (local x ) Q, the final process is Q 00 and not Q 0 .S i n c eQ is monotonic, there are no unless processes in it. Furthermore, since d 0 `d,i t must be the case that Q 0 may contain sub-terms (in parallel composition) of the form R 0 [ t/x] resulting from a process of the form (abs ỹ ; e) R s.t. d 00 `e[ t/x] and c 6 `e[ t/x]. Therefore, by Rule D PAR , it must be also the case that s 0 2 [[ F (Q 00 )]] and then, s 29 9x , ỹ 0 [[ F (Q 00 )]]. Finally, note that ỹ 00 is not necessarily equal to ỹ 0 .W i t h a similar analysis we can show that in Q 0 there are possibly more local processes running in parallel than in Q 00 and then, s 29 9ỹ 00

[[ F (Q 00 )]].
By repeated applications of the previous Lemma, we show the completeness of the denotation with respect to the strongest postcondition relation.

Theorem 4 (Completeness) Let D.P be a locally independent program, w = s 1 .s 0 1 and w 2

[[ P ]] . I f P (s1,s 0 1 ) ==== ) then s 1 ⇠ = s 0 1 . Furthermore, if P (w,w 0 ) ==== ) ! then w ⇠ = w 0 .
Notice that completeness of the semantics holds only for the locally independent fragment, while soundness is achieved for the whole language. For the abstract interpretation framework we develop in the next section, we require the semantics to be a sound approximation of the operational semantics and then, the restriction imposed for completeness does not affect the applicability of the framework.

Abstract Interpretation Framework

In this section we develop an abstract interpretation framework [START_REF] Cousot | Abstract Interpretation and Applications to Logic Programs[END_REF] for the analysis of utcc (and tcc) programs. The framework is based on the above denotational semantics, thus allowing for a compositional analysis. The abstraction proceeds as a composition of two different abstractions: (1) we abstract the constraint system and then (2) we abstract the infinite sequences of abstract constraints. The abstraction in (1) allows us to reuse the most popular abstract domains previously defined for logic programming. Adapting those domains, it is possible to perform, e.g., groundness, freeness, type and suspension analyses of utcc programs. On the other hand, the abstraction in (2) along with (1) allows for computing the approximated output of the program in a finite number of steps.

Abstract Constraint Systems

Let us recall some notions from (Falaschi et al. 1997a) and [START_REF] Zaffanella | Abstracting synchronization in concurrent constraint programming[END_REF]).

Definition 11 (Descriptions) A description (C,↵,A) between two constraint systems

C = hC,  , t, t, f, Var , 9,Di A = hA,  ↵ , t ↵ , t ↵ , f ↵ , Var , 9 ↵ ,D ↵ i
consists of an abstract domain (A,  ↵ ) and a surjective and monotonic abstraction function ↵ : C!A .W el i f t↵ to sequences of constraints in the obvious way.

We shall use c ↵ , d ↵ to range over constraints in A and s ↵ ,s 0 ↵ ,w ↵ ,w 0 ↵ , to range over sequences in A ⇤ and A ! (the set of finite and infinite sequences of constraints in A). To simplify the notation, we omit the subindex "↵" when no confusion arises. The entailment `↵ is defined as in the concrete counterpart, i.e.

c ↵  ↵ d ↵ iff d ↵ `↵ c ↵ . Similarly, d ↵ ⇠ =↵ c ↵ iff d ↵ `↵ c ↵ and c ↵ `↵ d ↵ .
Following standard lines in [START_REF] Giacobazzi | Generalized semantics and abstract interpretation for constraint logic programs[END_REF]Falaschi et al. 1997a;[START_REF] Zaffanella | Abstracting synchronization in concurrent constraint programming[END_REF]) we impose the following restrictions over ↵ relating the cylindrification, diagonal and lub operators of C and A.

Definition 12 (Correctness) Let ↵ : C!Abe monotonic and surjective. We say that A is upper correct w.r.t. the constraint system C if for all c 2C and x, y 2 Var:

(1) ↵(9x (c)) ⇠ =↵ 9 ↵ x (↵(c)). (2) ↵(d x t) ⇠ =↵ d ↵ x t.
Since ↵ is monotonic, we also have ↵(c t d) `↵ ↵(c) t ↵ ↵(d).

In the example below we illustrate an abstract domain for the groundness analysis of tcc programs. Here we give just an intuitive description of it. We shall elaborate more on this domain and its applications in Section 5.2.

Example 8 (Constraint System for Groundness) Let the concrete constraint system C be the Herbrand constraint system. As abstract constraint system A, let constraints be propositional formulas representing groundness information as in x ^(y $ z) that means, x is a ground variable and, y is ground iff z is ground. In this setting, ↵(x =[a]) = x (i.e., x is a ground variable). Furthermore, ↵(x =[a|y]) = x $ y meaning x is ground if and only if y is ground.

[[ skip]] ↵ X = A ! ATELL [[ tell(c)]] ↵ X = "(↵(c)).A ! AASK [[ when c do P ]] ↵ X = *c.A ! [ (*c.A ! \ [[ P ]] ↵ X ) AABS [[ ( abs x ; c) P ]] ↵ X = 88 x ([[when c do P ]] ↵ X ) APAR [[ P k Q]] ↵ X =[ [ P ]] ↵ X \ [[ Q]] ↵ X ALOC [[ ( local x ) P ]] ↵ X = 99 x ([[P ]] ↵ X ) ANEXT [[ next P ]] ↵ X = A.[[ P ]] ↵ X AUNL [[ unless c next P ]] ↵ X = A ! ACALL [[ p( t)]] ↵ X = X(p( t))
In the following definition we make precise the idea when an abstract constraint approximates a concrete one.

Definition 13 (Approximations) Let (C,↵,A) be a description satisfying the conditions in Definition 11. Given d ↵ = ↵(d), we say that d ↵ is the best approximation of d. Furthermore, for all c ↵  ↵ d ↵ we say that c ↵ approximates d and we write c ↵ / d. This definition is pointwise extended to sequences of constraints in the obvious way (see Figure 4a).

Abstract Semantics

Now we define an abstract semantics that approximates the observable behavior of a program and is adequate for modular data-flow analysis. The semantic equations are given in Figure 5 and they are parametric on the abstraction function ↵ of the description (C,↵,A). We shall dwell a little upon the description of the rules A ASK and A UNL . The other cases are self-explanatory.

Given the right abstraction of the synchronization mechanism of blocking asks in ccp is crucial to give a safe approximation of the behavior of programs. In abstract interpretation, abstract elements are weaker than the concrete ones. Hence, if we approximate the behavior of when c do P by replacing the guard c with ↵(c), it could be the case that P proceeds in the abstract semantics but it does not in the concrete one. More precisely, let d, c 2C. Notice that from ↵(d) `↵ ↵(c) we cannot, in general, conclude d `c. Take for instance the constraint systems in Example 8. We know that ↵(x = a) ⇠ = ↵ ↵(x = b)b u tx = a 6 `x = b. Assume now we were to define the abstract semantics of ask processes as:

[[ when c do Q]] ↵ X = " (↵(c)).A ! [ (" (↵(c)).A ! \ [[ Q]] ↵ X ) (1)
A correct analysis of the process P = tell(x = a) k when x = b do tell(y = b) should conclude that only x is definitely ground. Since ↵(x = a) `↵ ↵(x = b), if we use Equation 1, the analysis ends with the result (x ^y).A ! , i.e., it wrongly concludes that x and y are definitely ground. We thus follow [START_REF] Zaffanella | Abstracting synchronization in concurrent constraint programming[END_REF]Falaschi et al. 1993;Falaschi et al. 1997a) for the abstract semantics of the ask operator. For this, we need to define the entailment `A that relates constraints in A and C.

Definition 14 (`A relation) Let d ↵ 2Aand c 2C. We say that d ↵ entails c, notation d ↵ `A c, if for all c 0 2Cs.t. d ↵ / c 0 it holds that c 0 `c. We shall use *c to denote the set {d ↵ 2A|d ↵ `A c}.
In words, the (abstract) constraint d ↵ entails the (concrete) constraint c if all constraints approximated by d ↵ entail c (see Figure 4b). Then, in Equation A ASK , we guarantee that if the abstract computation proceeds (i.e., d ↵ `A c)t h e ne v e r y concrete computation it approximates proceeds too.

In Equations D ABS and D LOC we use the operators 8 8 and 9 9 analogous to those in Notation 5. In this context, they are defined on sequences of constraints in A ! and they use the elements 9 ↵ , t ↵ and d ↵

x t instead of their concrete counterparts:

9 9 x (S ↵ )={s ↵ 2A ! | there exists s 0 ↵ 2 S ↵ s.t. 9 ↵ x (s ↵ ) ⇠ =↵ 9 ↵ x (s 0 ↵ )} 8 8 x (S ↵ )={9 ↵ ỹ (s ↵ ) 2 S ↵ | ỹ ✓ Var ,s ↵ 2 S ↵ and for all s 0 ↵ 2A ! , if 9 ↵ x (s ↵ ) ⇠ = 9 ↵ x (s 0 ↵ ),(d ↵ x t)
!  s 0 ↵ and adm(x , t)t h e ns 0 ↵ 2 S ↵ } We omitted the superindex "↵" in these operators since it can be easily inferred from the context.

The abstract semantics of the unless operator poses similar difficulties as in the case of the ask operator. Moreover, even if we make use of the entailment `A in Definition 14, we do not obtain a safe approximation. Let us explain this. One could think of defining the semantic equation for the unless process as follows:

[[ unless c next Q]] ↵ X = *c.[[ Q]] ↵ X [* c.A ! (2)
The problem here is that ↵(d) 6 `A c does not imply, in general, d 6 `c. (2), we conclude that d

↵ .(t ↵ ) ! / 2 [[ Q]] ↵ .
Hence, we have a sequence s such that s 2 [ [ Q]] and ↵(s) 6 2 [[ Q]] ↵ and the abstract semantics cannot be shown to be a sound approximation of the concrete semantics (see Theorem 5).

Notice that defining d ↵ 6 `A c as true iff c 0 6 `c for all c 0 approximated by d ↵ does not solve the problem. This is because under this definition, d ↵ 6 `A c does not hold for any d ↵ and c. To see this, notice that f entails all the concrete constraints and it is approximated by any abstract constraint. Therefore, we cannot give a better (safe) approximation of the semantics of unless c next P than A ! (Rule A UNL ).

Now we can formally define the abstract semantics as we did in Section 3. Given a description (C,↵,A), we choose as abstract domain is

A =( A, v ↵ )w h e r eA = {X | X 2P(A ! ) and (f ↵ ) ! 2 X} and X v ↵ Y iff X ◆ Y .
The bottom and top of this domain are similar to the concrete domain, i.e., A ! and {(f ↵ ) ! } respectively.

Definition 15 Let [[•]] ↵

X be as in Figure 5. The abstract semantics of a program D.P is defined as the least fixpoint of the continuous semantic operator:

T ↵ D (X)(p( t)) = [[(Q[ t/x])]] ↵ X if p(x ):-Q 2D We shall use [[P ]] ↵ to denote [[P ]] ↵ lfp(T ↵ D )
. The following proposition shows the monotonicity of [[•]] ↵ and the continuity of T ↵ D . The proof is analogous to that of Proposition 2.

Proposition 3 (Monotonicity of [[ •]]

↵ and Continuity of T ↵ D ) Let P be a process and X 1 v ↵ X 2 v ↵ X 3 ... be an ascending chain. Then,

[[P ]] ↵ Xi v c [[ P ]] ↵ Xi+1 (Monotonicity). Moreover, [[P ]] ↵ F X i = F Xi [[ P ]] ↵ Xi (Continuity).

Soundness of the Approximation

This section proves the correctness of the abstract semantics in Definition 15. We first establish a Galois insertion between the concrete and the abstract domains.

Proposition 4 (Galois Insertion) Let (C,↵ 0 , A) be a description and E, A be the concrete and abstract domains. If A is upper correct w.r.t. C then there exists an upper Galois insertion E ---! ---

↵ γ A. Proof Let A =(A, v ↵ ), E =(E, v c
) and ↵ : E ! A and γ : A ! E be defined as follows:

↵(S)= {β(s) | s 2 S} for S 2{X | X 2P(C ! ) and f ! 2 X} γ(S ↵ )= {s | β(s) 2 S ↵ } for S ↵ 2{X | X 2P(A ! ) and (f ↵ ) ! 2 X}
where β is the pointwise extension of ↵ 0 over sequences. Notice that β is a monotonic and surjective function between C ! and A ! and set intersection is the lub in both E and A. We conclude by the fact that any additive and surjective function between complete lattices defines a Galois insertion [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF]).

We lift, as standardly done in abstract interpretations [START_REF] Cousot | Abstract Interpretation and Applications to Logic Programs[END_REF]), the approximation induced by the above abstraction. Let I : ProcHeads ! E, X : ProcHeads ! A, β be as in Proposition 4 and p be a process definition. Then

↵(I(p)) = {β(s) | s 2 I(p)} γ(X(p)) = {s | β(s) 2 X(p)}
We conclude here by showing that concrete computations are safely approximated by the abstract semantics.

Theorem 5 (Soundness of the approximation) Let (C,↵,A) be a description and A be upper correct w.r. )(then-th application of T D ). We proceed by induction on the lexicographical order on the pair n and the structure of P , where the predominant component is n. We only present the interesting cases. The others can be found in Appendix C.

Case P =(abs x ; c) Q. Let [ t/x] be an admissible substitution. We shall prove that s 2 [[ ( when c do Q)[ t/x]]] implies s ↵ 2 [[ ( when c do Q)[ t/x]]] ↵ .
T h er e s u l t follows from Proposition 1 and from the fact that s

↵ 28 8x ([[when c do Q]] ↵ )i ff s ↵ 2 [[ ( when c do Q)[ t/x]
]] ↵ for all adm(x , t). The proof of the previous statement is similar to that of Proposition 1 and it appears in Appendix D.

Assume that

d `c[ t/x]. Then, d.s 2 [[ Q[ t/x]]
] and we distinguish two cases:

(1) d ↵ `A c[ t/x]. Since d.s 2 [[ Q[ t/x]]] then d.s 29 9x ([[Q]] \" (d ! x t)).
Therefore, there exists d 0 .s 0 , an x -variant of d.s,s . t .d 0 .s 0 2 [ [ Q]] and d 0 .s 0 2"(d ! x t). By (structural) inductive hypothesis, ↵(d 0 .s 0 ) 2 [[ Q]] ↵ . Furthermore, by monotonicity of ↵ and Property (2) in Definition 12, we derive ↵(d 0 .s 0 ) 2" (d

↵ x t) ! . Hence ↵(d 0 .s 0 ) 2 ([[Q]] ↵ \" ((d ↵ x t) ! ). Since 9x (d.s)=9x (d 0 .s 0 ), by Property (1) in Definition 12, we have 9 ↵ x (↵(d.s)) = 9 ↵ x (↵(d 0 .s 0 )) (i.e., ↵(d 0 .s 0 ) is an x -variant of d ↵ .s ↵ ). Then, d ↵ .s ↵ 29 9x ([[Q]] ↵ \" ((d ↵ x t) ! )) and we conclude d ↵ .s ↵ 2 [[ Q[ t/x]]] ↵ . (2) d ↵ 6 `A c[ t/x]. Hence trivially d ↵ .s ↵ 2 [[ ( when c do Q)[ t/x]]] ↵ .
We conclude by noticing that if

d 6 `c[ t/x]thend ↵ 6 `A c[ t/x] and therefore d ↵ .s ↵ 2 [[ ( when c do Q)[ t/x]]] ↵ . Case P :-p( t). Let p(x ):-Q in D be a process definition. If d.s 2 [[ p( t)]] then d.s 2 I(p( t)) (recall that I = lfp(T D )). We know that d.s 2 [[ Q[ t/x]]] and then, d.s 2 [[ Q[ t/x]]] I 0 where I 0 = T m D (I ?
)w i t hm<n . By induction, and continuity of

T ↵ D , we know that d ↵ .s ↵ 2 [[ Q[ t/x]]] ↵ and then d ↵ .s ↵ 2 [[ p( t)]] ↵ .

Obtaining a finite analysis

As standard in Abstract Interpretation, it is possible to obtain an analysis which terminates, by imposing several alternative conditions (see for instance Chapter 9 in [START_REF] Cousot | Abstract Interpretation and Applications to Logic Programs[END_REF]). So, one possibility is to impose that the abstract domain is noetherian (also called finite ascending chain condition). Another possibility is to use widening operators, or to find an abstract domain that guarantees termination after a finite number of steps. So, our framework allows to use all this classical methodologies. In the examples that we have developed we shall focus our attention on a special class of abstract interpretations obtained by defining what we call a sequence abstraction mapping possibly infinite sequences of (abstract) constraints into finite ones. Actually we can define these abstractions as Galois connections.

Definition 16 (k-sequence Abstraction) A k-sequence abstraction is given by the following pair of functions (↵ k ,γ k ), with

↵ k :( A ! ,  ↵ ) ! (A ⇤ k ,  ↵ ), and γ k :( A ⇤ k ,  ↵ ) ! (A ! ,  ↵ ).
As for the function ↵ k ,w es e t↵ k (s)=s 0 where s 0 has length k and s 0 (i)=s(i) for i  k. Similarly, γ k (s 0 )=s where s 0 (i)=s(i) for i  k and s 0 (i)=t for i>k.

It is easy to see that, for any k,( ↵ k ,γ k ) defines a Galois connection between (A ! ,  ↵ ) and (A ⇤ k ,  ↵ ). Thus it is possible to use compositions of Galois connections for obtaining a new abstraction [START_REF] Cousot | Abstract Interpretation and Applications to Logic Programs[END_REF].

If A in (C,↵,A) leads to a Noetherian abstract domain A, then the abstraction obtained from the composition of ↵ and any ↵ k above guarantees that the fixpoint of the abstract semantics can be reached in a finite number of iterations. Actually the domain that we obtain in this way is given by sequences cut at length k.Thenumber k determines the length of the cut and hence the precision of the approximation. The bigger k the better the approximation.

Applications

This section is devoted to show some applications of the abstract semantics developed here. We shall describe three specific abstract domains as instances of our framework: (1) we abstract a constraint system representing cryptographic primitives. Then we use the abstract semantics to exhibit a secrecy flaw in a security protocol modeled in utcc. Next, (2) we tailor two abstract domains from logic programming to perform a groundness and a type analysis of a tcc program. We then apply this analysis in the verification of a reactive system in tcc. Finally, [START_REF] Giacobazzi | Generalized semantics and abstract interpretation for constraint logic programs[END_REF] we propose an abstract constraint system for the suspension analysis of tcc programs.

Verification of Security Protocols

The ability of utcc to express mobile behavior, as in Example 2, allows for the modeling of security protocols. Here we describe an abstraction of a cryptographic constraint system in order to bound the length of the messages to be considered in a secrecy analysis. We start by recalling the constraint system in (Olarte and Valencia 2008b) whose terms represent the messages generated by the protocol and cryptographic primitives are represented as functions over such terms.

Definition 17 (Cryptographic Constraint System) Let Σ be a signature with constant symbols in P[K, function symbols enc, pair , priv and pub and predicates out(•) and secret(•). Constraint in C are formulas built from predicates in Σ, conjunction (t) and 9.

Intuitively, P and K represent respectively the principal identifiers, e.g. A, B, . . . and keys k, k 0 .W eu s e{m} k and (m 1 ,m 2 ) respectively, for enc(m, k) (encryption) and pair (m 1 ,m 2 ) (composition). For the generation of keys, priv (k) stands for the private key associated to the value k and pub(k) for its public key.

As standardly done in the verification of security protocols, a Dolev-Yao attacker [START_REF] Dolev | On the security of public key protocols[END_REF] is presupposed, able to eavesdrop, disassemble, compose, encrypt and decrypt messages with available keys. The ability to eavesdrop all the messages in transit in the network is implicit in our model due to the shared store of constraints. The other abilities are modeled by the following utcc processes: Disam() :-(abs x, y; out(( x, y)) )tell(out (x) t out (y)) Comp() :-(abs x, y; out(x) t out(y)) tell(out (( x, y)) ) Enc( ):-(abs x, y; out(x) t out(y)) tell(out ({x} pub(y) )) Dec( ):-(abs x, y; out(priv (y)) t out({x} pub(y) )) tell(out (x)) Pers( ):-(abs x; out(x)) next tell(out(x)) Spy()

:-Disam() k Comp() k Enc() k Dec() k Pers() k next Spy()
Since the final store is not automatically transferred to the next time-unit, the process Pers above models the ability to remember all messages posted so far.

It is easy to see that the process Spy() in a store out(m) may add messages of unbounded length. Take for example the process Comp() that will add the constraints out(m), out((m, (m, m))), out(((m, m),m)) and so on.

To deal with the inherent state explosion problem in the model of the attacker, symbolic (compact) representations of the behavior of the attacker have been proposed, for instance in [START_REF] Boreale | Symbolic trace analysis of cryptographic protocols[END_REF][START_REF] Fiore | Computing symbolic models for verifying cryptographic protocols[END_REF]Olarte and Valencia 2008b;[START_REF] Bodei | Detecting and preventing type flaws at static time[END_REF]). Here we follow the approach of restricting the number of states to be considered in the verification of the protocol, as for instance in [START_REF] Escobar | State space reduction in the maude-nrl protocol analyzer[END_REF][START_REF] Song | Athena: A novel approach to efficient automatic security protocol analysis[END_REF][START_REF] Palamidessi | Sat-based model-checking for security protocols analysis[END_REF]. Roughly, we shall cut the messages generated of length greater than a given , thus allowing us to model a bounded version of the attacker.

Before defining the abstraction, we notice that the constraint system we are considering includes existentially quantified syntactic equations. For this kind of equations it is necessary to refer to a solved form of them in order to have a uniform way to compute an approximation of the constraint system. We then consider constraints of the shape 9ỹ (x 1 = t 1 (ỹ ) t ... t x n = t n (ỹ )) where x = x 1 ,...x n are pairwise distinct and x \ỹ = ;. Here, t(ỹ )referstoatermwherefv (t(ỹ )) ✓ ỹ .Given a constraint, its normal form can be obtained by applying the algorithm proposed in [START_REF] Maher | Complete axiomatizations of the algebras of finite, rational and infinite trees[END_REF] where: quantifiers are moved to the outermost position and equations of the form f (t 1 ,...,t n )=f (t 0 1 ,...,t 0 n ) are replaced by t 1 = t 0 1 t ... t t n = t 0 n ; equations such as x = x are deleted; equation of the form t = x are replaced by x = t; and given x = t,ifx does not occur in t, x is replaced by t in t 0 in all equation of the form x 0 = t 0 . For instance, the solved form of 9z, y(x = f (y) t y = g(z)) is the constraint 9z(x = f (g(z))).

Definition 18 (Abstract secure constraint system) Let M be the set of terms (messages) generated from the signature Σ in Definition 17. Let lg : M!N be defined as lg(m)=0i fm 2P [K[Var; lg({m

1 } m2 )= M1 A ! B : {(m, A)} pub(B) M2 B ! A : {(m, n, B)} pub(A) M3 A ! B : {n} pub(B) (a) M1 A ! C : {(m, A)} pub (C) M 0 1 C ! B : {(m, A)} pub (B) M2 B ! A : {(m, n, B)} pub (A) M3 A ! C : {n} pub (C) (b)
↵  (c(m)) = c(cut  (m)) ↵  (d xt )=d xt 0 where t 0 = cut  (t) ↵  (c t c 0 )=↵  (c) t ↵  (c 0 ) ↵  (9x c )=9x ↵  (c)
and NF(c) is a solved form of the constraint c. We omit the superscript ↵ in the abstract operators t ↵ , 9 ↵ and d ↵ x t to simplify the notation.

We note that the previous abstraction reminds of the depth- abstractions typically done in the analysis of logic programs (see e.g., [START_REF] Sato | Enumeration of Success Patterns in Logic Programs[END_REF]).

We shall illustrate the use of the abstract constraint system above by performing a secrecy analysis on the Needham-Schröder (NS) protocol [START_REF] Lowe | Breaking and fixing the needham-schroeder public-key protocol using fdr[END_REF]. This protocol aims at distributing two nonces in a secure way. Figure 6(a) shows the steps of NS where m and n represent the nonces generated, respectively, by the principals A and B. The protocol initiates when A sends to B a new nonce m together with her own agent name A, both encrypted with B's public key. When B receives the message, he decrypts it with his secret private key. Once decrypted, B prepares an encrypted message for A that contains a new nonce n together with the nonce m and his name B. A then recovers the clear text using her private key. A convinces herself that this message really comes from B by checking whether she got back the same nonce sent out in the first message. If that is the case, she acknowledges B by returning his nonce. B does a similar test.

Assume the execution of the protocol in Figure 6(b). Here C is an intruder, i.e. a malicious agent playing the role of a principal in the protocol. As it was shown in [START_REF] Lowe | Breaking and fixing the needham-schroeder public-key protocol using fdr[END_REF], this execution leads to a secrecy flaw where the attacker C can reveal n which is meant to be known only by A and B. In this execution, the attacker replies to B the message sent by A and B believes that he is establishing a session key with A. Since the attacker knows the private key priv (C), she can decrypt the message {n} pub (C) and n is no longer a secret between B and A as intended.

We model the behavior of the principals of the NS protocol with the process definitions in Figure 7. Nonce generation is modeled by local constructs and the process tell(out(m)) models the broadcast of the message m. Inputs (message reception) are modeled by abs processes as in Example 3. In Resp,weusetheprocess Secrete(n) to state that the nonce n cannot be revealed. Finally, the process SpKn corresponds to the initial knowledge of the attacker: the names of the principals, their public keys and the leaked keys in the set Bad (e.g., the private key of C in the configuration of Figure 6

)}\ {c | if c À out({x, y})t h e nc `↵ out(x) t out(y)}\ {c | if c À out({x} pub(y) ) t out(priv (y)) then c `↵ out(x)}) [[ SpKn]] ↵ = {c1.c2 | ci `↵ out(pub(A)) t out(pub(B)) t out(pub(C))}\ {c1.c2 | ci `↵ out(A) t out(B) t out(C) t out(priv (C))} [[ NS]] ↵ =[ [ Spy]] ↵ \ [[ SpKn]] ↵ \ [[ init(A, C)]] ↵ \ [[ resp(B)]] ↵
Fig. 8: Abstract semantics of the process NS in Equation 3Consider the following process:

NS : -Spy k SpKn k Init(A, C) k Resp(B) (3)
By using the composition of ↵ 3 (as in Definition 18) and the sequence abstraction 2-sequence, we obtain the abstract semantics of NS as showed in Figure 8. This allows us to exhibit the secrecy flaw of the NS protocol pointed out in [START_REF] Lowe | Breaking and fixing the needham-schroeder public-key protocol using fdr[END_REF]:

Let s = c 1 .c 2 s.t. s 2 [[ NS]] ↵ .T h e n ,t h e r ee x i s tam 1 -n 1 -variant s 0 = c 0 1 .c 0 2 of s s.t. c 0 1 `out({m 1 ,A} pub(C) ) t out(priv (C)) t out({m 1 ,A} pub(B) ) c 0 2 `out({m 1 ,n 1 ,A} pub(A) ) t out({n 1 } pub(C) ) t out(secret(n 1 )) t out(out(n 1
)) This means that the nonce n 1 appears as plain text in the network and it is no longer a secret between A and B as intended.

Groundness Analysis

In logic programming one useful analysis is groundness. It aims at determining if a variable will always be bound to a ground term. This information can be used, e.g., for optimization in the compiler or as base for other data flow analyses such as independence analysis, suspension analysis, etc. Here we present a groundness anal- ysis for a tcc program. To this end, we shall use as concrete domain the Herbrand Constraint System and the following running example.

Example 9 (Append ) Assume the process definitions in Figure 9. The process gen a (x) adds an "a"tothe stream x when the environment provides go a = [] as input. Under input stop a =[], gen a (x) terminates the stream binding its tail to the empty list. The process gen b can be explained similarly. The process assign(x, y) persistently equates x and y. Finally, append (x, y, z)b i n d sz to the concatenation of x and y.

We shall use Pos [START_REF] Armstrong | Two classes of Boolean functions for dependency analysis[END_REF]) as abstract domain for the groundness analysis. In Pos, positive propositional formulas represent groundness dependencies among variables. For instance, ↵ G (x =[ a|b]) = x meaning that x is a ground variable and ↵ G (x =[ y|z]) = x $ (y ^z) meaning that x is ground if and only if both y and z are ground. Elements in this domain are ordered by logical implication, e.g., x t (x $ (y ^z)) `↵G y.

Observation 2 (Precision of Pos with respect to Synchronization) Notice that Pos does not distinguish between the empty list and a list of ground terms: Definition 14). This affects the precision of the analysis. For instance, let P = tell(x = []) and Q = when x =[ ]do tell(y = []). One would expect that the groundness analysis of P k Q determines that x and y are ground variables. Nevertheless, it is easy to see that x.true ! 2 [[ P ]] ↵ G and then, the information added by tell(y = []) is lost.

d  = ↵ G (x =[ ] )=↵ G (x =[ a]) = x and then, d  6 `A x = [] (see
We improve the accuracy of the analysis by using the abstract domain defined in [START_REF] Codish | Deriving polymorphic type dependencies for logic programs using multiple incarnations of prop[END_REF] to derive information about type dependencies on terms. The abstraction is defined as follows:

↵ T (x = t)= ⇢ list(x, x s )i ft =[y | x s ] for some y nil (x)i f t =[]
Informally, list(x, x s ) means x is a list iff x s is a list and nil(x) means x is the empty list. If x is a list we write list(x) and nil(x) `↵T list(x). Elements in the domain are ordered by logical implication.

The following constraint systems result from the reduced product [START_REF] Cousot | Abstract Interpretation and Applications to Logic Programs[END_REF]) of the previous abstract domains, thus allowing us to capture groundness and type dependency information.

[[ gena(x) k genb(y) k append(x, y, z)]] ↵ = 99 x1(GA1) \9 9 y1(GB1) \ A1 where Definitions of gen a (x),gen b (y) and append(x, y, z) are given in Example 9. Sets GB 1 ,..,GB  are similar to GA 1 ,..,GA  and omitted here.

GA1 = "hx $ x1,list(x, x1)i.A\ {c.s | if c À goa =[]thens 29 9x2(GA2)}\ {c.s | if c À stopa =[]thenhx1,nil(x1)i !  ↵ c.s} ••• GA = "hx-1 $ x,list(x-1,x)i.✏ \ {c.✏ | if c À stopa =[]thenc `↵ hx,nil(x)i} A1 = {c.s | if c À x =[]then(d ↵ yz ) !  ↵ c.s}\ {c.s | if c À 9x 0 ,x2(x =[x 0 |x2]) then c.s 29 9x 0 99 x2 99 z2("(hx $ x2,list(x, x2)i ! ) \ "(hz $ z2,list(z, z2)i ! ) \A.A2)} ••• A = {c.✏ | if c À x =[]thend ↵ yz  ↵ c}\ {c.✏ | if c À 9x 0 ,x  0 (x =[x 0 |x  0 ]) then c.✏ 29 9x 0 99 x  0 99 z  0 ("(hx $ x  0 ,list(x,x  0 )i).✏ \ "(hz $ z  0 ,list(z,z  0 )i).✏)}
Definition 19 (Groundness-type Constraint System) Let A GT = hA,  ↵ GT t ↵ GT , t ↵ GT , f ↵ GT , Var , 9 ↵ GT ,d ↵ GT i.G i v e nc 2C, ↵ GT (c)= h↵ G (c),↵ T (c)i.
The operations t ↵ GT and 9 ↵ GT correspond to logical conjunction and existential quantification on the components of the tuple and d ↵ GT

x t

is defined as h↵ We can verify that c m `↵ hy, list(y)i. Finally, since s 2 append(x, y, z), we can show that c max(n,m) `↵ hz, list(z)i. In words, the process P binds x, y and z to ground lists whenever the environment provides as input a series of constraints go a =[ ]( r e s p . go b = []) followed by an input stop a =[](resp.stop b =[]).

G (x = t),↵ T (x = t)i. Finally, hc  ,d  i ↵ GT hc 0  ,d 0  i iff c 0  `↵G c 

Reactive Systems

Synchronous data flow languages [START_REF] Berry | The Esterel synchronous programming language: Design, semantics, implementation[END_REF] such as Esterel and Lustre can be encoded as tcc processes [START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF][START_REF] Tini | On the expressiveness of timed concurrent constraint programming[END_REF]). This makes tcc an expressive declarative framework for the modeling and verification of reactive systems. Take for instance the program in Figure 11 The analyses developed here can provide additional reasoning techniques in tcc for the verification of such systems. For instance, by using the groundness analysis in the previous section, we can show that if c 1 .c 2 ....c  2 [[ micCtrl(Error, Button)]] ↵ and there exists 1

 i   s.t. c i `A (open =[]t on = [])
, then, it must be the case that c 1 `↵ hError, list(Error)i,i . e . ,Error is a ground variable. This means, that the system correctly binds the list Error to a ground term whenever the system reaches an inconsistent state.

Observation 3 (Synchronization constraints)

In several applications of tcc and utcc the environment interact with the system by adding as input some constraints that only appear in the guard of ask processes as on, off, open, close in Figure 11 and go a , stop a in the Figure 9. These constraints can be thought of as "synchronization constraints" (Fages et al. 2001). Furthermore, since these constraints are inputs from the environment, they are not expected to be produced by the program, i.e., they do not appear in the scope of a tell process. In these situations, in order to improve the accuracy of the analyses, one can orthogonally add those constraints in the abstract domain. This can be done, for instance, with a reduced product as we did in Definition 19 to give a finer approximation of the inputs go a and stop a by adding type dependency information.

Suspension Analysis

In a concurrent setting it is important to know whether a given system reaches a state where no further evolution is possible. Reaching a deadlocked situation is something to be avoided. There are many studies on this problem and several works developing analyses in (logic) concurrent languages (e.g. (Codish et al. 1994;[START_REF] Codish | A Confluent Semantic Basis for the Analysis of Concurrent Constraint Logic Programs[END_REF])). However, we are not aware of studies available for ccp and its temporal extensions. A suspended state in the context of ccp may happen when the guard of the ask processes are not carefully chosen and then, none of them can be entailed. In this section we develop an analysis that aims at determining the constraints that a program needs as input from the environment to proceed. This can be used to derive information about the suspension of the system. We start by extending Let ↵  be as in Definition 18. We choose as abstract domain A = S(↵  (C)) and we consider sequences of length one. In Figure 12 we show the abstract semantics. We notice that hc, nsi where c = 9m(out({x, y, m} pub(srv) ) t out({x, m} pub(y) )) is in the semantics [[Protocol]] ↵ and hc, ?i / 2 [[ Protocol]] ↵ . We then conclude that the protocol is able to correctly deliver the message to B.

Assume now that the code for the server is (wrongly) written as S 0 :-(abs x, y, m; out({x, y, m} pub(srv) )) tell(out({x, m} pub(x) )) k next S 0 () where we changed tell(out({x, m} pub(y) )) to tell(out({x, m} pub(x) )). We can verify that hc, ?i 2 [[ Protocol 0 ]] ↵ where c = 9m(out({x, y, m} pub(srv) )tout({x, m} pub(x) )). This can warn the programmer that there is a mistake in the code.

Concluding Remarks

Several frameworks and abstract domains for the analysis of logic programs have been defined (see e.g. [START_REF] Cousot | Abstract Interpretation and Applications to Logic Programs[END_REF][START_REF] Codish | Sharing and groundness dependencies in logic programs[END_REF][START_REF] Armstrong | Two classes of Boolean functions for dependency analysis[END_REF])). Those works differ from ours since they do not deal with the temporal behavior and synchronization mechanisms present in tcc-based languages. On the contrary, since our framework is parametric w.r.t. the abstract domain, it can benefit from those works.

We defined in (Falaschi et al. 2007) a framework for the declarative debugging of ntcc (Nielsen et al. 2002a) programs (a non-deterministic extension of tcc). The framework presented here is more general since it was designed for the static analysis of tcc and utcc programs and not only for debugging. Furthermore, as mentioned above, it is parametric w.r.t an abstract domain. In (Falaschi et al. 2007) we also dealt with infinite sequences of constraints and a similar finite cut over sequences was proposed there.

In (Olarte and Valencia 2008b) a symbolic semantics for utcc was proposed to deal with the infinite internal reductions of non well-terminated processes. This semantics, by means of temporal formulas, represents finitely the infinitely many constraints (and substitutions) the SOS may produce. The work in (Olarte and Valencia 2008a) introduces a denotational semantics for utcc based on (partial) closure operators over sequences of temporal logic formulas. This semantics captures compositionally the symbolic strongest postcondition and it was shown to be fully abstract w.r.t. the symbolic semantics for the fragment of locally-independent (see Definition 10) and abstracted-unless free processes (i.e., processes not containing occurrences of unless processes in the scope of abstractions). The semantics here presented turns out to be more appropriate to develop the abstract interpretation framework in Section 4. Firstly, the inclusion relation between the strongest postcondition and the semantics is verified for the whole language (Theorem 3) -in (Olarte and Valencia 2008a) this inclusion is verified only for the abstracted-unless free fragment-. Secondly, this semantics makes use of the entailment relation over constraints rather than the more involved entailment over first-order linear-time temporal formulas as in (Olarte and Valencia 2008a). Finally, our semantics allows us to capture the behavior of tcc programs with recursion. This is not possible with the semantics in (Olarte and Valencia 2008a) which was thought only for utcc programs where recursion can be encoded. This work then provides the theoretical basis for building tools for the data-flow analyses of utcc and tcc programs.

For the kind of applications that stimulated the development of utcc, it was defined entirely deterministic. The semantics here presented could smoothly be extended to deal with some forms of non-determinism like those in (Falaschi et al. 1997a), thus widening the spectrum of applications of our framework.

A framework for the abstract diagnosis of timed-concurrent constraint programs has been defined in [START_REF] Comini | Abstract diagnosis for timed concurrent constraint programs[END_REF] where the authors consider a denotational semantics similar to ours, although with several technical differences. The language studied in [START_REF] Comini | Abstract diagnosis for timed concurrent constraint programs[END_REF]) corresponds to tccp (de Boer et al. 2000), a temporal ccp language where the stores are monotonically accumulated along the time-units and whose operational semantics relies on the notion of true parallelism. We note that the framework developed in [START_REF] Comini | Abstract diagnosis for timed concurrent constraint programs[END_REF]) is used for abstract diagnosis rather than for general analyses.

Our results should foster the development of analyzers for different systems modeled in utcc and its sub-calculi such as security protocols, reactive and timed systems, biological systems, etc (see [START_REF] Olarte | Models and emerging trends of concurrent constraint programming[END_REF]) for a survey of applications of ccp-based languages). We plan also to perform freeness, suspension, type and independence analyses among others. It is well known that this kind of analyses have many applications, e.g. for code optimization in compilers, for improving run-time execution, and for approximated verification. We also plan to use abstract model checking techniques based on the proposed semantics to automatically analyze utcc and tcc code. In Theorem 5, the proof of the abs case requires the following auxiliary results (similar to those in the concrete semantics).

Observation 5 (Equality and x -variants) Let s ↵ and w ↵ be x -variants such that (d ↵ x t) !  ↵ s ↵ ,( d ↵ x t) !  ↵ w ↵ and adm(x , t). Then s ↵ ⇠ = ↵ w ↵ .

Proof

Let c ↵ = s ↵ (i) and d ↵ = w ↵ (i)w i t hi ≥ 1. We shall prove that c ↵ `↵ d ↵ and d ↵ `↵ c ↵ . We know that c ↵ t ↵ d ↵ x t ⇠ = ↵ c a and d ↵ t ↵ d ↵ x t ⇠ = ↵ d ↵ . We also know that 9

↵ x (c ↵ t ↵ d ↵ x t) ⇠ = ↵ 9 ↵ x (d ↵ t ↵ d ↵ x t).

  Elements in C are called constraints with typical elements c, c 0 ,d,d 0 .... If c  d and d  c we write c ⇠ = d.I fc  d and c 6 ⇠ = d,w ew r i t ec<d. -Var is a denumerable set of variables and for each x 2 Var the function 9x : C!Cis a cylindrification operator satisfying: (1) 9x

Fig. 1 :

 1 Fig.1: SOS. In R STR , ⌘ is given in Definition 4. In R ABS and R CALL , adm(x , t)i s defined in Notation 2. In R ABS , E is assumed to be a set of diagonal elements and 6 is defined in Convention 1. In R STRVAR , nf (d) is defined in Notation 4.

Fig. 2 :

 2 Fig. 2: Semantic Equations for tcc and utcc constructs. Operands ".", " , 8 8 and 9 9 are defined in Notation 5. A denotes the set complement of A in C ! .

  I and d ! x t  s 00 . By Observation 1, s 0 ⇠ = s 00 and thus, s 0 2 [[ P ]] I , a contradiction.As e q u e n c ed.s is quiescent for the process Q =(abs x; c) P if for all admissible substitution [ t/x], either d 6 `c[ t/x] or d.s is also quiescent for P [ t/x], i.e., d.s 2 8 8 x ([[(when c do P )]] I )( r u l eD ABS ). Notice that we can simply write Equation D ABS by unfolding the definition of D ASK as follows:[[ ( abs x ; c) P ]] I = 8 8 x ("c.C ! [ ("c.C ! \ [[ P ]] I ))The reader may wonder why the operator 8 8 (resp. Rule D ABS ) is not entirely dual w.r.t. 9 9 (resp. Rule D LOC ), i.e., why we only consider x -variants entailing d x t where [ t/x] is an admissible substitution. To explain this issue, let Q =(abs x; c) P where c = out (x) and P = tell(out 0 (x)). We know thats =(out(a) ^out 0 (a)). t ! 2 sp(Q)for a given constant a. Suppose that we were to define:[[ Q]] I = {s | for all x-variant s 0 of s if s 0 (1) `c then s 0 2 [[ P ]] I } Let c 0 = out(a) ^out 0 (a) ^out(x) and s 0 = c 0 . t ! . Notice that s 0 is an x-variant of s, s 0 (1) `c but s 0 / 2 [[ P ]] I (since c 0 6 `out 0 (x)). Then s/ 2 [[ Q]] I underthis naive definition of [[Q]] I . We thus consider only the x -variants s 0 s.t. each element of s 0 entails d x t. Intuitively, this condition requires that s 0 (1) `c t d x t in Equation D ABS and hence that s 0 (1) `c[ t/x]. Furthermore s 2 [[ P [ t/x]]] I realizes the operational intuition that P runs under the substitution [ t/x]. The operational rule R STRVAR makes also echo in the design of our semantics: the operator 8 8 considers constraints of the form 9z (s)w h e r ez is a (possibly empty) set of variables, thus allowing us to open the existentially quantified constraints as shown in the following example. Example 5 (Scope extrusion) Let P = when out(x) do tell(out 0 (x)), Q =( abs x ; out(x)) tell(out 0 (x)). We know that [[Q]] I = 8 8 x([[P ]] I ). Assume that d.s 2 [[ P ]] I .T h e n ,d must be in the set: C = {9x(out(x)), out(x)tout 0 (x), 9x(out(x)tout 0 (x)), out(y), out(y)tout 0 (y) •••} where either, d 6 `out(x) or d `out 0 (x). We note that: (1) (9x(out(x))).s / 2 [[ Q]] I since out(x) 6 2 C. Similarly, 9y(out(y)).s / 2 [[ Q]] I since out(y) 2 C but the xvariant out(x) t d xy 6 2 C (it does not entail out 0 (x)). (3) out(y).s 6 2 [[ P ]] I for the same reason. (4) Let e =( out(x) t out 0 (x)). We note that e.s 2 [[ Q]] I since e 2 C and there is not an admissible substitution [t/x]s . t .9x(e) ⇠ = 9x(e[t/x]). (5) Let e =(out(y) t out 0 (y)). Then, e.s 2 [[ Q]] I since e 2 C and the x-variant e t d xy 2 C. (6) Finally, if e = 9x(out(x) t out 0 (x)).s,t h e ne.s 2 [[ Q]] I as in (

Lemma 3 (

 3 Properties of 8 8 ) 8 8 is a closure operator, i.e., it satisfies (1) Extensivity: S v c 8 8 x (S); (2) Idempotency: 8 8 x (8 8 x (S)) = 8 8 x (S); and (3) Monotonicity:I fS v c S 0 then 8 8 x (S) v c 8 8 x (S 0 ). Furthermore, (4) 8

  •]] be as in Definition 9. If P (d,d 0 ) ==== ) R and d ⇠ = d 0 ,t h e nd.[[ R]] ✓ [[ P ]] .

  Lemma 5 (Completeness) Let D.P be a locally independent program s.t. d.s 2 [[ P ]] . I f P (d,d 0 ) ==== ) R then d 0 ⇠ = d and s 2 [[ R]] .

  Case P = Q k S. We know that d.s 2 [[ Q]] and d.s 2 [[ S]] and by (structural) inductive hypothesis, there are derivations hz ; Q; di-! ⇤ hz [ x 0 ; Q 0 ; d 0 t ci 6 -! and hz ; S; di-! ⇤ hz [ ỹ 0 ; S 0 ; d 00 t ei 6 -! s.t. s 29 9z , x 0 [[ F (Q 0 )]], s 29 9z , ỹ 0 [[ F (S 0 )]], 9z (d) ⇠ = 9z , x 0 (d 0 t c) and 9z (d) ⇠ = 9z , ỹ 0 (d 00 t e). Therefore, assuming by alpha conversion that x 0 \ ỹ 0 = ;, 9z (d) ⇠ = 9z , x 0 ,ỹ 0 (d 0 t d 00 t c t e) and by rule R PAR , hz

0 ↵

 0 Fig. 4: (a). c 0 ↵ approximates c (i.e., c 0 ↵ / c) and c ↵ = ↵(c) is the best approximation of c (Definition 13). Since ↵ is monotonic and c  d, c ↵  ↵ d ↵ . In (b), assume that for all d s.t. d 6 `c, d is not approximated by c ↵ . Then, all constraint c 0 approximated by c ↵ (the upper cone of c) entails c. In this case, c ↵ `A c (Definition 14).

ASKIP

Fig. 5 :

 5 Fig. 5: Abstract denotational semantics for utcc. `A and * are in Definition 14. A denotes the set complement of A.

  Take for instance ↵ in Example 8. We know that x 6 `A x =[ a] and x =[ a] `x =[ a]. Now let Q = unless c next tell(e), d be a constraint s.t. d `c and d ↵ = ↵(d). We know by rule D UNL that d. t ! 2 [[ Q]] . I f ↵(d) 6 `A c, then by using the Equation

  t. C.G i v e nautcc program D.P ,i fs 2 [[ P ]] t h e n ↵(s) 2 [[ P ]] ↵ . Proof Let d ↵ .s ↵ = ↵(d.s) and assume that d.s 2 [[ P ]] . T h e n , d.s 2 [[ P ]] I where I is the lfp of T D . By the continuity of T D ,thereexistsn s.t. I = T n D (I ?

Fig. 6 :

 6 Fig. 6: Steps of the Needham-Schroeder Protocol

  (b)).

Fig. 7 :

 7 Fig. 7: utcc model of the Needham-Schröder Protocol

Fig. 9 :

 9 Fig. 9: Appending streams (Example 9). The process definition gen b is similar to gen a but replacing the constant a with b.

Fig. 10 :

 10 Fig. 10: Abstract semantics of the process P = gen a (x) k gen b (y) k append(x, y, z). Definitions of gen a (x),gen b (y) and append(x, y, z) are given in Example 9. Sets GB 1 ,..,GB  are similar to GA 1 ,..,GA  and omitted here.

and d 0 

 0 `↵T d  . Consider the Example 9 and the abstraction ↵ resulting from the composition of ↵ GT above and sequence  . Note that the program makes use of guards of the form 9x 0 ,x 00 (x =[ x 0 |x 00 ]) and x = []. Note also that list(x, x 0 ) `A 9x 0 ,x 00 (x =[ x 0 |x 00 ]) and nil(x) `A x = []. Roughly speaking, this guarantees that the chosen domain is accurate w.r.t. the ask processes in the program. The semantics of the process P = gen a (x) k gen b (y) k append(x, y, z)isdepicted in Figure 10. Assume that s = c 1 .c 2 ...c  2 [[ P ]] ↵ . Let n   and assume that for i<n , c i `A go a = [] and c n `A stop a =[ ] .S i n c es 2 [[ P ]] ↵ , we know that s 2 [[ gen a (x)]] ↵ and then, we can verify that c n `↵ hx, list(x)i. Similarly, take m   and assume that for j<m , c j `A go b = [] and c m `A stop b = [].

Fig. 11 :

 11 Fig. 11: Model for a microwave controller (see Notation 3 for the definition of ! ).

[[

  Fig. 12: Semantics of the protocol in Example 12.

Proposition 7

 7 If x 6 2 fv (Q)t h e n9 9 x ([[P ]]\ [[ Q]] ) = 9 9 x ([[P ]] ) \ [[ Q]] . Proof (✓): Let d.s 29 9x ([[P ]] \ [[ Q]]).Then, there exists an x -variant d 0 .s 0 s.t. d 0 .s 0 2 [[ P ]] \ [[ Q]] . T h e n , d.s 29 9x ([[P ]]) (by definition) and d.s 2 [[ Q]] by Proposition 5. (◆): Let d.s 29 9x ([[P ]] ) \[[ Q]] . T h e n , t h e r e e x i s t s d 0 .s 0 x -variant of d.s s.t. d 0 .s 0 2 [[ P ]] . By Proposition 5, d 0 .s 0 2 [[ Q]] and therefore, d.s 29 9x ([[P ]] \ [[ Q]] ) .

  ..,n}, we shall use Q i2I P i to denote the parallel composition P 1 k ... k P n .Theprocess(local x ) P binds x in P by declaring it private to P .Itbeha v eslik eP , except that all the information on the variables x produced by P can only be seen by P and the information on the global variables in x produced by other processes cannot be seen byP .

  .. to range over configurations. Processes are quotiented by ⌘ defined as follows.

	Definition 4 (Structural Congruence)
	Let ⌘ be the smallest congruence satisfying: (1) P ⌘ Q if they differ only by a
	renaming of bound variables (alpha-conversion); (2) P k skip ⌘ P ; (3)

  If d entails c,t h e nd.s must be quiescent for P (rule D ASK ). In some cases, for the sake of presentation, we may write this equations as: Observation 1 (Equality and x -variants) Let S ✓C ! , z ✓ Var and s, w 2C ! be x -variants such that d ! x t  s, d ! x t  w and adm(x , t). (1) s ⇠ = w. (2) 9z (s) 28 8x (S)i ffs 28 8x (S). Now we establish the correspondence between the sets 8 8 x ([[P ]] I ) and [[P [ t/x]]] I which is fundamental to understand the way we defined the operator 8 8 . I . (() Let [ t/x] be an admissible substitution. Suppose, to obtain a contradiction, that s 2 [[ P [ t/x]]] I ,t h e r ee x i s t ss 0 x -variant of s s.t. d ! x t  s 0 and s 0 / 2 [[ P ]] I (i.e., s/ 28 8x ([[P ]] I )). Since s 2 [[ P [ t/x]]] I then s 29 9x ([[P ]] I \" d ! x t). Therefore, there exists s 00 x -variant of s s.t. s 00 2 [[ P ]]

	Before explaining the Rule D ABS , let us show some properties of 8 8 x (•). First, we
	note that the x -variables satisfying the condition d ! x t  s in the definition of 8 8 are equivalent (see the proof in Appendix B).
	Proposition 1
	s 28 8x ([[P ]]

[[ when c do P ]] I = {d.s | if d `c then d.s 2 [[ P ]] I } I ) if and only if s 2 [[ P [ t/x]]] I for all admissible substitution [ t/x]. Proof ())Let s 28 8x ([[P ]] I ) and s 0 be an x -variant of s s.t. d ! x t  s 0 where adm(x , t). By definition of 8 8 , we know that s 0 2 [[ P ]] I .S i n c ed ! x t  s 0 then s 0 2 [[ P ]] I \" (d ! x t). Hence s 29 9x ([[P ]] I \" (d ! x t)) and we conclude s 2 [[ P [ t/x]]]

  We abuse of the notation and we write 8 8 z(A).S instead of 8 8 z(A.C ! ) \C.S. (S i ). By definition we know that s and all x -variant s 0 of s satisfying d ! x t  s 0 for adm(x , t) belong to

	T 8 8 x (S i )=8 8 x ( for the T 8 8 x (S i ) ✓8 8x ( T S i ). The "✓" part (i.e., w c ) is trivial since 8 8 is monotonic. As T S i ) part, by extensiveness we know that 8 8 x (S i ) ✓ S i for all S i and then, T 8 8 x (S i ) ✓ T S i . Let s 2 T 8 8 x T 8 8 x (S i ) and then in T S i . Hence, s 28 8x ( T S i ) and we conclude T 8 8 x (S

i ) ✓8 8x ( T S i ).

Proposition 2 (Monotonicity of [[ •]] and continuity of T D ) Let P be a process and I 1 v c I 2 v c I 3 ... be an ascending chain. Then, [[P ]] Ii v c [[ P ]] Ii+1 (Monotonicity). Moreover, [[P ]]

  For an admissible d x t,e itherd 6 `c[ t/x] or d `c[ t/x]. In the first case, trivially d.s 2 [[ ( when c do Q)[ t/x]]]. In the second case, E n d x t. Hence, d.s 2 [[ Q[ t/x]]] and d.s 2 [[ ( when c do Q)[ t/x]]]. Here we conclude that for all admissible [ t/x], d.s 2 [[ ( when c do Q)[ t/x]]] and by Proposition 1 we derive:

	9ỹ (d). 9 9 ỹ [[ F (	Y
		d x ti	2En

  d m1 1 t ... t d mn n i where P n takes the form (abs x ; c; E n ) Q and E n = {d x t1 ,...,d x tn }. In the derivation above, d j i represents the constraint added by

  Init(A, C)]] ↵ = 99 m1 99 m2 ({c1.c2 | c1 `↵ out({m1,A} pub (C) ),c 2 `↵ out({A, m2} pub (C) )}\ A. 88 x({c2 | if c2 À out({m1,x,C} pub(A) )t h e nc2 `↵ out({x} pub(C) )})) [[ resp(B)]] ↵ = 88 x, u( 99 n1 {c1.c2 | if c1 À out({x, u} pub(B) )t h e n c2 `↵ secret(n1) t out({x, n1,B} pub(u) )}) [[ Spy]] ↵ = 88 x ({c1.c2 | if c1 À out(x)t h e nc2 `↵ out(x)}) \ S.S where S = 88 x, y({c | if c À out(x) t out(y)t h e nc `↵ out({x, y}) t out({x} pub(y)

[[

  Since c ↵ `↵ 9 ↵ x (c ↵ ), we can show that c ↵ `↵ 9 ↵ x (d ↵ t ↵ d ↵ x t). Furthermore, 9 ↵ x (d ↵ t ↵ d ↵ x t) t ↵ d ↵ x t `↵ d ↵ (see Notation 2). Hence, we conclude c ↵ `↵ d ↵ . The proof of d ↵ `↵ c ↵ is analogous. ↵ X . (() Let [ t/x]be an admissible substitution. Suppose, to obtain a contradiction, that s ↵ 2 [[ P [ t/x]]] ↵ X ,thereexistss 0 ↵ x -variant of s ↵ s.t. (d ↵ Therefore, there exists s 00 ↵ x -variant of s ↵ s.t. s 00 ↵ 2 [[ P ]] ↵ X and d ↵ x t!  ↵ s 00 ↵ . By Observation 5, s 0 ↵ ⇠ = ↵ s 00 ↵ and thus, s 0 ↵ 2 [[ P ]] ↵ X , a contradiction.

	Proposition 8
	s ↵ 28 8x ([[P ]] ↵
	!  ↵ s 0 ↵ where X .S i n c e( d ↵ x t) ↵ 2 [[ P ]] ↵ 8 , we know that s 0 adm(x , t). By definition of 8 !  ↵ s 0 ↵ x t) then s 0 ↵ 2 [[ P ]] ↵ X \" ((d ↵ x t)
	s ↵ / 28 8x ([[P ]] ↵	x t)	!  ↵ s 0 ↵ and s 0 ↵ / 2 [[ P ]] ↵ X (i.e.,

X ) if and only if s 2 [[ P [ t/x]]] ↵ X for all admissible substitution [ t/x]. Proof ())Let s ↵ 28 8x ([[P ]] ↵ X ) and s 0 ↵ be an x -variant of s ↵ s.t. (d ↵ ! ). Hence, s ↵ 29 9 ↵ x ([[P ]] ↵ X \" ((d ↵ x t) !

)) and we conclude

s ↵ 2 [[ P [ t/x]]] X )). Since s ↵ 2 [[ P [ t/x]]] ↵ X then s ↵ 29 9 ↵ x ([[P ]] ↵ X \" (d ↵ x t) ! ).

Acknowledgments. We thank Frank D. Valencia, François Fages and Rémy Haemmerlé for insightful discussions on different subjects related to this work. We also thank the anonymous reviewers for their detailed comments. Special thanks to Emanuele D'Osualdo for his careful remarks and suggestions for improving the paper. This work has been partially supported by grant 1251-521-28471 from Colciencias, and by Digiteo and DGAR funds for visitors.

the concrete semantics to a collecting semantics that keeps information about the suspension of processes. For this, we define the following constraint system.

Definition 20 (Suspension Constraint System) Let S = {?, ns} s.t. ?ns. Given a constraint system C = hC, , t, t, f, Var , 9,di, the suspension-constraint system S(C) is defined as S = hC ⇥ S,  s , t s , ht, ?i, hf, nsi,Var,9 s ,d s i where  s , t s are pointwise defined, 9 s

x (hc, c 0 i)=h9 x c, c 0 i and d s x t = hd x t, ?i.G i v e n a constraint c 2C, we shall use b c to denote the constraint hc, ?i.

Let us illustrate how S(C) allows us to derive information about suspension. We then have:

[[ b P ]] = {ht, "?i, hb, nsi, hc, "?i, hd, "?i, hf, nsi}.(C⇥S) ! [[ b Q]] = {ht, "?i, ha, "?i, hb, "?i, hd, nsi, hf, nsi}. Q]] and e `c,t h e ni tm u s t be the case that e 0 = ns. This corresponds to the intuition that if an ask process can evolve on a store c, it can evolve under any store greater than c (Lemma 1).

Next we define a program transformation that allows us to scatter suspension information when we want to verify that none of the ask processes suspend.

Example 11

Let P and Q be as in Example 10. Let also b

Hence we can conclude that only under input f neither P nor Q suspend.

The previous program transformation can be arbitrarily applied to subterms of the form P = Q i2I when c i do P i . Similarly, for verification purposes, a subterm of the form P =(abs ~x 1 ; c 1 ) P 1 k ... k (abs ~x n ; c n ) P n can be replaced by

Appendix A Detailed proofs Section 2.4

Before presenting the proof that utcc is deterministic, we shall prove the following auxiliary result.

Lemma 6 (Confluence) Suppose that γ 0 -! γ 1 , γ 0 -! γ 2 and γ 1 6 ⌘ γ 2 .T h e n ,t h e r ee x i s t sγ 3 such that γ 1 -! γ 3 and γ 2 -! γ 3 .

Proof

Let γ 0 = hx ; P ; ci. The proof proceed by structural induction on P . In each case where γ 0 has two different transitions (up to ⌘) γ 0 -! γ 1 and γ 0 -! γ 2 , one shows the existence of γ 3 s.t. γ 1 -! γ 3 and γ 2 -! γ 3 .

Given a configuration γ = hx ; P ; ci let us define the size of γ as the size of P as follows:

The proof proceeds by induction on the size of γ 0 . From the assumption γ 1 6 ⌘ γ 2 , it must be the case that the transition -! is not an instance of the rule R STRVAR ; moreover, P is neither a process of the form tell(c), (local x ) P , p( t) or unless c next P 0 (since those processes have a unique possible transition modulo structural congruence) nor next P or skip (since they do not exhibit any internal derivation).

For the case P = Q k R, we have to consider three cases. Assume that

2 ⌘hx 2 ; Q 2 ; c 2 i. We know by induction that if γ 0 0 -! γ 0 1 and γ 0 0 -! γ 0 2 then there exists γ 0 3 ⌘hx 3 ; Q 3 ; c 3 i such that γ 0 1 -! γ 0 3 and γ 0 2 -! γ 0 3 . We conclude by noticing that γ 1 -! γ 3 and γ 2 -! γ 3 where γ 3 ⌘h x 3 ; Q 3 k R; c 3 i. The remaining cases when (1) R has two possible transitions and (2) when Q moves to Q 0 and then R moves to R 0 are similar.

Let γ 0 ⌘h x ; P ; c 0 i with P =( abs ỹ ; c; D) Q. One can verify that γ 1 ⌘h x [ x 1 ; P 1 ; c 0 i where P 1 takes the form (abs ỹ ;

and γ 2 ⌘ hx [ x 2 ; P 2 ; c 0 i where P 2 takes the form (abs z ;

From the assumption γ 1 6 ⌘ γ 2 , it must be the case that d ỹ t1 6 ⇠ = d ỹ t2 . By alpha conversion we assume that

by a finite internal derivation. The number of possible internal transitions (up to ⌘) in any γ i = hx i ; P i ; c i i in the above derivation is finite.

Proof

We proceed by structural induction on P i . The interesting case is the abs process. Let Q =( abs x ; c) P . Suppose, to obtain a contradiction, that c i `c[ t/x] for infinitely many t (to have infinitely many possible internal transitions). In that case, it is easy to see that we must have infinitely many internal derivation, thus contradicting the assumption that γ n 6 -!.

Lemma 7 (Finite Traces)

If there is a finite internal derivation of the form γ 1 -! γ 2 -! • • • -! γ n 6 -! then, any derivation starting from γ 1 is finite.

Proof

We observe that recursive calls must be guarded by a next processes. Then, any infinite behavior inside a time-unit is due to an abs process. From Observation 4 and Lemma 6, it follows that any derivation starting from γ 1 is finite.

Theorem 1 (Determinism) Let s, w and w 0 be (possibly infinite) sequences of constraints. If both (s, w), (s, w 0 ) 2 io(P )t h e nw ⇠ = w 0 .

Proof

Lemma 2 (Closure Properties) Let P be a process. Then, (1) io(P ) is a function.

(2) io(P ) is a partial closure operator, namely it satisfies:

Extensiveness:I f( s, s 0 ) 2 io(P )t h e ns  s 0 .

Idempotence:I f( s, s 0 ) 2 io(P )t h e n( s 0 ,s 0 ) 2 io(P ).

Monotonicity: Let P be a monotonic process such that (s 1 ,s 0 1 ) 2 io(P ). If (s 2 ,s 0

2 ) 2 io(P ) and s 1  s 2 ,t h e ns 0 1  s 0 2 .

Proof

We shall assume here that the input and output sequences are infinite. The proof for the case when the sequences are finite is analogous. The proof of (1) is immediate from Theorem 1. For (2), assume that s = c 1 .c 2 ..., s 0 = c 0 1 .c 0 2 ... and that (s, s 0 ) 2 io(P ). We then have a derivation of the form:

For i ≥ 1, we also know that there is an internal derivation of the form h;; P i ; c i i-! ⇤ hx ; P 0 i ; c 0 i i 6 -! where P i+1 =(local x ) F (P 0 i ). Extensiveness follows from (1) in Lemma 1.

Idempotence is proved by repeated applications of (3) in Lemma 1.

As for Monotonicity, we proceed as in (Nielsen et al. 2002a). Let be the minimal ordering relation on processes satisfying: (1) skip P . (2) If P Q and

Intuitively, P Q represents the fact that Q contains "at least as much code" as P .

We have to show that for every P , P 0 , c, c 0 and x , x 0 if hx ; P ; ci-! ⇤ hx 0 ; P 0 ; c 0 i 6 -! then for every d `c and Q s.t. P Q there hx ; Q; di-! ⇤ hỹ ; Q 0 ; d 0 i 6 -! for some ỹ and Q 0 with (local x 0 ) F (P 0 ) (local ỹ ) F (Q 0 ) and 9ỹ (d 0 ) `9 x 0 (c 0 ). This can be proved by induction on the length of the derivation using the following two properties: (a) -! is monotonic w.r.t. the store, in the sense that, if hx ; P ; ci-!h x 0 ; P 0 ; c 0 i then for every d `c and Q s.t. P Q, hx ; Q; di-!hỹ ; Q 0 ; d 0 i where 9ỹ (d 0 ) `9x 0 (c 0 ) and (local x 0 ) P 0 (local ỹ ) Q 0 . (b) For every monotonic process P ,i fhx ; P ; ci 6 -! then for every d `c and Q such that P Q we have either hx

The restriction to programs which do not contain unless constructs is essential here.

Theorem 2

Let min be the minimum function w.r.t. the order induced by  and P be a monotonic process. Then, (s, s 0 ) 2 io(P )i ffs 0 = min(sp(P ) \{w | s  w})

Proof

Let P be a monotonic process and (s, s 0 ) 2 io(P ). By extensiveness s  s 0 and by idempotence, (s 0 ,s 0 ) 2 io(P ). Let s 00 = min(sp(P ) \{w | s  w}). Since s 0 2 sp(P ) and s  s 0 , it must be the case that s  s 00  s 0 .If(s 00 ,s 000 ) 2 io(P ), by monotonicity s 0  s 000 .S i n c es 00 2 sp(P ), s 00 ⇠ = s 000 and then, s 0  s 00 . We conclude s 0 ⇠ = s 00 .

Appendix B Detailed Proofs Section 3

Observation 1 (Equality and x -variants) Let S ✓C ! , z ✓ Var and s, w be x -variants such that d ! x t  s, d ! x t  w and adm(x , t). (1) s ⇠ = w. (2) 9z (s) 28 8x (S)i ffs 28 8x (S).

Proof

(1) Let i ≥ 1, c = s(i) and d = w(i). We prove that c `d and d `c.W ek n o w that c t

T h e" d `c" side is analogous and we conclude c ⇠ = d. Property (2) follows directly from the definition of 8 8 (•).

Lemma 4

Let

We proceed by induction on the lexicographical order on the length of the internal derivation and the structure of P ,w h e r et h e predominant component is the length of the derivation. Here we present the missing cases in the body of the paper. Case P = skip. This case is trivial.

where, by alpha-conversion, x \ ỹ = ; and x \ fv (d)=;. Assume that 9ỹ (d) ⇠ = 9ỹ 9x 0 (d 0 ). Since the derivation starting from Q is shorter than that starting from P , we conclude 9ỹ (d). 9

Proof

Assume that P is locally independent, d.s 2 [ [ P ]] and there is a derivation of the form hx ; P ; di-! ⇤ hx 0 ; P 0 ; d 0 i 6 -!. We shall prove that 9x(d) ⇠ = 9x 0 (d 0 ) and s 2 9 9 x 0 [[ F (P 0 )]]. We proceed by induction on the lexicographical order on the length of the internal derivation (-! ⇤ ) and the structure of P , where the predominant component is the length of the derivation. The locally independent condition is used for the case P =(local x ; c) Q. We present here the missing cases in the body of the paper. Case skip. This case is trivial Case P = tell(c). This case is trivial since it must be the case that d `c and hence d t c ⇠ = d. Case P = next Q. This case is trivial since hx ; P ; di 6 -! for any d and x and F (P )=Q.

. By using the rule R CALL we can show that there is a derivation hỹ

Proof

The proof proceeds by induction on the structure of P . We shall use the notation c(ỹ ) and P (ỹ ) to denote constraints and processes where the free variables are exactly ỹ and we shall assume that ỹ \ x = ;. We assume that d.s 2 [[ P (ỹ )]] and d 0 .s 0 is an x -variant of d.s. We consider the following cases. The others are easy.