Carlos Olarte
email: colarte@lix.polytechnique.fr

Frank D Valencia
email: fvalenci@lix.polytechnique.fr

The Expressivity of Universal Timed CCP: Undecidability of Monadic FLTL and Closure Operators for Security

Keywords: Concurrent Constraint Programming, First-order Linear Temporal Logic, Closure Operators, Security Protocols

The timed concurrent constraint programing model (tcc) is a declarative framework, closely related to First-Order Linear Temporal Logic (FLTL), for modeling reactive systems. The universal tcc formalism (utcc) is an extension of tcc with the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols. This paper is devoted to the study of 1) the expressiveness of utcc and 2) its semantic foundations. As applications of this study, we also state 3) a noteworthy decidability result for the well-established framework of FLTL and 4) bring new semantic insights into the modeling of security protocols. More precisely, we show that in contrast to tcc, utcc is Turing-powerful by encoding Minsky machines. The encoding uses a monadic constraint system allowing us to prove a new result for a fragment of FLTL: The undecidability of the validity problem for monadic FLTL without equality and function symbols. This result refutes a decidability conjecture for FLTL from a previous paper. It also justifies the restriction imposed in previous decidability results on the quantification of flexible-variables. We shall also show that as in tcc, utcc processes can be semantically represented as partial closure operators. The representation is fully abstract wrt the input-output behavior of processes for a meaningful fragment of the utcc. This shows that mobility can be captured as closure operators over an underlying constraint system. As an application we identify a language for security protocols that can be represented as closure operators over a cryptographic constraint system.

Introduction

Timed concurrent constraint programming (tcc) [START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF] is a declarative temporal formalism from concurrency theory for modeling reactive systems. The tcc calculus combines the traditional operational view of process calculi with a declarative one based upon first-order linear-time temporal logic (FLTL). The tcc language is parametric in an underlying constraint system specifying the basic constraints (pieces of information) that agents can tell or ask during execution (e.g, x > 42).

Both the computational expressiveness and semantic foundations of tcc have been thoroughly studied in the literature [START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF][START_REF] Nielsen | Temporal concurrent constraint programming: Denotation, logic and applications[END_REF][START_REF] Valencia | Decidability of infinite-state timed ccp processes and first-order ltl[END_REF]. This allowed for a better understanding of tcc and its relation with other formalisms. In particular, the expressiveness study in [START_REF] Valencia | Decidability of infinite-state timed ccp processes and first-order ltl[END_REF] shows that tcc processes can be represented as finitestate Büchi automata [START_REF] Buchi | On a decision method in restricted second order arithmetic[END_REF]. The denotational semantics study in [START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF] shows that tcc processes can be compositionally interpreted as closure operators (monotonic, idempotent, and extensive functions) over sequences of constraints.

Universal tcc [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF], henceforth utcc, is an extension of the tcc calculus. The purpose of the extension is to add to tcc the expressiveness needed for modeling mobility while preserving its elegant closure-operator semantic characterization. (Mobility refers to the communication of private names as typically done for mobile systems and security protocols in Concurrency Theory). Although [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF] illustrates several utcc examples involving mobility, no formal statement about the expressiveness of utcc nor the preservation of the closure-operator semantics has been previously given.

In this paper we shall study the expressiveness of utcc in terms of its computational power and semantic characterization. We shall show that 1) unlike tcc processes, utcc processes can represent Turing-powerful formalisms. Furthermore, we shall show that despite this extra expressiveness as tcc processes 2) utcc processes can still be compositionally interpreted as partial closure operators. We shall also show the applicability of this declarative framework and the elegant theory of concurrent constraint programming to other domains of computer science. By using 1) we shall state a new insightful undecidability result for the well-established framework of FLTL. As an application of 2) we shall also bring new semantic insights into the modeling of security protocols. These two applications correspond to 3) and 4) in the contributions below.

Contributions. More precisely, to show 1) above we shall encode in utcc Minsky machines [START_REF] Minsky | Computation: finite and infinite machines[END_REF]. The encoding of Minsky machines in utcc will be given in terms of a very simple decidable constraint system involving only monadic predicates and no equality nor function symbols. The importance of using such a constraint system is that it will allow us to use utcc to state a new impossibility result for monadic FLTL and the main technical application of this paper: Namely, 3) the undecidability of the validity problem for monadic FLTL without functions symbols and equality. In fact, we show that this FLTL is strongly incomplete which of course implies its undecidability. Notice that this result contrasts the standard decidability result of (untimed) monadic classic first-order logic [START_REF] Borger | The Classical Decision Problem[END_REF].

It is worth noticing that there are several works in the literature addressing the decidability of fragments of FLTL and in particular the monadic one [START_REF] Abadi | Corrigendum: The power of temporal proofs[END_REF][START_REF] Merz | Decidability and incompleteness results for first-order temporal logics of linear time[END_REF][START_REF] Szalas | Incompleteness of first-order temporal logic with until[END_REF][START_REF] Hodkinson | Decidable fragment of firstorder temporal logics[END_REF][START_REF] Nielsen | On the expressive power of temporal concurrent constraint programming languages[END_REF]. The above-mentioned result is insightful in that it answers an issue raised in a previous work and justifies some restrictions on monadic FLTL in other decidability results by showing them to be necessary. Namely, in [START_REF] Valencia | Decidability of infinite-state timed ccp processes and first-order ltl[END_REF] it was suggested that one could dispense with the restriction to negation-free formula in the decidability result for the Pnueli's FLTL fragment there studied. Our undecidability result actually contradicts this conjecture since with negation that logic would correspond to the FLTL here presented. Furthermore, another work in [START_REF] Merz | Decidability and incompleteness results for first-order temporal logics of linear time[END_REF] shows the decidability of monadic FLTL. This seemingly contradictory statement arises from the fact that unlike this work, [START_REF] Merz | Decidability and incompleteness results for first-order temporal logics of linear time[END_REF] disallows, without a technical explanation, quantification over flexible variables. Our results, therefore, show that restriction to be necessary for decidability thus filling a gap on the decidability study of monadic FLTL. We shall elaborate more on these related results in Section 4.2.

As for 2) above, by building on the semantics of tcc given in [START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF] we show that the input-output behavior of any utcc process can be characterized as a partial closure-operator. Because of additional technical difficulties posed by utcc, the codomain of the closure-operators is more involved than that for tcc. Namely, we shall use sequences of future-free temporal formulae (constraints) rather than sequences of basic constraints as in tcc. We shall also give a compositional denotational account of this closure-operator characterization. We shall show that closure-operator denotation of utcc is fully abstract wrt the input-output behavior of processes for a significant fragment of utcc. This in particular shows that mobility in utcc can be elegantly represented as closure operators over some underlying constraint system.

As an application of the above-mentioned semantic result, we shall 4) identify a process language for security protocols that can be represented as closure operators. This language arises as a specialization of utcc with a particular cryptographic constraint systems. We argue that the interpretation of the behavior of protocols as closure operators is a natural one: E.g., suppose f is a closure-operator denoting a spy inferring information from the one he sees on the network. By extensiveness (f (w) w), the spy produces new information from the one he obtains, by monotonicity (w v implies f (w) f (w)) the more information the spy gets, the more he will infer, and finally by idempotence (f (f (w)) = f (w)) the spy infers as much as possible from the info he gets. To our knowledge no closure operator denotational account has previously been given in the context of calculi for security protocols.

All in all, this paper gives an expressiveness account of a declarative framework in terms of computational power and semantic characterization, and importantly, with novel applications to other domains, namely FLTL and security protocols.

Organization. The paper is organized as follows. Section 2 gives some preliminaries and Section 3 recalls the notions and definitions of utcc. The expressiveness study and its application to FLTL is presented in Section 4. The closure-operator semantics and its application to security protocols is given in Section 5. Finally, we discuss the related work in Section 6.

In this section we recall the notions of constraint systems and Linear-Time Temporal Logic (FLTL).

Constraint Systems. Concurrent Constraint Programming (CCP) calculi [START_REF] Saraswat | The semantic foundations of concurrent constraint programming[END_REF] are parametric in a constraint system. A constraint system can be represented as a pair (Σ, ∆) where Σ is a signature of function and predicate symbols, and ∆ is a first-order theory over Σ. Given a constraint system (Σ, ∆), let L be its underlying first-order language with variables x, y, . . ., and the standard logic symbols ¬, ∧, ∨, ⇒, ⇔, ∃, ∀, true and false. The set of constraints C with typical elements c, d, . . . is given by the set of formulae over L modulo logical equivalence. We say that c entails d in ∆, written c ⊢ ∆ d, iff (c ⇒ d) ∈ ∆ (i.e., iff c ⇒ d is true in all models of ∆). We shall omit "∆" in ⊢ ∆ when no confusion arises. For operational reasons ⊢ is often required to be decidable.

Let T be the set of terms induced by Σ with typical elements t, t ′ , ... We shall use . = to denote syntactic term equivalence (e.g. x .

= x and x . = y). We use t for a sequence of terms t 1 , . . . , t n with length | t| = n. If | t| = 0 then t is written as ǫ. We use c[ t/ x], where | t| = | x| and x i 's are pairwise distinct, to denote c with the free occurrences of x i replaced with t i . The substitution [ t/ x] will be similarly applied to other syntactic entities.

Temporal Formulae and Constraints. In the following sections we shall make use of notions from First-Order Linear-Time Temporal Logic (FLTL). Here we recall the syntax and semantics of this logic. See [START_REF] Manna | The Temporal Logic of Reactive and Concurrent Systems: Specification[END_REF] for further details. Definition 1. Given a constraint system with a first-order language L, the LTL formulae we use are given by the syntax:

F, G, . . . := c | F ∧ G | ¬F | ∃xF | ⊖ F | •F | F.
where c is a constraint in L, from now on also referred to as state formula.

The modalities ⊖F, •F and F stand for resp., that F holds previously, next and always. We use ∀xF for ¬∃x¬F , and the eventual modality ✸F as an abbreviation of ¬ ¬F .

We presuppose the reader is familiar with the basic concepts of Model Theory. The non-logical symbols of L are given meaning in an underlying L-structure, or L-model, M(L) = (I, D). (They are interpreted via I as relations over a domain D of the corresponding arity). A state s is a mapping assigning to each variable x in L a value s[x] in D. This interpretation is extended to L-expressions in the usual way (e.g.

s[f (x)] = I(f )(s[x])). We write s |= M(L) c iff c is true wrt s in M(L). The state s is an x-variant of s ′ iff s ′ [y] = s[y]
for each y = x. We use σ to range over infinite sequences of states. We say that σ is an x-variant of σ ′ iff for each i ≥ 0, σ(i) (the i-th state in σ) is an x-variant of σ ′ (i) .

Furthermore, the variables are partitioned into rigid and flexible variables. For the rigid variables, each σ must satisfy the rigidity condition: If x is rigid then for all s, s ′ in σ s[x] = s ′ [x]. If x is a flexible variable then different states in σ may assign different values to x. Definition 2. We say that σ satisfies F in an L-structure M(L), written σ |= M(L) F, iff σ, 0 |= M(L) F where:

σ, i |= M(L) true σ, i |= M(L) false σ, i |= M(L) c iff σ(i) |= M(L) c σ, i |= M(L) ¬F iff σ, i |= M(L) F σ, i |= M(L) F ∧ G iff σ, i |= M(L) F and σ, i |= M(L) G σ, i |= M(L) ⊖F iff i > 0 and σ, i -1 |= M(L) F σ, i |= M(L) •F iff σ, i + 1 |= M(L) F σ, i |= M(L) F iff for all j ≥ i, σ, j |= M(L) F σ, i |= M(L) ∃xF iff for some x-variant σ ′ of σ, σ ′ , i |= M(L) F We say that F is valid in M(L) iff for all σ, σ |= M(L) F . F is said to be valid if F is valid for every model M(L).
Definition 3 (FLTL Theories). Given a constraint system (∆, Σ) with firstorder language L, the FLTL theory induced by ∆, T (∆) is the set of FLTL sentences that are valid in all the L-structures (or L-models) of ∆. We write

F ⊢ T (∆) G iff (F ⇒ G) ∈ T (∆).
We omit "(∆)" in ⊢ T (∆) when no confusion arises.

Closure Operators. Finally we recall the notion of (partial) closure operator that we shall use in Section 5. Given a partially ordered set (S, ≤), a partial closure operator on S is a function f : S → S with the following properties: For all x ∈ S 1. Extensiveness:

x ≤ f (x). 2. Idempotence: f (f (x)) = f (x).
Furthermore, f is a closure operator if it also satisfies 3 Monotonicity: for all x, y ∈ S, if x ≤ y then f (x) ≤ f (y).

A fundamental derived property of a closure operator is that it is uniquely determined by its set of fixed points.

Universal Timed CCP

In this section we first describe the temporal concurrent constraint (tcc) model [START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF] following the presentation in [START_REF] Nielsen | Temporal concurrent constraint programming: Denotation, logic and applications[END_REF]. We then recall the universal tcc model (utcc) introduced in [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF].

Timed CCP. The tcc calculus extends CCP for timed systems [START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF]. 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 interval. The resulting store d is not automatically transferred to the next time interval.

Definition 4. Processes P, Q, . . . in tcc are built from constraints in the underlying constraint system by the following syntax:

P, Q := skip | tell(c) | when c do P | P Q | (local x; c) P | next P | unless c next P | ! P
with the variables in x being pairwise distinct.

The process skip does nothing and tell(c) adds c to the store in the current time interval. If in the current time interval c can eventually be derived from the store, the ask process when c do P evolves into P within the same time interval. Otherwise when c do P evolves into skip. P Q denotes P and Q running in parallel during the current time interval and (local x; c) P binds x in P by declaring them private to P under a constraint c. The bound variables bv (Q) (free variables fv (Q)) are those with a bound (a not bound) occurrence in Q.

The unit-delay next P executes P in the next time interval. The time-out unless c next P is also an unit-delay, but P is executed in the next time unit iff c is not entailed by the final store at the current time interval. We use next n P as short for next . . . next P , with next repeated n times. Finally, the replication ! P means P next P next 2 P . . ., i.e., unboundedly many copies of P but one at a time.

The Language of UTCC

In [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF] the authors introduced the Universal Timed CCP calculus (utcc) by extending the tcc language with an abstraction operator. This calculus allows for mobility behavior in the sense of the π-calculus [START_REF] Milner | Communicating and Mobile Systems: the Pi-Calculus[END_REF], i.e. generation and communication of private channels or links. In this section we recall the notion of abstractions in utcc central to its expressivity. Later we present its operational semantics. See [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF] for further details.

In utcc, the ask operation when c do P is replaced with a parametric ask of the form (abs x; c) P . This process can be viewed as an abstraction of the process P on the variables x under the constraint (or with the guard ) c. From a programming language perspective, x in (local x; c) P can be viewed as the local variables of P while x in (abs x; c) P as the formal parameters of P.

From a logic perspective abstractions have a pleasant duality with the local operator: The processes (local x; c) P and (abs x; c) P correspond, resp., to the existential and universal formulae ∃ x(c ∧ F P ) and ∀ x(c ⇒ F P ) where F P corresponds to P . We shall elaborate more on this logical meaning of utcc processes in Section 4.2.

Definition 5 (utcc processes). The utcc processes result from replacing in the syntax in Definition 4 the expression when c do P with (abs x; c) P with the variables in x being pairwise distinct.

Intuitively, Q = (abs x; c) P executes P [ t/ x] in the current time interval for all the sequences of terms t s.t c[ t/ x] is entailed by the store. The process Q binds the variables x in P and c. Sets fv(.) and bv(.), are extended accordingly. Furthermore Q evolves into skip after the end of the time unit, i.e. abstractions are not persistent when passing from one time-unit to the next one.

Notation 1 We use when c do P for the empty abstraction (abs ǫ; c) P. We write (local x) P as a short for (local x; true) P . The derived operator (wait x; c) do P waits, possibly for several time units until for some t, c[ t/ x] holds. where stop, go / ∈ fv (P ). We shall use whenever c do P as a short for (wait ǫ; c) do P .

Mobile links. We conclude this section with a small example from [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF] illustrating how mobility is obtained from the interplay between abstractions and local processes.

Example 1 (Mobility). Let Σ be a signature with the unary predicates out 1 , out 2 , . . . and a constant 0. Let ∆ be the set of axioms over Σ valid in first-order logic. Let P = (abs y; out 1 (y)) tell(out 2 (y)) Q = (local z) (tell(out 1 (z)) when out 2 (z) do next tell(out 2 (0)))

Intuitively, if a link y is sent on channel out 1 , P forwards it on out 2 . Now, Q sends its private link z on out 1 and if it gets it back on out 2 it outputs 0 on out 2 .

An Operational Semantics for UTCC

The structural operational semantics (SOS) of utcc considers transitions between process-store configurations P, c with stores represented as constraints and processes quotiented by ≡. We use γ, γ ′ , . . . to range over configurations. Definition 6. Let ≡ be the smallest congruence satisfying: 0) P ≡ Q if they differ only by a renaming of bound variables 1) P skip ≡ P , 2)

P Q ≡ Q P , 3) P (Q R) ≡ (P Q) R, 4) P (local x; c) Q ≡ (local x; c) (P Q) if x ∈ fv (P ), 5) (local x; c) skip ≡ skip. Extend ≡ by decreeing that P, c ≡ Q, c iff P ≡ Q.
The SOS transitions are given by the relations -→ and =⇒ in Table 1. The internal transition P, d -→ P ′ , d ′ should be read as "P with store d reduces, in one internal step, to P ′ with store d ′ ". The observable transition P (c,d) = = = =⇒ R should be read as "P on input c, reduces in one time unit to R and outputs d". The observable transitions are obtained from finite sequences of internal transitions.

RT tell(c), d -→ skip, d ∧ c RP P, c -→ ˙P ′ , d ¸ P Q, c -→ ˙P ′ Q, d ŖL P, c ∧ (∃ xd) -→ ˙P ′ , c ′ ∧ (∃ xd) ¸ (local x; c) P, d -→ ˙(local x; c ′ ) P ′ , d ∧ ∃ xc ′ ŖU d ⊢ c unless c next P, d -→ skip, d RR ! P, d -→ P ||next ! P, d RA d ⊢ c[ t/ x] | t| = | x| (abs x; c) P, d -→ ˙P [ t/ x] (abs x; c ∧ x = t ) P, d ŖS γ1 -→ γ2 γ ′ 1 -→ γ ′ 2 if γ1 ≡ γ ′ 1 and γ2 ≡ γ ′ 2 RO P, c -→ * Q, d -→ P (c,d) = = = =⇒ F (Q)
Table 1. Internal and observable reductions. ≡ and F are given in Definitions 6 and 7. In RA,

x = t denotes W 1≤i≤| x| xi = ti. If | x| = 0, x = t is defined as false.
We only describe some of the rules in Table 1 due to space restrictions. The other rules are standard, easily seen to realize the operational intuitions given above (see [START_REF] Nielsen | Temporal concurrent constraint programming: Denotation, logic and applications[END_REF] for further details). As clarified below, the seemingly missing rules for "next" and "unless" processes are given by R O .

We dwell a little upon the description of Rule R L as it may seem somewhat complex. Consider Q = (local x; c) P in Rule R L . The global store is d and the local store is c. We distinguish between the external (corresponding to Q) and the internal point of view (corresponding to P ). From the internal point of view, the information about x, possibly appearing in the "global" store d, cannot be observed. Thus, before reducing P we first hide the information about x that Q may have in d by existentially quantifying x in d. Similarly, from the external point of view, the observable information about x that the reduction of internal agent P may produce (i.e., c ′ ) cannot be observed. Thus we hide it by existentially quantifying x in c ′ before adding it to the global store. Additionally, we make c ′ the new private store of the evolution of the internal process.

Rule R A describes the behavior of (abs x; c) P . If the store entails c[ t/ x] then P [ t/ x] is executed. Additionally, the abstraction persists in the current time interval to allow other potential replacements of x in P but c is augmented with x i = t i to avoid executing P [ t/ x] again.

Rule R O says that an observable transition from P labeled with (c, d) is obtained from a terminating sequence of internal transitions from P, c to a Q, d . The process R to be executed in the next time interval is equivalent to F (Q) (the "future" of Q). F (Q) is obtained by removing from Q abstractions and any local information which has been stored in Q, and by "unfolding" the sub-terms within "next" and "unless" expressions. Definition 7. Let F be a partial function defined as:

F (P ) =                skip if P = skip skip if P = (abs x; c) Q F (P 1 ) F (P 2 ) if P = P 1 P 2 (local x) F (Q) if P = (local x; c) Q Q if P = next Q Q if P = unless c next Q Notation 2
We shall denote with C ω the set of infinite sequences of constraints with typical elements α, α ′ , . . . . Given c ∈ C, c ω represents the constraint c.c . . . . The i-th element in α is denoted by α(i).

Input-Output Behavior. We will use the following input-output relations over utcc processes.

Definition 8 (Input-Output Relations). Given α = c 1 .c 2 ... and α ′ = c ′ 1 .c ′ 2 ..., we write P (α,α ′ ) ====⇒ whenever P = P 1 (c1,c ′ 1 ) ====⇒ P 2 (c2,c ′ 2 ) ====⇒ .... The set io(P ) = {(α, α ′ ) | P (α,α ′ )
====⇒} denotes the input-output behavior of P . If io(P ) = io(Q) we say that P and Q are input-output equivalent and we write P ∼ io Q. Furthermore, we say that P eventually outputs c, written P ⇓ c , if

P (true ω ,α ′ )
====⇒ and α ′ (i) ⊢ c for some i > 0.

Remark 1. Let P be a process and α, α ′ be sequences of constraints s.t. (α, α ′ ) ∈ io(P ). Recall that computation in tcc during a time-unit progresses via the monotonic accumulation of constraints [START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF]. Then for all i > 0, c ′ (i) ⊢ c(i).

Recall also that the final store at the end of the time-unit is not automatically transfered to the next one. Therefore, it may be the case that c(i

) ′ ⊢ c(i -1) ′ .
Constraints in α are provided by the environment as input to the system and then, they are not supposed to be related to each other.

In [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF], utcc is shown to be deterministic in the following sense:

Theorem 1 (Determinism [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF]). Let α, α ′ and β be sequences of constraints. If both (β, α), (β, α ′ ) ∈ io(P ) then for all i > 0, ⊢ α(i) ⇔ α ′ (i). I.e. the outputs of P are the same up to logical equivalence.

Remark 2. The reader may have noticed that the abstraction operator may induce an infinite sequence of internal transitions within a time interval thus never producing an observable transition. One source of infinite internal behavior involves looping (recursion) in abstractions. E.g.

R = (abs x; out 1 (x)) ((local z) tell(out 1 (z)))
with out 1 as in Example 1. A similar problem involves several abstractions producing mutual recursive behavior. Another source of infinite internal behavior involves the constraint system under consideration. Let R = (abs x; c) P.

If the current store d entails c[t/x] for infinitely many t's, then R will have to execute P [t/x] for each such t.

We shall see that there are meaningful utcc processes which do not exhibit infinite internal behavior. We call them well-terminated processes. In fact, we shall prove in the next section that they are sufficient to show that utcc is Turing-powerful.

Definition 9 (Well-termination). The process P is said to be well-terminated iff for every α, there exists α ′ such as (α, α ′ ) ∈ io(P ).

Nevertheless, in Section 5 we shall consider also non well-terminated processes. For this purpose, we will recall in Section 5.1 the alternative symbolic operational semantics given in [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF] which deals with the above-mentioned internal termination problems.

Expressiveness of UTCC

In this section we shall state the Turing expressiveness of utcc with monadic first-order logic as underlying constraint system. We shall also state our main application result, namely the undecidability of the validity problem for Monadic FLTL without equality nor function symbols.

Turing-Expressiveness of UTCC

We shall begin by showing that the sub-language of well-terminated utcc processes is Turing-powerful. We prove this by providing a utcc construction (or encoding) of two-counter machines, also called Minsky machines, which are known to be Turing-powerful [START_REF] Minsky | Computation: finite and infinite machines[END_REF]. This construction will be defined in terms of a very simple decidable underling constraint system: The monadic fragment of firstorder logic without function symbols nor equality. This is a key property for our undecidability result for FLTL.

A two-counter Minsky machine M (v0, v1) is an imperative program consisting of a sequence of labeled instructions L 1 ; . . . ; L k which modify the values of two non-negative counters c 0 and c 1 initially set to v 0 and v 1 (resp.). The instructions, using counters c n for n ∈ {0, 1}, are of three kinds:

L i : halt L i : c n := c n + 1; goto L j L i : if c n = 0 then goto L j else c n := c n -1; goto L k
The Minsky machine starts at L s and halts if the control reaches the location of a halt instruction. Furthermore, the Minsky machine M (v 0 , v 1 ) computes the value n if it halts with c 0 = n.

We presuppose a monadic constraint system including the uninterpreted predicates out, out m n (•) for n ∈ {0, 1} and m ∈ {1, 2} as in Example 1. Additionally, we presuppose the following propositional variables: isz n , inc n , dec n for n ∈ {0, 1} and halt . A counter is defined as follows The counters c 0 and c 1 are obtained by replacing the sub-index n in out m n (•), isz n , inc n and dec n by 0 and 1 respectively in the expression above. Intuitively, isz n is used to test if the counter is zero (line 1) and inc n and dec n to trigger the action of increment and decrement the counter respectively. Each time an increment instruction is executed, a new local variable is created and sent through the public channel out 1 n (•) (lines 3 and 7). Decrement operations (line 6) send back these local variables using the channel out 2 n (•). The processes in lines 3 ′ and 7 ′ when receiving the correspondent local variable on channel out 2 n (•) move to the state immediately before the last increment instruction took place.

c n = 1 ! when isz n do 2 unless inc n next tell(isz n ) 3 when inc n do next (local a) (tell(out 1 n (a))|| 3 ′ ! when out 2 n (a) do tell(isz n )) 4 ||! (abs z; out 1 n (z))
For the set of instruction L 1 ; . . . ; L n we assume a set of variables l 1 , . . . , l n . The i-th instruction is encoded as

[[L i ]] =! when out(l i ) do ins(L i ) where ins(L i ) =                    tell(halt) if L i = halt tell(inc n ) next tell(out(l j )) if L i = c n := c n + 1; goto L j when isz n do next tell(out(l j )) if L i = if c n = 0 then goto L j unless isz n next (tell(dec n ) else c n := c n -1;goto L k next tell(out(l k )))
Without loss of generality assume that counters are initially set to 0. The program takes the form:

[[M (0, 0)]] = (local l 1 , . . . , l n ) (tell(out(l s )) c 0 c 1 tell(isz 0 ) tell(isz 1 ) [[L 1 ]] ... [[L n ]])
Let Dec n be the process decrementing n times the counter c 0 . If it succeeds, it outputs the constraint yes:

Dec 0 = when isz 0 do tell(yes) Dec n = unless isz 0 next (tell(dec 0 ) Dec n-1 )
For the correctness of the construction, one can verify that M (0, 0) computes the value n if and only if after the encoding halts one can decrement c 0 exactly n times until telling "yes". More precisely:

Theorem 2 (Correctness). A Minsky machine M (0, 0) computes the value n iff ([[M (0, 0)]] whenever halt do Dec n ) ⇓ yes
As an application of the above construction we can show the undecidability of the input-output equivalence for well-terminated processes.

Given M (0, 0) we define [[M (0, 0)]] ′ as the above encoding [[M (0, 0)]] except that ins(halt) = skip-notice that ins(halt

) = tell(halt) in [[M (0, 0)]]. Clearly, M (0, 0) does not halt iff [[M (0, 0)]] ′ ∼ io [[M (0, 0)]].
We then obtain the following corollary.

Corollary 1. Fix the underling constraint system to be monadic first-order logic without equality nor function symbols. Then, the question of whether P ∼ io Q, given two well-terminated processes P and Q, is undecidable.

A more compelling application of the above construction is given in the next section. In fact, the following result is the main application of the paper.

Application: Undecidability of monadic FLTL

In this section we shall state a new undecidability result for monadic FLTL as an application of the above Minsky encoding and the logic characterization of utcc in [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF].

FLTL Characterization. We first need to recall the FLTL characterization of utcc [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF].

Definition 10. Let [[•]
] a map from utcc processes to FLTL formulae given by:

[[skip]] = true [[tell(c)]] = c [[(abs y; c) P ]] = ∀ y(c ⇒ [[P ]]) [[P Q]] = [[P ]] ∧ [[Q]] [[(local x; c) P ]] = ∃ x(c ∧ [[P ]]) [[next P ]] = •[[P ]] [[unless c next P ]] = c ∨ •[[P ]] [[! P ]] = ✷[[P ]]
The compositional encoding in Definition 10 gives a pleasant correspondence between utcc processes and FLTL formulae.

Theorem 3 (Logic Correspondence [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF]). Let [[•]] as in Definition 10 and ⊢ T as in Definition 3. If P is a well-terminated process and c a state formula then

[[P ]] ⊢ T ✸c iff P ⇓ c .
It should be noticed that the encoding of Minsky machines in the previous section uses only well-terminated processes.

Quantification of flexible variables. In [START_REF] Merz | Decidability and incompleteness results for first-order temporal logics of linear time[END_REF] a FLTL named TLV is studied. The logic we present in Definition 1 differs from TLV only in that TLV disallows quantification of flexible variables as well as the past operator. We shall see that quantification over flexible variables is fundamental for our encoding of Minsky machines. We also state in Corollary 2 that the past-free monadic fragment of the FLTL in Section 2 without equality nor function symbols is strongly incomplete. This in contrast with the same TLV fragment which is decidable wrt validity [START_REF] Merz | Decidability and incompleteness results for first-order temporal logics of linear time[END_REF].

Because of the above-mentioned difference with TLV we shall use the following notation:

Notation 3 Henceforth we use TLV-flex to denote the past-free fragment of the FLTL presented in Section 2, i.e., the set of FLTL formulae without occurrences of the past modality ⊖.

In [START_REF] Merz | Decidability and incompleteness results for first-order temporal logics of linear time[END_REF] it is proven that the problem of validity of a monadic TLV formula A without equality and function symbols is decidable. This decidability result is proven the same way as the standard decidability result for classical monadic first-order logic-By getting rid of quantifiers and reducing the problem to the decidability of propositional LTL.

Nevertheless, quantification of flexible variables makes impossible to obtain a prenex form of a formula which may then allows us to get rid of quantifiers as it can be done for monadic first-order logic. Consider for example the unary predicate p c (x) testing if x is equal to a constant c. Take the formula F = (p c (x) ∧ •¬p c (x)). If x is a flexible variable, notice that ∃xF is satisfiable whereas ∃x F is not. Hence, moving quantifier to the outermost position to get a prenex form does not preserve satisfiability. Notice also that if x is a rigid variable instead, ∃xF and ∃x F are both logically equivalent to false.

The following proposition follows from composing the encodings from Minsky machines into utcc and from utcc into FLTL. To see the importance of quantifying over flexible variables in the encoding A = [[P ]], take the output of a in line 3 of the encoding P = [[M (0, 0)]] and assume that a is rigid. Notice that abstraction in line 4 is replicated, thus corresponding to a formula of the form ∀ z out 1 n (z) ⇒ F . Once the formula out 1 n (a) is true, by the rigidity of a, the formula F [a/z] must be true in the following states, which does not correspond to the intended meaning of the machine execution. Instead, if a is flexible, the fact that out 1 n (a) is true at certain state does not imply that F [a/z] must be true in the subsequent states. Now with the help of the above proposition and the encoding we obtain the following:

Proposition 2. Given a Minsky machine M (0, 0), it is possible to construct a monadic TLV-flex formula without equality and function symbols F M s.t F M is valid iff M (0, 0) loops (i.e., it never halts).

Let M (0, 0) be a Minsky machine. Let P = [[M (0, 0)]] ′′ where [[M (0, 0)]] ′′ is defined as the encoding [[M (0, 0)]] in Section 4.1 except that ins(•) adds tell(running) in parallel to the encoding of all instructions but halt. For the above proposition, we can then take F M = A ⇒ running, where A = [[P ]] and [[P ]] as given in Definition 10.

Since the set of looping Minsky machines (i.e. the complement of the halting problem) is not recursively enumerable, a finitistic axiomatization of monadic TLV-flex without equality and function symbols would yield to a recursively enumerable set of tautologies. Therefore such a logic is strongly incomplete.

Corollary 2 (Incompleteness). Monadic TLV-flex without equality and function symbols is strongly incomplete.

From this corollary it follows that the validity problem in the above-mentioned monadic fragment of TLV-flex is undecidable.

Closure-Operator Semantics

In the previous section we showed that utcc processes can represent Minsky machines. In this section we show that utcc processes can be represented as partial closure operators.

More precisely, we shall give a compositional characterization of the inputoutput behavior of utcc processes in terms of (partial) closure operators. We build on the closure operator semantics in [START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF] for tcc. Because of additional technical difficulties posed by the abstraction operator of utcc, the codomain of the closure-operators is more involved than that for tcc. Namely, instead of sequences of constraints as in tcc, we shall use sequences of future-free temporal formulae (constraints).

The proposed denotational semantics takes into account also non well-terminated processes (Definition 9). Consequently, we shall use the alternative symbolic reduction semantics in [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF] which deals with the infinite internal computation problems discussed in Section 3.2 (Remark 2).

Symbolic Semantics

Here we recall the symbolic reduction semantics in [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF]. Intuitively, the symbolic observable reductions use temporal constraints to represent in a finite way a possibly infinite number of substitutions as well as the information that an infinite loop may provide. This semantics guarantees that every sequence of internal transitions is finite.

Before defining the symbolic semantics let us give some intuitions of its basic principles.

A. Substitutions as Constraints. Take R = (abs x; c) P. B. Timed Dependencies in Substitutions. The symbolic semantics represents as temporal constraints dependencies between substitutions from one time interval to another. E.g., suppose that for R above, P = next tell(c ′ ). Operationally, once we move to the next time unit, the constraints produced are of the form c ′ [t/x] for those t's s.t the final store d in the previous time unit entails c[t/x]. The symbolic semantics captures this as e ′ = (⊖d) ∧ ∀x((⊖c) ⇒ c ′ ) where ⊖ is the "previous" (or "past") modality in FLTL (see Section 2).

For the symbolic semantics we then use the Future-free fragment of the FLTL in Definition 1.

Definition 11 (Future-free constraints). A temporal formula is said to be future-free iff it does not contain occurrences of and •. We shall use e, e ′ ... to range over future-free formulae and w, w ′ , v, v ′ , . . . to range over infinite sequences of future-free formulae. Notice that every constraint (i.e., state formula) is a future-free formula.

We shall assume that processes and configurations are extended to include future-free formulae rather than just constraints (state formulae). So, for example a process-store configuration of the form (abs y; ⊖c) P, ⊖d may appear in the transitions of the symbolic semantics.

Symbolic Reductions. The internal and observable symbolic transitions -→ s , =⇒ s are defined as in Table 1 with ⊢ replaced by ⊢ T and with R A and R O replaced by R As and R Os in Table 2 resp.

The rule R As represents with the temporal constraint ∀ x(e ⇒ e ′ ) the substitutions that its operational counterpart R A would induce. Notice that in the reduction of P the variables x in e are hidden, via existential quantification, to avoid clashes with those in P .

The function F s in R Os is similar to its operational counterpart F in Definition 7. However, F s records the final global and local stores as well as abstraction guards as past information. As explained before, this past information is needed in next time unit. Definition 12. Let F s be a partial function from configurations to processes defined by F s (P, e) = tell(⊖e) F ′ (P ) where:

F ′ (P ) =                skip if P = skip (abs x; ⊖e) F ′ (Q) if P = (abs x; e) Q F ′ (P 1 ) F ′ (P 2 ) if P = P 1 P 2 (local x; ⊖e) F ′ (Q) if P = (local x; e) Q Q if P = next Q Q if P = unless c next Q
Clearly, no infinite sequence of internal transitions γ 1 -→ s γ 2 -→ s . . . can be generated by the symbolic semantics.

We now define the input-output behavior and equivalence for the symbolic reduction semantics.

Definition 13 (Symbolic Relations). Let e and e ′ be future-free formulae.

We write e e ′ whenever e ⊢ T e ′ . If e e ′ and e ′ e we write e ≈ e ′ . If e e ′ and e ≈ e ′ then we write e ≻ e ′ . We extend , ≻ and ≈ to sequences of future-free formulae: w

v (w ≻ v, w ≈ v) iff for all i > 0, w(i) v(i) (w(i) ≻ v(i), w(i) ≈ v(i)). If P = P 1 (e1,e ′ 1 ) ====⇒ s P 2 (e2,e ′ 2 )
====⇒ s ..., we write P (w,w ′ )

====⇒ s where w = e 1 .e 2 ... and w ′ = e ′ 1 .e ′ 2 ... The symbolic input-output behavior io s (P ) is defined as the set

{(w, w ′ ) | P (w,w ′ ) ====⇒ s } modulo ≈ . We write P ∼ io s Q iff io s (P ) = io s (Q).
As shown in [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF], the symbolic reduction semantics and the SOS coincide for the fragment of abstracted-unless free processes: Definition 14 (Abstracted-unless free Processes). We say that P is abstractedunless free if it has no occurrences of processes of the form unless c next Q where c or Q has occurrences of variables under the scope of an abstraction.

The correspondence is confined to this fragment of the calculus due to the problem of representing the negation of entailment as logic formulae (see [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF] for further details).

Theorem 4 (Semantic Correspondence [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF]). Let P be an abstracted-unless free process. Suppose that P (c1,d1)

====⇒ P 1 (c2,d2) ====⇒ . . . (ci,di) ====⇒ P i and P (c1,e1) ====⇒ s P 1 ′ (c2,e2) ====⇒ s . . . (ci,ei) ====⇒ P ′ i .
Then for every c ∈ C and j ∈ {1, . . . , i}, d j ⊢ c iff e j ⊢ T c.

Monotonic fragment and closure operators

In this section we show that io s (P ) is a partial closure operator-see Section 2. Notice that the "unless" operator unlike the other constructs in utcc exhibits non-monotonic input-output behavior in the following sense: Given w w ′ and P = unless c next Q, if (w, v), (w ′ , v ′ ) ∈ io s (P ), it may be the case that v ′ v. E.g., take Q = tell(d), w = c. true ω and w ′ = true ω . Definition 15 (Monotonic Processes). We say that P is a monotonic process iff P does not have occurrences of processes of the form unless c next Q.

In fact, for a monotonic process P, io s (P ) is a closure operator. The next proposition basically follows from the corresponding closure-operator properties for internal symbolic transition which in turn can be proven by induction on the (depth of) derivation of internal symbolic transitions.

Proposition 3 (Closure Properties). Let P be an arbitrary utcc process. We have the following:

-Extensiveness: If (w, w ′ ) ∈ io s (P ) then w ′ w -Idempotence: If (w, w ′ ) ∈ io s (P ) then (w ′ , w ′ ) ∈ io s (P ) -Monotonicity: if P is monotonic, (w 1 , w 2 ) ∈ io s (P ) and w ′ 1 w 1 , then there exists w ′ 2 such that (w ′ 1 , w ′ 2 ) ∈ io s (P ) and w ′ 2 w 2 .

A pleasant property of closure operators is that they are uniquely determined by its set of fixed points; here referred to as strongest postcondition.

Definition 16 (Strongest Postcondition). Given a utcc process P , the set sp s (P ) = {w | (w, w) ∈ io s (P )} denotes the strongest postcondition of P . Moreover, if w ∈ sp s (P ), we say that w is a quiescent sequent for P , i.e. P under input w cannot add any information whatsoever. Define P ∼ sp s Q iff sp s (P ) = sp s (Q). Recall that the symbolic semantics transfers the final store of a time-unit to the next one as a past formula (Definition 12). Therefore, for any process P , if s ∈ sp s (P ) then s is a past-monotonic sequence in the following sense.

Definition 17 (Past-Monotonic Sequences, PM). We say that an infinite sequence of future-free formulae w is past-monotonic iff for all i > 1, w(i) ⊢ T ⊖w(i -1). The set of infinite sequences of past-monotonic formulae is denoted by PM .

Before relating the input-output behavior with the strongest postcondition of a process, we need to introduce the following notation.

Notation 4

The upper closure of a future-free formula e is the set {e ′ | e ′ e} and we write ↑ e. We extend this notion to sequences by decreeing that ↑ w = {w ′ | w ′ w}.

The input-output behavior of a monotonic process can be retrieved from its strongest postcondition. This characterization is expressed by the following corollary, whose proof is standard, given that io s (P ) is a closure operator.

Corollary 3. Let min be the minimum function wrt the order induced by . Given a monotonic utcc process P , (w, w ′ ) ∈ io s (P ) iff w ′ = min(sp s (P )∩ ↑ w) Therefore to characterize the input-output behavior of P , it suffices to specify sp s (P ). In the next section we give a denotational semantics [[•]] that aims at specifying sp s (•) compositionally.

Denotational Model

This section presents a denotational model for the strongest postcondition of utcc processes. This semantics is built on the closure operator semantics for tcc in [START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF]. We will briefly discuss the technical problems in giving a closure operator semantics for the abstraction process.

We need the following notations.

Notation 5 Given the sequence of variables x = x 1 , ..., x n , ∃ x stands for the expression ∃ x1 ∃ x2 ...∃ xn . We shall use ∃ x w to denote the sequence obtained by pointwise applying ∃ x to each constraint in w. Similarly, w ∧ w ′ denotes the sequence v such that v(i) = w(i) ∧ w ′ (i) for i > 0. Abusing of the notation, for x / ∈ fv (w) we understand that none of the variables in x occurs free in the constraints of w.

The equations for the local and abstraction operators involve the notion of x-variants. Basically, two formulae (or sequences of formulae) are x-variant if they are the same except for the information about the variables in x. Formally: Definition 18 ( x-variant). We say that e and e ′ are x-variants if ∃ x e = ∃ x e ′ . Similarly, the sequence w is an x-variant of the sequence w ′ iff ∃ x w = ∃ x w ′ .

The denotational semantics is defined as a function [[•]] which associates to each process a set of infinite sequences of past-monotonic formulae, namely [[•]] : Proc → P(PM ). The definition of [[•]

] is given in Figure 1. Recall that [[P ]] is meant to capture the quiescent sequences of P ; those sequences P cannot add any information whatsoever-i.e., the strongest postcondition of P .

Let us first give some intuition about the semantics of processes that do not bind variables. So, skip cannot add any information to any sequence in PM (D S ). The sequences to which tell(c) cannot add information are those whose first element can entail c (D T ). A sequence is quiescent for P Q if it is for P and Q (D P ). Process next P has not influence in the first element of a sequence, thus e.w is quiescent for it if w is quiescent for P (D N ). A similar explanation can be given for the process unless c next P (D U ). A sequence is quiescent for ! P if every suffix of it is quiescent for P (D R ).

We now consider the binding processes. A sequence w is quiescent for Q = (local x; c) P if there exists an x-variant w ′ of w s.t. w ′ is quiescent for P . Hence, if P cannot add any information to w ′ then Q cannot add any information to w. To see this notice that w and w ′ are x-variants; i.e., they are the same except possibly on the information about the variables in x. Clearly Q cannot add any information on (the global variables) x appearing in w. So, if Q were to add information to w, then P could also do the same to w ′ . But the latter is not possible since w ′ is quiescent for P . Now, we may then expect that the semantics for the abstraction can be straightforwardly obtained in a similar fashion by quantifying over all possible x-variants. Nevertheless, this is not the case as we shall illustrate below.

Denotation of Abstraction Using x-variants

Recall that the ask tcc process when c do Q is a shorthand for the empty abstraction process (abs ǫ; c) Q (Notation 1). Recall also that T denotes the set of all terms in the underlying constraint system. The first intuition for the denotation of the process P = (abs x; c) Q is given with the following equation.

t∈T | x| [[(when c do Q)[ t/ x]]]
where [[when c do Q]] is the usual denotational equation for the ask processes in tcc, i.e.

[[when c do

Q]] = {w | w(1) ⊢ T c implies w ∈ [[Q]]}
This equation arises directly from the fact that P can be viewed as the (possibly infinite) parallel composition of the processes (when c do Q)[ t/ x] for every sequence of terms t ∈ T | x| .

Nevertheless we can give a denotational equation for abstraction which is analogous to that of the local operator. By using the notion of x-variants the equation does not appeal to substitution as the one above. As illustrated below the denotation of abstraction is not entirely dual to the denotation of the local operator. The lack of duality between D L and D A is reminiscent of the result in CCP [START_REF] De Boer | Proving concurrent constraint programs correct[END_REF] stating that negation does not correspond exactly to the complementation (See [START_REF] Cortesi | Complementation in abstract interpretation[END_REF][START_REF] De Boer | Proving concurrent constraint programs correct[END_REF]).

Notation 6 Given a sequence e 1 .e 2 ..., we use e 1 .e 2 ... to denote the past-monotonic sequence e 1 .(e 2 ∧ ⊖e 1 ).(e 3 ∧ ⊖e 2 ∧ ⊖ 2 e 1 )..

Example 2. Let Q = (abs x; c) P where c = out (x) and P = tell(out ′ (x)). Take the past-monotonic sequence

w = (out(0) ∧ out ′ (0)). true ω ∈ sp s (Q).
Suppose that we were to give the following definition of [[Q]]:

{w | for every x-variant w ′ of w if w ′ (1) ⊢ T c then w ′ ∈ [[P ]]}
Let 0 be a term. Notice that we have an x-variant

w ′ = (out(0) ∧ out ′ (0) ∧ out(x)). true ω of w s.t. w ′ (1) ⊢ T c but w ′ / ∈ [[P ]]. Then w / ∈ [[Q]] under this naive definition of [[Q]].
We fix the above definition in Equation D A by using the following condition

w ′ ( x = t) ω .
for a sequence of terms t s.t. | t| = | x| and t . = x. Intuitively, this condition together with w ′ (1) ⊢ T c requires that w ′ (1) ⊢ T c∧ x = t and hence that w ′ (1) ⊢ T cσ for a substitution σ = [ t/ x]. Furthermore w ′ ( x = t) ω together with w ′ ∈ [[P ]] realizes the operational intuition that P runs under the substitution σ. In fact the denotation satisfies the following:

Proposition 4. Let [[•]] as in Figure 1 and Q = (abs x; c) P . w ∈ [[Q]] iff w ∈ t∈T | x| [[(when c do P )[ t/ x]]] DS [[skip]] = PM DT[[tell(c)]] = {e.w ∈ PM | e ⊢T c} DP[[P Q]] = [[P ]] ∩ [[Q]] DN[[next P ]] = {e.w ∈ PM | w ∈ [[P ]]} DU[[unless c next P ]] = {e.w ∈ PM | e ⊢T c and w ∈ [[P ]]}∪ {e.w ∈ PM | e ⊢T c} DR[[! P ]] = {w ∈ PM | for all v, v ′ s.t. w = v.v ′ , v ′ ∈ [[P ]]} DL [[(local x; c) P ]] = {w ∈ PM | there exists an x-variant w ′ of w s.t w ′ (

Full-abstraction

In this section we show the correspondence between the symbolic reduction semantics of utcc and the denotational one.

Soundness. The soundness of the denotation holds for the abstracted-unless free fragment of utcc (see Definition 14). The technical reason is that in proving sp s (P ) ⊆ [[P ]] for P = (abs x; c) Q where x ∈ f v(Q) we need Q to be monotonic (Definition 15).

Theorem 5 (Soundness). Given an abstracted-unless free process P , sp s (P ) ⊆

[[P ]]
The proof of the above theorem proceeds by induction on the size of P . Here we only outline the main steps of the abstraction case P = (abs x; c) Q -the other cases proceed as in [START_REF] Nielsen | Temporal concurrent constraint programming: Denotation, logic and applications[END_REF]. As a mean of contradiction assume that w ∈ sp s (P ) and w / ∈ [[P ]]. By using alpha-conversion we can assume that x / ∈ fv (w). Since

w / ∈ [[P ]] then let w ′ be an x-variant of w s.t. w ′ (1) ⊢ T c, w ′ ( x = t) ω with x . = t and w ′ / ∈ [[Q]]
. By hypothesis w ′ ∈ sp s (Q). Since P is abstracted-unless free then Q is a monotonic process and thus

Q (w ′ ,v ′ )
====⇒ s for a v ′ ≻ w ′ . We can now use the facts that w ′ ( x = t) ω and that w ′ is an x-variant of w to verify that (Q

! tell( x = t)) (w ′ ,v ′ ) ====⇒ s and thus that R = (local x) (Q ! tell( x = t)) (w,∃ x v ′ ) ====⇒ s . We then show that R ∼ io s Q[ t/ x] and hence (w, ∃ x v ′ ) ∈ io s (Q[ t/ x]). Since w and w ′ are x-variants, x / ∈ fv (w) and v ′ ≻ w ′ then ∃ x v ′ ≻ w. Therefore, w / ∈ sp s (Q[ t/ x])
Notice that because w ′ (1) ⊢ T c and w ′ ( x = t) ω we have w ′ (1) ⊢ T c[ t/ x], and thus w(1) ⊢ T c[ t/ x] since w and w ′ are x-variants. This leads to a contradiction by verifying that for all w, t if w ∈ sp s (P ) and w(1) ⊢ T c[ t/ x] it must be the case that w ∈ sp s (Q[ t/ x]).

Completeness. For completeness we have similar technical problems that in the case of tcc [START_REF] Nielsen | Temporal concurrent constraint programming: Denotation, logic and applications[END_REF] namely: the combination between the local and the "unless" operator-see [START_REF] Nielsen | Temporal concurrent constraint programming: Denotation, logic and applications[END_REF] for details. Thus as in [START_REF] Nielsen | Temporal concurrent constraint programming: Denotation, logic and applications[END_REF] the full abstraction is achieved only for the locally independent fragment.

Definition 19 (Locally Independent Processes). We say that P is locally independent iff P has no occurrences of processes of the form unless c next Q under the scope of a local operator.

The use of the abstracted-unless free condition in the completeness result is analogous to that for soundness. Theorem 6 (Completeness). Given a locally independent and abstracted-unless free process P , [[P ]] ⊆ sp s (P ) Similar to the case of soundness, the proof of completeness proceeds by induction on the size of P . Here we only outline the main steps of the abstraction case P = (abs x; c) Q. As a mean of contradiction assume that w ∈ [[P ]] and w / ∈ sp s (P ). By alpha-conversion we can assume that x / ∈ fv (w). Since w / ∈ sp s (P ) then one can verify that we have a t . = x s.t. w(1) ⊢ c[ t/ x] and

w / ∈ sp s (Q[ t/ x]). Let w ′ = w ∧ ( x = t) ω . Notice that w ′ is an x-variant of w because x / ∈ fv (w). Thus, since w(1) ⊢ T c[ t/ x] then w ′ (1) ⊢ T c[ t/ x]. From w ∈ [[P ]], and Equation D A , w ′ ∈ [[Q]]
and by hypothesis w ′ ∈ sp s (Q). Using Rule R As and the fact that w / ∈ sp s (P ), we can show that w / ∈ sp s (Q). Since

w ′ ∈ sp s (Q) then Q (w ′ ,w ′ ) ====⇒ s .
From this we can verify that (Q ! tell( x = t))

(w ′ ,w ′ ) ====⇒ s and Q[ t/ x] (w,w) ====⇒ s . Therefore, w ∈ sp s (Q[ t/ x]), a contradiction.
Full Abstraction. From Corollary 3, soundness and completeness, we can derive the following full-abstraction result.

Corollary 4 (Full abstraction). Let P and Q be locally independent and monotonic processes and [[•]] as in Figure 1. Then

P ∼ io s Q iff [[P ]] = [[Q]]
. Therefore, the input-output behavior of the monotonic locally-independent fragment of utcc can be compositionally specified in terms of closure operators. To illustrate the applicability of this fragment, in the next section we shall identify a language for security protocols whose semantics can be given in terms of this kind of closure operators. Remark 3. Notice that the connection between the operational semantics and the denotational semantics for well-terminated processes follows from Theorem 4 and the soundness and completeness results in this section.

Application: A security process language

Cryptographic protocols aims at communicating agents securely over an untrusted network. Several process languages have been defined to analyze these protocols [START_REF] Crazzolara | Petri nets in cryptographic protocols[END_REF][START_REF] Abadi | A calculus for cryptographic protocols: The spi calculus[END_REF][START_REF] Amadio | On the symbolic reduction of processes with cryptographic functions[END_REF][START_REF] Boreale | A method for symbolic analysis of security protocols[END_REF]. Typically, these calculi provide a mechanism for communication of private names (nonces) and they are parametric in an entailment relation over a logic for reasoning about cryptographic properties.

In this section we show how the monotonic locally-independent fragment of utcc and its closure operator characterization can be used to give meaning to a process language enjoying the typical features of calculi for security mentioned above. This language arises as specialization of utcc with a particular cryptographic constraint systems. We will show that processes in the language can be compositionally specified as closure operators. So, e.g., the set of messages a protocol may produce can be represented as a closure operator over sequences of constraints. The least fixed point of this operator may be used to verify if a secrecy property is not verified by the protocol.

The modeling language: SCCP We shall use a syntax of processes following that of SPL [START_REF] Crazzolara | Petri nets in cryptographic protocols[END_REF]. Basically, this language offers primitives to output and receive messages as well as to generate secrets or nonces (randomly-generated unguessable items).

Definition 20 (Syntax of SCCP).

Values

v, v ′ ::= n |x Keys k ::= pub(v) | priv (v) Messages M, N ::= v | k | X | (M, N ) | {M } k Patterns Π, Π ′ ::= v | k | X | (Π, Π ′ ) Processes R ::= nil |new(x)R |out(M ).R |in [M > Π].R |!R |R R
We shall refer to the language given by the above syntax as SCCP (Security Concurrent Constraint Programming Language). The language includes a set of names (values) with n, m, A, B ranging over it. These values represent ids of principals or nonces. The set of keys is built upon two constructors providing public (pub(v)) and the private key (priv (v)) associated to a value. Messages can be constructed from composition (M, N ) and encryption {M } k of messages. As explained below, message decomposition can be obtained by using pattern matching.

Intuitively, processes in SCCP run in time intervals. The output process out(M ).R broadcasts M over the network and then it behaves as R in the next time unit. The input in [M > Π].R waits for a message M that matches the pattern Π and binds the variables occurring in the pattern and then it behaves like R in the next time unit. For example, for every message of the form (N, N ′ ) pub(A) , the process in [{M } pub (A) > (x, y)].R executes R[N/x, N ′ /y] in the next time unit. The process new(x)R generates a (nonce) x private to R. The process nil does nothing; R R ′ denotes the parallel execution of R and R ′ . Finally !R denotes the execution of R in each time unit. Dolev-Yao Constraint System. Typically in the modeling of security protocols one must take into account all possible actions the attacker may perform. This attacker is usually given in terms of the Dolev and Yao thread model [START_REF] Fiore | Computing symbolic models for verifying cryptographic protocols[END_REF] which presupposes an attacker that can eavesdrop, disassemble, compose, encrypt and decrypt messages with available keys. It also presupposes that cryptography is unbreakable.

Before giving a closure operator semantics to our security language, we then need a constraint system handling the cryptographic constructs (e.g. encryption, message composition, etc) and whose entailment relation follows the inferences a Dolev-Yao attacker may perform. Definition 21. Let Σ s be a signature with constant symbols in V, function symbols enc, pair , priv and pub and unary predicate out. Let ∆ s be the closure under deduction of { F | ⊢ s F } with ⊢ s as in Table 3. The (secure) constraint system is the pair (Σ s , ∆ s ). Intuitively, V represents the set of principal ids, nonces and values. We use {m} k and (m 1 , m 2 ) resp., for enc(m, k) (encryption) and pair (m 1 , m 2 )(composition). Rule ENC says that if one can infer that the message m as well as a key k are output on the global channel out, then one may as well infer that {m} k is also output on out. The other rules can be explained similarly.

A Protocol in SCCP To illustrate the language consider the following simplification of the Denning-Sacco key distribution protocol [START_REF] Denning | Timestamps in key distribution protocols[END_REF]:

msg 1 A → B : {(A, m)} pub(B) msg 2 B → A : {n} pub(m)
This protocol involves two principals A and B. In the first step, A sends to B the message {A, m} pub(B) representing the composition of the A's identifier and the nonce m encrypted with the B's public key. With its private key, B decrypts the message sent by A and he sends a new nonce n encrypted with the public key generated from m. The property that must be verified is that only A and B can know n.

Assume the following execution of the protocol between A, B and C. Here C is an intruder, i.e. a malicious agent playing the role of a principal in the protocol.

msg 1 A → C : {(A, m)} pub (C) msg ′ 1 C → B : {(A, m)} pub (B) msg 2 B → A : {n} pub(m)
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 nonce m from the first message, he can decrypt the message {n} pub (m) and n is not longer a secret between A and B as intended.

We model the behavior of the initiator and the responder in our running example as follows:

Init(A, B) ≡ ! new(m) out({(A, m)} pub(B) ).nil Resp(B) ≡ ! in [M > {(x, u)} pub(B) ]. new(n) out({n} pub (u) ).nil Spy ≡ A∈P ! out(A).nil A∈P ! out(pub(A)).nil A∈Bad ! out(priv (A)).nil
The process Spy corresponds to the initial knowledge the attacker has. Given the set of principals of the protocol P, the spy knows all the names of the principals in the protocol and their public keys. He also knows a set of private keys denoted by Bad. This set represents the leaked keys, for example, the private key of C in the above configuration exhibiting the secrecy flaw. Notice that the processes Init and Resp are replicated. This models the fact that principal may initiate different sessions during the execution of the protocol.

Closure Operators for SCCP The following definition interprets SCCP processes as monotonic utcc processes. Definition 22. Let I be a function from SCCP to monotonic utcc processes defined by:

I =                skip if R = nil (local x) I (R ′ ) if R = new(x)R ′ ! tell(out(M )) next I (R ′ ) if R = out(M ).R ′ (abs x; c) next I (R ′ ) if R = in [M > Π].R ′ i∈I I (R i ) if R = i∈I R i ! I (R ′ ) if R =! R ′ where x = fv (Π) and c = out (M ) ∧ (M = Π).
It is easy to see that the above interpretation realizes the behavioral intuition of SCCP given before. Intuitively the output out(M ) is mapped to a process adding the constraint out (M ). Since the final store in utcc is not automatically transferred to the next time interval, the process tell(out(M )) is replicated. This reflects the fact that the attacker can remember all the messages posted over the network.

For the case of inputs, we use the guard of the abstraction operator to check if the input received matches with the pattern Π. Take for example Resp(B) in our example. This process is interpreted via I above as: ! (abs x, u; out({M } pub(B) ) ∧ M = (x, w)) next Q where Q = I (new(n)out({n}) pub(u) .nil). When a constraint of the form out({(N, N ′ )} pub(B) ) can be deduced from the current store, the process Q[N/x, N ′ /y] is executed in the next time unit as expected.

The following function maps our security processes into its set of fixed points as specified in Figure 1-i Modeling Secrecy Properties. We can represent protocols in such a way that potential attacks can be specified as the least fixed point of the closure operators representing them. To detect when the secret created by Resp is revealed by the attacker, we modify the definition of this process as follows:

Resp ′ (B) ≡ ! in [M > {(x, u)} pub(B) ]. new(n)(out({n} pub(u) ).nil) ! in [Y > n].out(attack).nil)
Intuitively, Resp ′ outputs the message attack when the message n appears unencrypted on the network, i.e., when out(n) can be deduced from the current store.

Recall that false is an absorbing element for conjunction and it is the greatest future-free formulae wrt . Our approach is then to add the constraint false when the message attack can be read from the network. In terms of the closure operator semantics it implies that if a process R outputs the message attack, then the least fixed point of the closure operator representing R is a sequence whose suffix is the sequence false ω . More precisely, Proposition 5. Let R be a SCCP process. Let f be defined as

[[R]] SCCP ∩ [[! when out(attack) do ! tell(false)]]
Therefore, I (R) ⇓ attack iff the least-fixed point of the closure operator corresponding to f takes the form w. false ω

The previous proposition allows us to exhibit the secrecy flaw in our running example. I.e., let P = {A, B, C} be the set of principal names and Bad = {C} be the set of leaked keys in our previous protocol example. Given the process DS = Init(A, C) X∈P Resp ′ (X) and

f = [[DS]] SCCP ∩ [[! when out(attack) do !tell(false)]]
The least fixed point v of f takes the form v = w. false ω .

Closure Properties of a Spy. We conclude this section by pointing out that the interpretation of the behavior of protocols as closure operators is a natural one. To see our intuition, let us suppose that f is a closure operator denoting a SCCP Spy eavesdropping and producing information in the network.

f (w) w: The Spy produces new information from the one he obtains.

-If w v then f (w) f (v): The more information the Spy gets, the more he will infer. -f (f (w)) = f (w): The Spy infers as much as possible from the info he gets.

Concluding Remarks and Related Work

We showed that unlike the processes of its predecessor tcc, utcc processes can represent Turing-powerful formalisms. As an application we showed the undecidability of monadic FLTL without function symbols nor equality. We also showed that like for tcc processes, utcc can be represented as partial closure operators. As an application we identify a language for security in which protocols can be represented as closure operators. The language arose as a specialization of utcc in a particular cryptographic constraint system.

Expressiveness of TCC and FLTL. The expressivity of CCP-based languages has been explored in [START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF][START_REF] Nielsen | On the expressive power of temporal concurrent constraint programming languages[END_REF][START_REF] Valencia | Decidability of infinite-state timed ccp processes and first-order ltl[END_REF]. These works show that tcc processes are finitestate. The results in [START_REF] Nielsen | On the expressive power of temporal concurrent constraint programming languages[END_REF] also imply that the processes of the extension of tcc with arbitrary recursive definitions are not finite-state. Nevertheless these results do not imply that they can encode Turing-expressive formalisms.

There are several works addressing the decidability of fragments of FLTL. In Section 4 we already discussed that in [START_REF] Merz | Decidability and incompleteness results for first-order temporal logics of linear time[END_REF] showing that the validity problem in monadic TLV without equality and function symbols is decidable. As mentioned before, TLV unlike TLV-flex does not allow quantification over flexible variables. Our decidability results justifies the imposition of this quantification restriction.

The work in [START_REF] Nielsen | On the expressive power of temporal concurrent constraint programming languages[END_REF] shows the decidability of the satisfiability problem restricted to negation-free TLV-flex formulae. It was also suggested in [START_REF] Nielsen | On the expressive power of temporal concurrent constraint programming languages[END_REF] that one could dispense with this restriction. This paper refutes this since in the absence of this restriction one can obviously define universal quantification (not present in the negation-free fragment of [START_REF] Nielsen | On the expressive power of temporal concurrent constraint programming languages[END_REF]) and then be able to reproduce the encoding of looping Minsky machines here presented.

Based on the undecidability result of TLV(∅) [START_REF] Szalas | Incompleteness of first-order temporal logic with until[END_REF] (i.e. TLV with the empty set of predicates), [START_REF] Merz | Decidability and incompleteness results for first-order temporal logics of linear time[END_REF] proves an incompleteness result for monadic without equality and function symbols TLP logic. Unlike TLV, in TLP the interpretation of the predicates is flexible (state dependent) and all the variables are rigid. [START_REF] Merz | Decidability and incompleteness results for first-order temporal logics of linear time[END_REF] also relates undecidability results of n-adic fragments of TLP with undecidability results of n + 1-adic fragments of TLV. Thus adding binary predicates turns TLV strongly incomplete. In [START_REF] Hodkinson | Decidable fragment of firstorder temporal logics[END_REF] the monodic fragment of FLTL is introduced. A formula is monodic if every subformulae beginning with a temporal operator have at most one free variable. In this case the authors use a TLP-like semantics and conclude that the set of valid formulae in the 2-variable monadic fragment (i.e. monadic formulae with at most 2 distinct individual variables) is not recursively enumerable even considering finite domains in the interpretation. Nevertheless validity in the fragment of 2-variable monodic formulae is decidable. In [START_REF] Degtyarev | Equality and monodic first-order temporal logic[END_REF] these results are extended claiming the undecidability for validity in the monodic monadic 2-variable with equality fragment of TLP.

Closure-Operator Semantics and Security. As previously mentioned the closureoperator semantics for utcc builds on that for its predecessor tcc in [START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF] and [START_REF] Nielsen | Temporal concurrent constraint programming: Denotation, logic and applications[END_REF]. The denotation in these works map processes into sequences of constraints. Because of the technical difficulties posed by the abstraction operator our denotation maps instead processes into sequences of past-monotonic sequences of future-free FLTL formulae.

Several process languages have been defined to analyze security protocols. For instance Crazzolara and Winskel's SPL [START_REF] Crazzolara | Petri nets in cryptographic protocols[END_REF], the spi calculus variants by Abadi [START_REF] Abadi | A calculus for cryptographic protocols: The spi calculus[END_REF] and Amadio [START_REF] Amadio | On the symbolic reduction of processes with cryptographic functions[END_REF], and Boreale's calculus in [START_REF] Boreale | A method for symbolic analysis of security protocols[END_REF] are all operationally defined in terms of configurations containing items of information (messages) which can only increase during evolution. Such monotonic evolution of information is akin to the notion of monotonic store in CCP. Moreover, the calculi in [START_REF] Amadio | On the symbolic reduction of processes with cryptographic functions[END_REF][START_REF] Boreale | A method for symbolic analysis of security protocols[END_REF][START_REF] Fournet | Hiding names: Private authentication in the applied pi calculus[END_REF] are parametric in an entailment relation over a logic for reasoning about protocol properties very much like CCP is parametric in an entailment relation over an underlying constraint system.

Although utcc can be used to reason about certain aspects of security protocols (e.g., secrecy), it was not specifically designed for this application domain.

Here we illustrated how the closure operator semantics of utcc may offer new reasoning techniques for the verification of security protocols. We also argued for the closure operators as a natural characterization of the information that can be inferred (e.g., by Spy) from a protocol. Furthermore, the closure operator semantics presented here and the full abstraction theorem in Section 5.4 may allow us to tailor techniques based on behavioral equivalences, e.g. [START_REF] Abadi | A calculus for cryptographic protocols: The spi calculus[END_REF][START_REF] Fournet | Hiding names: Private authentication in the applied pi calculus[END_REF], for analyzing security protocols. An example modeling the Needham-Schroeder protocol in utcc was presented in [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF]. This example however uses non-monotonic processes which do not allow a closure-operator representation. To our knowledge closure operators had not been considered in the study of security protocols.

The successful logic programming approach to security protocols in [START_REF] Abadi | Analyzing Security Protocols with Secrecy Types and Logic Programs[END_REF] is closely related to ours. Basically, in [START_REF] Abadi | Analyzing Security Protocols with Secrecy Types and Logic Programs[END_REF] protocols are modeled as a set of Horn clauses rather than processes. The verification of the secrecy property relies in deducing (or proving that it is not possible) the predicate attack(M ) from the set of Horn clauses. A benefit from our approach is that we can overcome the problem of false attacks pointed in [START_REF] Blanchet | Security Protocols: From Linear to Classical Logic by Abstract Interpretation[END_REF]. E.g. Consider a piece data that needs to be kept secret in a first phase of the protocol and later is revealed when is not longer a secret. Because the lack of temporal dependency this may generate a false attack. The temporal approach presented here allows us to control when a message is required to be secret. The work in [START_REF] Blanchet | Security Protocols: From Linear to Classical Logic by Abstract Interpretation[END_REF] also avoid false attacks by using a linear logic approach rather than a temporal one.

5 whenever dec n ∨ inc n do 6 when

 56 dec n do next tell(out 2 n (z))|| 7 when inc n do next (local b) (tell(out 1 n (b))|| 7 ′ ! when out 2 n (b) do tell(out 1 n (z)))

Proposition 1 .

 1 Let M (0, 0) be a Minsky machine and P = [[M (0, 0)]] as defined in Section 4.1. Let A = [[P ]] be the FLTL formula obtained as in Definition 10. Then A is a monadic without equality and function symbols TLV-flex formula.

  RAsP, ∃ xe -→s Q, e ′′ ∧ ∃ xe (abs x; e ′ ) P, e -→s (abs x; e ′ ) Q, e ∧ ∀ x(e ′ ⇒ e ′′ ) ROs P, e -→ * s Q, e ′ -→s P (e,e ′ ) = = = =⇒s Fs(Q, e ′ )

1 )Fig. 1 .

 11 Fig. 1. Denotational Semantics for utcc. The function [[•]] is of type Proc → P(PM ). In DA, x = t denotes the constraint V 1≤i≤| x| xi = ti and t . = x stands for point-wise syntactic difference, i.e. V 1≤i≤| x| ti . = xi (see Sect. 2). If | x| = 0 then x = t and x . = t are defined as true.

PRJF

  ⊢s out((m1, m2)) i ∈ {1, 2} F ⊢s out(mi)PAIR F ⊢s out(m1) F ⊢s out(m2) F ⊢s out((m1, m2)) ENC F ⊢s out(m) F ⊢s out(k) F ⊢s out({m} k ) DEC F ⊢s out(priv (k)) F ⊢s out({m} pub(k) )F ⊢s out(m)

1 .

 1 .e., its strongest postcondition. Definition 23. For any SCCP process R we define [[R]] SCCP as [[I (R)]] with I (•) as in Definition 22 and [[•]] as in Fig. Since the interpretation function I is given in terms of the monotonic fragment of utcc, it follows from Section 5.4 that [[R]] SCCP corresponds to a closure operator.

  The operational semantics performs P [t/x] for every t s.t c[t/x] is entailed by the store d. Instead, the symbolic semantics dictates that R should produce e = d ∧ ∀x(c ⇒ d ′ ) where, similarly, d ′ should be produced according to the symbolic semantics by P . Let t be an arbitrary term s.t d ⊢ c[t/x]. The idea is that if e ′ is operationally produced by P [t/x] then e ′ should be entailed by d ′ [t/x]. Since d ⊢ c[t/x] then e ⊢ d ′ [t/x] ⊢ e ′ . Therefore e entails the constraint that any arbitrary P [t/x] produces.

Table 2 .

 2 Symbolic Rules for Internal and Observable Transitions. The function Fs is given in Definition 12.

Table 3 .

 3 Security constraint system entailment relation.