# Diferencias

Muestra las diferencias entre dos versiones de la página.

Enlace a la vista de comparación

grupos:avispa:ccp-wikipedia [2009/11/13 11:57]
caolarte
grupos:avispa:ccp-wikipedia [2011/01/24 15:30] (actual)
Línea 1: Línea 1:
+====== Concurrent Constraint Programming (CCP) ======

+Concurrent Constraint Programming (CCP) is a [[http://en.wikipedia.org/wiki/Process_calculus|process calculus]]  originally developed by [[http://www.saraswat.org/|Vijay A. Saraswat]] as a  powerful paradigm for concurrency tied to logic. CCP extends and subsumes both [[http://en.wikipedia.org/wiki/Logic_programming#Concurrent_logic_programming|concurrent logic programming]] and [[http://en.wikipedia.org/wiki/Constraint_logic_programming|constraint logic programming]]. A fundamental issue in CCP is the specification of [[http://en.wikipedia.org/wiki/Concurrent_system|concurrent systems]]
+by means of constraints. A constraint (e.g. x + y ≥ 10) represents
+partial information about certain variables. During the computation, the current
+state of the system is specified by a set of constraints called the **store**.
+Processes can change the state of the system by **telling** information to the store (i.e., adding constraints), and synchronize by **asking** information to the store (i.e., determining  whether a given constraint can be inferred from the store).
+
+===== Constraint Systems =====
+
+CCP calculi  are parametric in a //constraint system//. A constraint system provides:
+
+  - A **signature** from which the constraints can be constructed.
+  - An **entailment relation**  specifying inter-dependencies between constraints.
+
+A constraint represents then a piece of (partial) information upon  which processes may act. For instance, processes modeling temperature controllers may have to deal with partial information such as //42 < tsensor < 100//
+expressing that the sensor registers an unknown (or not precisely determined) temperature value between 42 and 100.
+The entailment relation {{ :grupos:avispa:ent-example.png |}} expresses that  from the information //tsensor>42// we can deduce (//entail//) the information //tsensor>0//.
+
+
+The notion of constraint system can be formalized by using First-Order Logic as in [ [[#References|Smo94]] ]. Alternatively, this can be given in terms of  [[http://en.wikipedia.org/wiki/Scott_information_system|Scott's information system]] without consistency structure as it was done in [ [[#References|Sar93]] ].
+===== Basic Constructs =====
+
+In the spirit of [[http://en.wikipedia.org/wiki/Process_calculus|process calculi]], the language of processes in  CCP is given by a small number of primitive operators or combinators. A typical CCP process language features the following operators:
+
+  * A **tell** operator  adding a constraint to the store.
+  *  An **ask** operator  querying if a constraint can be deduced from the store.
+  * **Parallel Composition**  combining processes  concurrently.
+  *  A **hiding** operator (also called //restriction// or //locality//)  introducing local variables.
+
+
+^Example: CCP Processes ^  |
+|{{ :grupos:avispa:ccp-anim.gif |}}|The processes **tell** (temperature>42) and **tell** (temperature <70) augment the information in the store. From the new store 42<temperature<70 it is possible to deduce that  0<temperature<100 and then **ask** (0<temperature<100) **then** Q evolves into Q. Since from  42<temperature<70 is not possible to deduce that temperature=50, the process **ask** (temperature=50) **then** P remains blocked until more information is added. |
+
+==== Syntax ====
+Following the notation in [ [[#References|NPV02]] ], processes in CCP are built from constraints in the underlying constraint system  by the following syntax: {{ :grupos:avispa:syntax.png |}}
+
+
+   * The process **tell**( c ) adds the constraint //c// to the store.
+   * 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 waits until the store contains at least as much information as //c//.
+   * The parallel composition of //P// and //Q// is represented as //P// || //Q//.
+   * The process (**local** x;c) P behaves like //P//, except that all the information on //x// produced by //P// can only be seen by //P//. Additionally, the information on a global variable //x// produced by other  processes cannot be seen by //P//.  The local information on x produced by P corresponds to the constraint c representing a //local store//. If c=**true** one writes (**local** x)P instead of (**local** x;**true**)P.
+   * The process q(**y**) is an identifier with arity |**y**| and it is assumed a unique (recursive) definition of the form "q(**x**) = Q". The process q(**y**) behaves then as Q [**y**/ **x**].
+
+==== A Simple Example: Concatenating two Lists  ====
+
+In this example we shall use the Herbrand constraint system  [ [[#References|SRP91]] ] where  a first-order language  with equality is assumed. The entailment relation  is that one expects from equality, e.g., [x | y] = [a | z] must entail x=a and y=z.
+
+The program concatenating two list can be written in CCP as follows: {{ :grupos:avispa:concat.png |}}
+
+Intuitively, if //X// is the empty list, the constraint //Y=Z// is added to the store. In other case, if //X// takes the form X=[H|T] for some //H// and //T//,  //Z// is constrained to be the list [H | Z'] where //Z'// is the concatenation of  //T// and //Y//.
+====== CCP Calculi and Extensions ======
+Several extensions of CCP have been studied in order to provide settings for the programming and specification of  systems with the [[#Declarative View of CCP Processes|declarative flavor]]  of concurrent constraint programming. For example, **temporal extensions** to deal with reactive systems have been introduced in [ [[#References|SJG94]],[[#References|dBGM00]],[[#References|NPV02]] ], **non-deterministic** behavior and asynchrony [ [[#References|NPV02]],[[#References|dBGM00]] ], **probabilistic** and **stochastic** behavior [ [[#References|GJS97]],[[#References|BP08]] ], **mobility** [ [[#References|OV08]] ], **default** behavior [ [[#References|SJG96]] ], etc.
+
+We refer the reader to [ [[#References|GJS96]] ] that presents  a survey of the development of some of the previous extensions and the relationships between their semantic models.
+Calculi, Languages and Emerging Applications]] ([[http://www.cs.kuleuven.ac.be/~dtai/projects/ALP//newsletter|ALP Newsletter]] Vol. 21 n. 2-3, August 2008) presents a survey of CCP-based calculi, implementation and languages based on this paradigm as well as their applications.
+===== Timed Concurrent Constraint Programming =====
+
+
+Timed CCP (tcc)  was introduced in [ [[#References|SJG94]] ] as an extension of CCP aimed at programming and modeling timed reactive systems. This  model elegantly combines CCP with ideas from the paradigms of  [[http://en.wikipedia.org/wiki/Synchronous_programming_language|Synchronous Languages]].
+
+
+^     The TCC Model  ^^
+| {{:grupos:avispa:tcc-anim.gif|}} | In tcc,  time is conceptually divided into **discrete intervals**. In each time interval, a deterministic CCP processes receives a stimulus (i.e. a constraint) from the environment (**Step 1**), it executes with this stimulus as the  initial store and when it reaches its resting point (**Step 2**), it responds to the environment with the final store (**Step 3**). Furthermore, the resting point determines a residual process, which is then executed in the next time interval (**Step 4**). |
+
+
+
+The tcc calculus introduces constructs to
+  - //delay// the execution of a process and
+  -  //time-out//  (or weak pre-emption) operations that wait during the current time interval for a given piece of information to be present. If it is not, they trigger a process in the next time interval.
+
+In spite of its simplicity, many interesting temporal constructs can be expressed in tcc. As an example, tcc allows processes to be clocked by other processes. This provides meaningful pre-emption constructs and the ability of defining multiple forms of time instead of only having a unique global clock.
+=== Syntax of TCC ===
+
+Processes  P,Q,... in tcc are built from constraints  in the underlying constraint system by the following syntax:
+
+
+{{ :grupos:avispa:tcc.png |}}
+
+The processes **tell** ( c ), **when**  c **do** P, P ||  Q and  (**local** x;c) P  are similar to the corresponding processes in CCP.
+  * The process **skip** represents inaction.
+  * The process **next** P delays the execution of P to the next time interval.
+  * The //time-out//  **unless**  c  **next** P is also a unit-delay, but   P  is executed in the next time unit if and only if c is not entailed by the final store at the current time interval.
+  * The //replication// !P   executes unboundly many copies of  P  but one at a time-unit.
+
+** Applications: ** tcc is particularly appropriate for programming reactive systems such as robotic devices, micro-controllers, databases and reservation systems. These systems typically operate in a cyclic fashion, i.e.,  in each cycle they receive an input from the environment, compute on this input, and then return the corresponding output to the environment.
+
+===== Linear Concurrent Constraint Programming =====
+
+Linear CCP [ [[#References|SL92]],[[#References|FRS01]] ] is a variant of CCP where the constraints are built from a //linear constraint system// (based on [[http://en.wikipedia.org/wiki/Jean-Yves_Girard|Girard]]'s intuitionistic [[http://en.wikipedia.org/wiki/Linear_logic|linear logic]]) instead of a classic constraint system  based on first-order logic.
+
+Constraints in LCC are then linear formulae obtained from a [[http://en.wikipedia.org/wiki/Signature_(logic)|given signature]] and  the [[http://en.wikipedia.org/wiki/Linear_logic|multiplicative conjunction]] , existential quantification and  the [[http://en.wikipedia.org/wiki/Linear_logic|exponential connective]].
+
+ In LCC, the linear tell operator **tell** ( c ) increments the current store d to d ⊗ c instead of d ∧ c. Furthermore, the linear ask **when** c ** do ** P evolves to P iff there exists e s.t. the  current store d entails c ⊗ e. When this evolution occurs, the resulting store is e, i.e., the constraint c is removed. Due to the removal of information, this calculus is  intrinsically non-deterministic unlike tcc.
+
+**Applications: ** LCC being **non-monotonic** (in the sense that the information in the store can be dropped), this model introduces some forms of imperative programming particularly useful for reactive systems. For instance, imperative data structures are encoded directly with linear constraints instead of streams.
+====== Declarative View of CCP Processes ======
+
+CCP calculi enjoy a strong connection with logic that distinguishes this model from other formalisms for [[http://en.wikipedia.org/wiki/Concurrency_(computer_science)|concurrency]].
+This is, in addition to the usual behavioral techniques from process calculi, CCP-based calculi  enjoy a declarative view of processes based upon logic. This makes CCP  a language suitable for both the specification and the implementation of programs.  This correspondence allows also for rechability analysis by using deduction in logic.
+
+   * In [ [[#References|MPS95]] ] the correspondence of CCP and logic is deeply studied  by showing that CCP processes can be viewed as logic formulae, constructs in the language as logical connectives and simulations (runs) as proofs.
+   * In [ [[#References|SJG94]] ] a proof system for tcc based on an [[http://en.wikipedia.org/wiki/Intuitionistic_logic|intuitionistic logic]] enriched with a next operator is proposed. Judgements in the proof system have the form {{ :grupos:avispa:proof-sys.png |}} where  A<sub>1</sub>,...,A<sub>n</sub> and  A are agents (processes).  Such  judgements are valid if and only if any  observation that can be made from the parallel system of agents A<sub>1</sub>,...,A<sub>n</sub> can also be  made from A.
+   *  A calculus for proving correctness of CCP programs is developed in [ [[#References|dBGMP97]] ]. In this framework, the specification of the program is given in terms of a first-order formula. A program property, represented by a constraint, is interpreted as the set of constraints that entails it. A program P is then  said to satisfy a given property A if the  set of all its outputs is a subset of the constraints defining A. This proof system was  extended and strengthened in [ [[#References|NPV02]] ]  with  a proof system for the [[#Non-determinism and Asynchrony|ntcc]] calculus (a non-deterministic extension of tcc)  where  computation along time units are considered.
+====== Other Extensions and Dialects ======
+
+===== Eventual vs Atomic Tell =====
+In Atomic CCP, the process **tell** ( c ) adds the constraint c only if c in consistent with the current store.
+The process tell  can be then written in the  prefix form **P = tell** ( c ).Q where P adds c to the current store d if d∧c is consistent and then P behaves as Q.
+
+In Eventual CCP (or simply CCP), the consistency of c and the current store is not performed. Hence,  c is eventually added to the current store d even if d∧c=**false**.
+
+Notice that unlike CCP, Atomic CCP is non-deterministic. Take for example, **tell** ( x=1 ).Q || **tell** ( x=2 ). The execution of Q depends on whether **tell** ( x=2 ) is scheduled for execution first or not.
+===== Non-determinism and Asynchrony =====
+
+The tcc calculus has been extended to deal with non-deterministic behavior and asynchrony in the ntcc calculus [ [[#References|NPV02]] ]:
+The ntcc processes result from adding to the syntax of tcc the following constructs:
+{{ :grupos:avispa:ntcc.png |}}
+
+The //guarded-choice// Σ<sub>I</sub> **when** c **do** P<sub>i</sub> where I is a finite set of indices, represents a process that, in the current time interval, must non-deterministically  choose one of the P<sub>j</sub>  whose corresponding guard (constraint) c<sub>j</sub> is entailed by the store. The chosen alternative, if any, precludes the others. If no choice is possible then the summation remains blocked until more information is added to the store.
+
+The operator ★P allows  to express asynchronous behavior through the time intervals. Intuitively, ★P represents  an arbitrary long but finite delay for the activation of P.
+
+
+The tccp  calculus [ [[#References|dBGM00]] ] is another timed extension of the CCP model. This calculus introduces a discrete global clock and assumes that the ask
+and tell actions take one time-unit. Computation evolves in steps of one time-unit, so called clock-cycles, which are syntactically separated by action prefixing.
+Moreover maximal parallelism is assumed, that is, at each moment every enabled
+agent of the system is activated.
+
+Processes in tccp are generated from the following syntax:
+{{ :grupos:avispa:tccp.png |}}
+
+The process **stop** represents successful termination. The non-deterministic choice Σ<sub>i=1</sub> **ask** (c<sub>i</sub>) → A<sub>i</sub> is similar to that of ntcc. The process **now** c **then** A **else** B behaves as A or B depending on whether the constraint c is or is not entailed. The process ∃x A is similar to (**local** x)A.
+
+Unlike ntcc and tcc where the final store is not automatically transfered to the next time interval, in tccp the information in the store is carried through the time units.
+
+
+** Applications: ** The ntcc and tccp calculus has been used for programming of reactive systems such as micro-controllers such as RCX’s and PLC’s as well as musical applications.
+
+===== Strong Pre-Emption in tcc =====
+
+In ** Default tcc**  [ [[#References|SJG96]] ] the notion of strong pre-emption is introduced, i.e. the time-out operations can trigger activity in the current time interval. The strong pre-emption operator **if** c **else** P is useful when the process P must be triggered  immediately on the absence of c rather than delayed to the next interaction with the environment as in **unless** c **next** P. In this case, it is assumed that  c has not been produced in the store, and will not be produced throughout system execution at the present time instant.
+===== Continuous Time in tcc =====
+
+The Hybrid concurrent constraint  programming model, **Hybrid cc**  (hcc) [ [[#References|GJS98]] ], is a calculus  where it is possible to express discrete and continuous evolution of time. More precisely, there are points at which discontinuous change may occur (i.e. the execution proceeds as burst of activity) and open intervals in which the state of the system changes continuously (i.e. the system evolves continuously  and autonomously). The syntax of Default tcc is extended with the construct **hence** P, asserting that P holds continuously beyond the current instant. In combination with the other constructs in Default tcc, various patterns of temporal activity can be generated.
+
+** Applications: ** The hcc calculus has been used in the modeling of physical systems (see e.g., a model of a photocopier paper path [[http://www-cs-students.stanford.edu/~vgupta/publications/paperpath-ijcai95-abstract.html|here]]) and [[http://www.saraswat.org/njpls-02-27-2004.html|biological systems]].
+===== CCP and the Pi-Calculus =====
+In [ [[#References |BM07]] ], the cc-pi calculus is proposed as a language for the specification of Service Level Agreements contracts. This language results from the combination of the CCP model with a name-passing calculi. More precisely, cc-pi extends CCP  by adding synchronous communication and by providing a treatment of names in terms of  restriction and structural axioms closer to nominal calculi than to variables with existential quantiﬁcation.  The cc-pi name passing discipline is reminiscent to that in the pi-F calculus [ [[#References |WF05]] ]  whose synchronization mechanism is global and, instead of binding formal names to actual  names, it yields explicit fusions, i.e., simple constraints expressing name equalities. For
+example, the process x⟨y⟩.P (sending y on x) synchronizes with x⟨z⟩.Q and evolves into P ∥ Q ∥ y = z.
+
+The π<sup>+</sup>-calculus [ [[#References |DRV98]] ] is an extension of the [[http://en.wikipedia.org/wiki/Pi-calculus|π-calculus]] with constraint agents that
+can perform tell and ask actions. This provides a language where π processes can be synchronized via blocking asks.
+
+
+===== Universal Timed CCP =====
+
+Universal timed CCP  (utcc) [ [[#References|OV08]] ]  extends  tcc for **mobile** reactive systems.
+utcc replaces the ask operation **when** c  **do** P  with a  //parametric ask// constructor
+of the form  (**abs** **x** c) P.  This process can be viewed as an //lambda-abstraction// of the process P on the variables **x** under the constraint (or with the //guard//) c.
+Operationally, (**abs** **x** c) P  executes P[**t**/**x**]  in the current time interval for //all the terms// **t** in the underlying constraint system  such that  c[**t**/**x**] is entailed by the current store.
+
+** Applications: ** utcc has been used for the analysis of security protocols, to give declarative interpretation of languages for sessions, and for modeling of Dynamic Multimedia-Interaction systems. Further details [[http://www.lix.polytechnique.fr/~colarte/thesis-page/|here]].
+===== Probabilistic and Stochastic Behavior =====
+
+
+When modeling a physical system, it may be the case that some of its components are only partially known. Then, the model of the system must deal with an approximate or incomplete description of these components.  A natural way to model  this situation is to give a probability distribution to the set of  outputs the partially known  components may perform. For example,
+often information is available about failure models and their
+associated probabilities of a component in a mechanical device.
+In [ [[#References|GJS97]] ],  a probabilistic model for CCP and tcc is studied where random variables with a given probability  distribution are introduced.
+
+The works in [ [[#References|APRV08]], [[#References|BP08]] ] study stochastic extensions for CCP. In these calculi, a real number represents the frequency (rate) of occurrence of a certain action and then, processes are scheduled for execution according to this rate.
+
+** Applications: ** Stochastic and probabilistic extensions are used mainly in the modeling of physical and biological systems.
+
+====== Semantics of CCP languages ======
+The operational semantics of CCP calculi is defined by a transition relation "→" over configurations. A configuration is a pair <P,c> where P is a process and c is a constraint representing the global store. Then, a transition of the form <P,c> → <Q,d> means that P with current store c evolves into Q and the new store is d. For instance, a process of the form **tell**(d) evolves into **skip** and adds d to the current store, i.e., <**tell**(d),c> → <**skip**,c∧d>. In CCP, it is always the case that the constraint d entails c, i.e., the store is augmented monotonically. Notice that in Linear CCP this may not be the case since agents may delete information (constraints) when evolving.
+
+ Usually, for the case of  the parallel composition operator,  an interleaving semantics is considered. This is, if <P,c> can evolve to a configuration <P',d> then, <P||Q,c> → <P'||Q,c'>.
+Nevertheless, true concurrency semantics have been also considered for CCP, i.e., semantics where concurrency is explicitly represented. For example, in [ [[#References|BHMR98]] ] two semantics are proposed for [[#Eventual vs Atomic Tell|atomic CCP]]: One is based on partial orders of computation steps and another one based on contextual nets. These semantics allow for deriving concurrency, dependency and non-determinism information more precisely than when considering interleaving semantics.  The [[#The tccp Calculus|tccp]] calculus is also endowed with a //maximal parallelism// semantics rather than a interleaving semantics. In this case, if  <P,c> → <P',c'> and <Q,d> → <Q',d'> then <P||Q,c> → <P'||Q',c'∧ d'>. This is, the process P||Q executes in one time-unit all the initial enabled actions of P and Q.
+
+
+Different notions of **observables** (what the CCP agent compute) can be giving depending on what we observe from the process. For instance, we can observe among others,
+  * Finite computations.
+  * The limit of  infinite computations (when considering recursion).
+  * The set of constraints produced from the empty store (**default output behavior**).
+  * The output of a process given an initial store (**input-output behavior**).
+  * The set of constraints such that the process on input cannot add any information whatsoever or quiescent inputs (**strongest postcondition**).
+
+===== Operational Semantics of Timed CCP languages =====
+
+In temporal extensions of CCP, two transition relations are considered:
+  *  An //Internal transition//  "→" representing the evolution of processes during a time-unit. This transition is similar to that of untimed CCP.
+  * An //Observable transition//  P ⇒(c,d) Q that means "P on input c reduces in one time unit to Q and outputs d". The observable transitions are obtained from a finite sequences of internal transitions.
+
+===== Denotational Semantics for CCP =====
+
+CCP based languages have been endowed with denotational semantics based on  [[http://en.wikipedia.org/wiki/Closure_operator|Closure Operators]]. This is, functions satisfying:
+
+   * **Extensiveness**:  x≤f(x)
+   * **Idempotence**: f(f(x))=f(x)
+   * **Monotonicity**: x≤y implies f(x)≤f(y)
+
+The //strongest postcondition// of a process P is the set of constraints such that P under input cannot add any information whatsoever. For example, a process **tell** ( c ) cannot add any information to a constraint d if d entails c.
+
+A pleasant property of closure operators is that they are uniquely determined by their set of [[http://en.wikipedia.org/wiki/Fixed_point_(mathematics)|fixed points]].  Then, the strongest postcondition of P is determined by the set of fixed points of the closure operator associated to P.
+
+
+The reader can find [[Denotational Semantics of CCP|Here]] the semantics <html>[[P]]</html>  for the tcc calculus. We refer to [ [[#References|SRP91]],[[#References|dBGMP97]],[[#References|NPV02]],[[#References|SJG94]],[[#References|FGMP97]] [[#References|dBdPP95]] ] for more information on semantics of CCP calculi.
+ ====== References ======
+|    [APRV08]|J. Aranda, J. Pérez, C. Rueda, F. Valencia: Stochastic Behavior and Explicit Discrete Time in Concurrent Constraint Programming. In proc. of ICLP'08, 2008|
+|    [BM07]|M. Buscemi and U. Montanari. CC-Pi: A Constraint-Based  Language for Specifying Service Level Agreements. In Proc. of ESOP'07, 2007.|
+|    [BP08]|L. Bortolussi, A. Policriti. Modeling Biological Systems in Stochastic Concurrent Constraint Programming. Constraints 13(1-2): 66-90. 2008.|
+|  [dBCM00]|F. de Boer, M. Gabbrielli, M. C. Meo. A Timed Concurrent Constraint Language. Inf. Comput. 161(1): 45-83. 2000.|
+|  [dBGMP97]|F. de Boer, M. Gabbrielli, E. Marchiori, C. Palamidessi. Proving Concurrent Constraint Programs Correct. ACM Trans. Program. Lang. Syst. 19(5): 685-725. 1997.|
+|  [dBdPP95]|Frank S. de Boer, Alessandra Di Pierro, Catuscia Palamidessi: Nondeterminism and Infinite Computations in Constraint Programming. Theor. Comput. Sci. 151(1): 37-78 ,1995.|
+|    [FGMP97]|Moreno Falaschi, Maurizio Gabbrielli, Kim Marriott, Catuscia Palamidessi: Confluence in Concurrent Constraint Programming. Theor. Comput. Sci. 183(2): 281-315 ,1997.|
+|    [DRV98]|J. Díaz, C. Rueda and F. Valencia. Pi+-Calculus:  A Calculus for Concurrent Processes with Constraints. CLEI Electron. J., vol. 1, no. 2, 1998.|
+|    [FRS01]|F. Fages, P. Ruet, S. Soliman. Linear Concurrent Constraint Programming. Operational and Phase Semantics. Inf. Comput. 165(1): 14-41. 2001.|
+|    [GJS96]|V. Gupta, R. Jagadeesan, V. A. Saraswat. Models for Concurrent Constraint Programming. In Proc. of CONCUR'96. LNCS 1996.|
+|    [GJS97]|V. Gupta, R. Jagadeesan, V. A. Saraswat. Probabilistic Concurrent Constraint Programming. In Proc. of CONCUR'97, 1997.|
+|    [GJS98]|V. Gupta, R. Jagadeesan, V. A. Saraswat. Computing with Continuous Change. Sci. Comput. Program. 30(1-2): 3-49. 1998.|
+|    [MPS95]|N. P. Mendler, Prakash Panangaden, Philip J. Scott, R. A. G. Seely. A Logical View of Concurrent Constraint Programming. Nord. J. Comput. 2(2): 181-220. 1995.|
+|    [NPV02]|M. Nielsen, C. Palamidessi and  F. Valencia. Temporal Concurrent Constraint Programming: Denotation, Logic and Applications.  Nord. J. Comput. 9(1): 145-188, 2002.|
+|    [OV08]|C. Olarte and F. Valencia. The expressivity of universal timed CCP: Undecidability of monadic FLTL and closure operators for security. In PPDP. ACM, 2008.|
+|   [Sar93]|V. A. Saraswat. Concurrent Constraint Programming. MIT Press, 1993.|
+|   [SJG94]|V. A. Saraswat, R. Jagadeesan, V. Gupta. Foundations of Timed Concurrent Constraint Programming. In proc. of  LICS'94. IEEE 1994.|
+|   [SJG96]|V. A. Saraswat, R. Jagadeesan, V. Gupta. Timed Default Concurrent Constraint Programming. J. Symb. Comput. 22(5/6): 475-520. 1996.|
+|    [SL92]|V. Saraswat and Patrick Lincoln.  Higher-order Linear Concurrent Constraint Programming. Tech Report. 1992.|
+|   [Smo94]|G. Smolka. A foundation for higher-order concurrent constraint programming. In Proc. of CCL 94, 1994.|
+|   [SRP91]|V. A. Saraswat, M. Rinard, and P. Panangaden. The semantic foundations of concurrent constraint programming. In POPL ’91. ACM Press, 1991.|
+|   [WF05]|L. Wischik and P. Gardner. Explicit fusions. Theor. Comput. Sci., vol. 340, no. 3, 2005.|