Concurrent Constraint Programming (CCP) is a process calculus where
concurrent processes interact through a shared **store** of partial information. The store is represented by a set of constraints and it represents the current state of the system.

Processes can change the state of the system by **telling** information to the store (i.e., adding constraints to the store). Processes can also synchronize by **asking** if some information (constraint) can be deduced from the current store. As an example, the constraint x + y ≥ 10 can be deduced from the constraint x + y ≥ 2.

CCP was originally developed by Vijay A. Saraswat. CCP extends and includes both concurrent logic programming and constraint logic programming.
Several flavors of CCP have been studied such as temporal extensions to deal with reactive systems [ SJG94,dBGM00,NPV02 ], **non-deterministic** behavior and asynchrony [ NPV02,dBGM00 ], **probabilistic** and **stochastic** behavior [ APRV08, GJS97,BP08 ], **mobility** [ OV08 ] and **default** behavior [ SJG96 ].

CCP processes are parametric in a *constraint system*. A constraint system is composed by a set of basic constraints, called the **signature**, and an entailment relation that specifies which constraints can be deduced from others.

A commonly used constraint system is Finite Domain. Finite domain provides arithmetic relations over Natural Numbers. As an example, processes modeling an air conditioning temperature controller may have to deal with partial information such as *42 < tsensor < 100*
expressing that the temperature value is between 42 and 100. In this case, the sensor registers an unknown or not precisely determined.
The entailment relation 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 [ Smo94 ]. A constraint system can also be defined in terms of Scott's information system without consistency structure as it was done in [ Sar93 ].

CCP has a small number of primitive operators. A typical CCP process language features the following operators:

- A
**tell**operator, adding a constraint to the store. - An
**ask**operator, launching a process 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 in the sense of local variables in programming languages.

Following the notation in [ NPV02 ], processes in CCP are built from the following syntax:

- 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*. Otherwise, it waits until*c*can be deduced from the store. - 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 process q(
**y**) is an identifier with |**y**| parameters and it can be recursive. The process q(**y**) behaves then as Q [**y**/**x**].

CCP has both operational and denotational semantics.

The operational semantics of CCP are 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. 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. As an example, a process **tell**(d) evolves into **skip** and adds d to the current store, formally <**tell**(d),c> → <**skip**,c∧d>. In CCP, it is always the case that the constraint d entails c because the store is augmented monotonically.
Usually, for the case of the parallel composition operator, interleaving semantics are considered. This is, if <P,c> can evolve to a configuration <P',d> then, <P||Q,c> → <P'||Q,c'>.

Different notions of **observables** (what the CCP agent compute) can be giving depending on what we observe from the process. Examples of observables are

- 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 a process under input cannot add any information (strongest postcondition).

The denotational semantics of CCP [ Sar93 ] are based on closure Operators. A very good property of closure operators is that they are uniquely determined by their set of fixed points. Then, the strongest postcondition of P is determined by the set of fixed points of the closure operator associated to P.

CCP has a strong connection with logic that distinguishes this model from other formalisms for concurrency. It means that CCP has a declarative view of processes based on 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.

A calculus for proving correctness of CCP programs is developed in [ dBGMP97 ]. 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. There are other verification procedures for different flavors or CCP, in particular for timed CCP.

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

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

[GJS96] | V. Gupta, R. Jagadeesan, V. A. Saraswat. Models for Concurrent Constraint Programming. In Proc. of CONCUR'96. LNCS 1996. |

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

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