Concurrent Constraint Programming (CCP)

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

Constraint Systems

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

Basic Constructs

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.
Example: CCP Processes
The processes tell (temperature>42) and tell (temperature <70) add information to 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 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].

A Simple Example: The Air Conditioning Temperature Controller

The example above can be formally written as

Semantics of CCP

CCP has both operational and denotational semantics.

Operational Semantics for CCP

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

Denotational Semantics for CCP

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.

Declarative View of CCP Processes

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.

Verification of CCP

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.

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
[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.
 
grupos/avispa/ccp-wikipedia-new.txt · Última modificación: 2011/03/16 13:43 por mauriciotoro
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki