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

grupos:avispa:ccp-wikipedia-new [2011/03/16 13:40] mauriciotoro [Constraint Systems] |
grupos:avispa:ccp-wikipedia-new [2011/03/16 13:43] (actual) mauriciotoro [Basic Constructs] |
||
---|---|---|---|

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]] 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 [[http://en.wikipedia.org/wiki/Vijay_A._Saraswat|Vijay A. Saraswat]]. CCP extends and includes 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]]. | ||

+ | Several flavors of CCP have been studied such as [[http://en.wikipedia.org/wiki/Timed_concurrent_constraint_programming|temporal extensions]] to deal with reactive systems [ [[#References|SJG94]],[[#References|dBGM00]],[[#References|NPV02]] ], **non-deterministic** behavior and asynchrony [ [[#References|NPV02]],[[#References|dBGM00]] ], **probabilistic** and **stochastic** behavior [ [[#References|APRV08]], [[#References|GJS97]],[[#References|BP08]] ], **mobility** [ [[#References|OV08]] ] and **default** behavior [ [[#References|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 [[http://en.wikipedia.org/wiki/Entailment|entailment relation]] that specifies which constraints can be deduced from others. | ||

+ | |||

+ | A commonly used constraint system is [[http://en.wikipedia.org/wiki/Finite_domain_constraint#|Finite Domain]]. Finite domain provides arithmetic relations over [[http://en.wikipedia.org/wiki/Natural_numbers|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//. | ||

+ | {{ :grupos:avispa:ent-example.png |}} | ||

+ | |||

+ | The notion of constraint system can be formalized by using [[http://en.wikipedia.org/wiki/First-order_logic|First-Order Logic]] as in [ [[#References|Smo94]] ]. A constraint system can also be defined 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 ===== | ||

+ | |||

+ | 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 ^ | | ||

+ | |{{ :grupos:avispa:ccp-anim.gif |}}|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. | | ||

+ | |||

+ | ==== Syntax ==== | ||

+ | Following the notation in [ [[#References|NPV02]] ], processes in CCP are built from 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//. 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 [[http://en.wikipedia.org/wiki/Recursion_(computer_science)|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 | ||

+ | |||

+ | {{:grupos:avispa:temperaturecontrol.png}} | ||

+ | |||

+ | ====== 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 [[http://en.wikipedia.org/wiki/Monotonic_function|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 ([[http://en.wikipedia.org/wiki/Predicate_transformer_semantics#Strongest_postcondition|strongest postcondition]]). | ||

+ | |||

+ | The [[http://en.wikipedia.org/wiki/Denotational_semantics|denotational semantics]] of CCP [ [[#References|Sar93]] ] are based on [[http://en.wikipedia.org/wiki/Closure_operator|closure Operators]]. | ||

+ | A very good 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. | ||

+ | |||

+ | |||

+ | ====== Declarative View of CCP Processes ====== | ||

+ | |||

+ | CCP has a strong connection with logic that distinguishes this model from other formalisms for [[http://en.wikipedia.org/wiki/Concurrency_(computer_science)|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 [[http://en.wikipedia.org/wiki/Deductive_reasoning|deduction in logic]]. | ||

+ | |||

+ | ===== Verification of CCP ===== | ||

+ | |||

+ | A calculus for proving correctness of CCP programs is developed in [ [[#References|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.| | ||