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

Enlace a la vista de comparación

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
 +====== 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.|
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