Concurrent Constraint Programming (CCP)

Concurrent Constraint Programming (CCP) is a process calculus originally developed by Vijay A. Saraswat as a powerful paradigm for concurrency tied to logic. CCP extends and subsumes both concurrent logic programming and constraint logic programming. A fundamental issue in CCP is the specification of 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:

1. A signature from which the constraints can be constructed.
2. 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 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 ]. Alternatively, this can be given in terms of Scott's information system without consistency structure as it was done in [ Sar93 ].

Basic Constructs

In the spirit of 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 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.

Following the notation in [ NPV02 ], processes in CCP are built from constraints in the underlying constraint system by 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. 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 [ 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: 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 flavor of concurrent constraint programming. For example, temporal extensions to deal with reactive systems have been introduced in [ SJG94,dBGM00,NPV02 ], non-deterministic behavior and asynchrony [ NPV02,dBGM00 ], probabilistic and stochastic behavior [ GJS97,BP08 ], mobility [ OV08 ], default behavior [ SJG96 ], etc.

We refer the reader to [ GJS96 ] that presents a survey of the development of some of the previous extensions and the relationships between their semantic models. Concurrent Constraint Programming: Calculi, Languages and Emerging Applications (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 [ 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 Synchronous Languages.

The TCC Model 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

1. delay the execution of a process and
2. 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:

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 [ SL92,FRS01 ] is a variant of CCP where the constraints are built from a linear constraint system (based on Girard's intuitionistic linear logic) instead of a classic constraint system based on first-order logic.

Constraints in LCC are then linear formulae obtained from a given signature and the multiplicative conjunction , existential quantification and the 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 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 [ 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 [ SJG94 ] a proof system for tcc based on an intuitionistic logic enriched with a next operator is proposed. Judgements in the proof system have the form where A1,…,An 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 A1,…,An can also be made from A.
• A calculus for proving correctness of CCP programs is developed in [ 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 [ NPV02 ] with a proof system for the 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 [ NPV02 ]: The ntcc processes result from adding to the syntax of tcc the following constructs: The guarded-choice ΣI when c do Pi where I is a finite set of indices, represents a process that, in the current time interval, must non-deterministically choose one of the Pj whose corresponding guard (constraint) cj 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 [ 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: The process stop represents successful termination. The non-deterministic choice Σi=1 ask (ci) → Ai 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 [ 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) [ 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 here) and biological systems.

CCP and the Pi-Calculus

In [ 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 [ 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 π+-calculus [ DRV98 ] is an extension of the π-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) [ 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[tx] in the current time interval for all the terms t in the underlying constraint system such that c[tx] 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 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 [ GJS97 ], a probabilistic model for CCP and tcc is studied where random variables with a given probability distribution are introduced.

The works in [ APRV08, 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 [ BHMR98 ] two semantics are proposed for 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 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 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 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 Here the semantics [[P]] for the tcc calculus. We refer to [ SRP91,dBGMP97,NPV02,SJG94,FGMP97 dBdPP95 ] for more information on semantics of CCP calculi.

grupos/avispa/ccp-wikipedia.txt · Última modificación: 2011/01/24 15:30 (editor externo) 