Direction des Relations et Internationales (DRI)

Programme INRIA "Equipes Associées"




Equipe-Projet INRIA : COMETE
Organisme étranger partenaire : Pontificia Universidad Javeriana Cali
Centre de recherche INRIA : Futurs
Thème INRIA :  Systèmes Communicants
Pays : Colombia
Coordinateur français
Coordinateur étranger
Nom, prénom Valencia, Frank D.
Rueda, Camilo
Grade/statut CR2 (Permanent Researcher) Full Professor
Organisme d'appartenance
CNRS Pontificia Universidad Javeriana
Adresse postale LIX, École Polytechnique
Rue de Saclay, 91128 Palaiseau FRANCE
Dept. Ciencias e Ingeniería de la Computación.
Calle 18 No. 118-250 Cali, Colombia; A.A. No. 26239
Téléphone +33 1 6933 4144 +57 2 321 8397
Télécopie +33 1 6933 3014 +57 2 555 2823

La proposition en bref

Titre de la thématique de collaboration : FORCES (FORmalisms from Concurrency for Emergent Systems): Formalismes de la théorie des processus concurrents pour les systèmes émergents.

Concurrent Constraint Programming (CCP) is a mature formalism from Concurrency Theory which combines the traditional operational view of process calculi with a declarative one of processes based upon logic. Some of the members of the teams in this proposal developed and have been using NTCC [NPV02], a timed CCP calculus, to predict the behavior of several systems from emergent areas in computer science such as Security Protocols [LPP+06], Systems Biology [GPRV07] and Multimedia Semantic Interaction [RV05]. Although these areas differ significantly from one another, there is a fundamental commonality in the nature of the analysis one wants to achieve in them: Reachability, i.e., whether a system reaches a state satisfying a particular property. We chose NTCC for these systems because it provides several reasoning tools such as a temporal linear-time logic, a proof system, verification techniques and a denotational semantics which are particularly useful for reachability analysis.

Despite the success of our applications of NTCC to the above-mentioned areas, we have learned from our modeling experience and theoretical studies that NTCC is not sufficiently robust for them. For example, some security protocols use a mechanism to allow generation and communication of secrets. The NTCC calculus can at best express this mechanism indirectly [Val05]. Also, NTCC lacks probabilistic techniques. The modeling of the biological systems often requires to cope with uncertain and approximate information which can then be naturally represented using a probabilistic formalism. Furthermore, we have identified complex non-regular audio processing temporal behavior which cannot be expressed in NTCC.

In this collaboration we aim at providing more robust formalisms for analyzing the emergent systems our teams have been modeling during recent years: I.e., Security Protocols, Biological Systems and Multimedia Semantic Interaction. Our research strategy is, with the benefit of hindsight, to develop them as suitable extensions or specializations of NTCC. We believe that our expertise in process calculi and CCP as well as our experience in modeling the above-mentioned systems are fundamental for achieving this task.

Présentation de l'Équipe Associée

1. Présentation du coordinateur étranger

After finishing his computer science graduate work at MIT, Professor Rueda joined La Universidad de los Andes in Bogota and later La Pontificia Universidad Javeriana (PUJ) in Cali, Colombia, where he is currently full professor and chair of the department of Science and Engineering of Computing. He also worked as a researcher at the IRCAM-CNRS unit UMR9912 (Institut de Recherche Et Coordination Acoustique Musique). Professor Rueda founded the AVISPA research team in 1995 and has lead it since. He belonged to the directing board of the Latin American Informatics association (CLEI) until 2006 and was organizer of the annual conference of that association in 2005. He has been guest editor of the CLEI electronic journal, and member of the program committee of conferences in Latin America and Europe, in the domains of constraint programming and computer music. He is the author of 18 journal papers and several international refereed conference papers. His research interests are in using Concurrent Constraints Programming Calculi to model real-world systems, Constraint languages and tools for solving combinatorial problems and Programming languages and tools for music composition.

Présentation de l'équipe française

The French team is composed by the following members:

Présentation de l'équipe étranger

The Colombian team is composed by the following members:
2. Historique de la collaboration

3. Impact


Programme de travail

Before describing our work plan, let us give a brief description of Concurrent Constraint Programming (CCP).

Background. CCP is a well-established process calculus for concurrency in which processes interact with each other by telling and asking information represented as logic formulae also known as constraints (e.g., x > 42). The NTCC formalism [NPV02] is a particular CCP process calculus for timed-systems. The applicability of the calculus has been illustrated with by modeling robotic devices, multi-agent systems and applications in music and biology. Furthermore, the calculus is provided with a denotational semantics that captures the reactive computations of processes in the presence of arbitrary environments. Also, the calculus is provided with a process logic for expressing temporal specifications of NTCC processes as well as a complete inference system to prove that a given NTCC process satisfies a given formula in this logic.

Research Plan for 2008

The planned research for the year 2008 is articulated along the three topics below.

(1) CCP for Security Protocols.

Due to technological advances such as the Internet and mobile computing, security has become a serious challenge involving several frameworks of Computer Science, in particular Process Calculi.

Remarkably, most process calculi for security protocols have strong similarities with CCP. For instance, SPL [CW01], the Spi calculus variants in [ALV03, FA01], and the calculus in [BB01b] are all operationally defined in terms of configurations containing information which can only increase during evolution. Such a monotonic evolution of information is akin to the notion of monotonic store, which is central to CCP and a source of its simplicity. Also, the calculi in [ALV03,BC02, FA01] are parametric in the underlying logic much like CCP is parametric an underlying constraint system. Also, the assertion of (protocol) properties [ALV03] can be formalized as CCP processes imposing constraints.

We plan to give a CCP account of a representative calculus for security protocols. We will use CCP constraint systems to represent a logic to reason about the information an attacker can deduce from the information accumulated in the monotonic store. The CCP linear-time temporal logic and associated complete inference system in [NPV02] and the verification results in [Val05] can be used to specify and prove safety properties of protocol runs. Since most security protocols use mechanisms to allow generation of nonces (or names), we will provide CCP with such mechanisms.

It must be pointed out that there are several instances of the research in security protocols that have used tools and techniques from areas closely related to CCP. Namely, Constraint Programming (e.g. [BB01a] and [Mil95]) and Logic Programming (e.g. [CD99]) To our best knowledge there is no work on Security Protocols that takes advantage of the reasoning techniques of CCP.

Participants. Carlos Olarte, Catuscia Palamidessi, and Frank D. Valencia from COMETE, and Camilo Rueda and the student Gustavo Gutierrez from AVISPA.

(2) CCP in Systems Biology.

Quantitative information is fundamental for biological systems. E.g., most bio-chemical reactions are highly dependent on the presence of a certain amount of the substances involved. Moreover this information is "partial" as it is difficult to obtain "exact" values for parameterizing models. Unpredictable behavior is an inherent condition of the biologic phenomena. We usually count with "partial behavioral information" for describing interactions in models. This information not only ignores elements on "how" reactions occur, but also "when" such reactions commonly happen.

The above-mentioned "partial-information" notions makes us believe that CCP has much to offer in the biological context. The notion of partial quantitative information is central to CCP via constraints. Partial behavioral information is actually the novelty of NTCC via non-deterministic and asynchronous operators. In fact, our teams have already explored these advantages in a preliminary study by given a model of a mechanism for cellular transport; Sodium-Potassium pump.

Our plan is to exploit the above-mentioned advantages of CCP for expressing partial information in the biological context, representing relevant biological phenomena as NTCC processes and their properties as formulae. We will study whether this partial information will be best represented in terms of spatial logic formulae which can describe structural information about biological elements. This would enable us to both simulate systems and verify their encodings using the NTCC calculus. Furthermore we shall include probabilistic elements in the calculus since uncertain and approximate information is typical in biological systems.

There are other approaches using CCP for Biological systems. In [ERJ+04] the CCP-based calculus hcc was used for the modeling of a regulation processes over genes. Also [BC02] uses hcc to model dynamic biological systems. Nevertheless, since hcc does not include operators for expressing partial behavioral information, a considerable amount of biological phenomena may not be modeled appropriately. In [Sar04] a linear CCP language, is proposed to model protein interaction. Unlike our approach, this works only focus on system simulations. Finally, BIOCHAM [CRFS04] is a programming environment for modeling biochemical systems developed by the INRIA Contraintes group which allows for simulations and querying the model in the temporal logic CTL. Since we are mainly interested in reachability properties of biological systems the underlying temporal logic of our approach is LTL rather than CTL. In fact, NTCC has been specially designed to have a strong connection with LTL to facilitate reachability analysis. Our proposed extension will also follow this design criteria.

Participants. Jesus Aranda, Romain Beauxis, Sylvain Pradalier, and Frank D. Valencia from COMETE, and Camilo Rueda and the student Henry Perez from AVISPA.

(3) CCP for Multimedia Semantic Interaction

Semantic interaction is concerned with systems that interact with users in a creative way by on-line learning and maintaining a model of the user's behavioral style and using that model for updating, in generative way, their narrative/presentation/interaction strategies. While multimedia interaction involves many disciplines in Computer Sciences, such as computer graphics and digital audio rendering, the core of the system is concerned with powerful and consistent concurrent agents architectures. Little is known yet in the formalisms that would make these agents creative in some sense, allowing them to build up credible and surprising narrative forms conditioned by their learned knowledge and the present interaction.

Process calculi model agent interaction in general in such a way that the richness of complex interactions that are usual in multimedia can be understood by building compositionally from the rigorous semantics of a few simple constructs. In order to add learning and narrative action features, concurrent constraints calculi are good candidates because they add the possibility of modeling declaratively through constraints complex restrictions on mutual interactions. NTCC provides a control over time and non-determinism, thus opening the way to the generation of narrative sequences modeling innovative behavior that nevertheless keeps coherence with the past context of interaction as well as the current environment. In fact, preliminary experiments using NTCC on semantic music interaction feature a virtual musical improviser that learns from a human musician, models its style and play innovative improvisations that are stylistically consistent with the model [AS099,AD02, ADLB03, AD04]. However several theoretical and practical issues remain to be solved in order to cope with realistic application in multimedia interaction :

We have constructed a preliminary version of a NTCC simulator in Common Lisp and have used it to implement a Factor Oracle model of music improvisation [ADR06] in which three agents, a learner, a player and an oracle concurrently interact in real time. The oracle maintains the model of the human user's musical style.

Our plan is to begin by pursuing observation of our model behavior in ever more complex interaction settings. E.g., a scenario where independent learners acquire knowledge from particular points of view of the observed behavior of a third agent. We will then find out to what extent constraints on information available in a given time unit can be used for this, or what extensions of NTCC are needed. We expect to advance the temporal CCP theory to deal with richer notions of time, at least for handling real time coupled with default behavior of "late", interruptible processes. A formalism for expressing properties associated with this extension will be defined. We will construct a framework for the above, including an interpreter of the calculus able to run in real time.

To the best of our knowledge, apart from our work mentioned above, no other attempts have been made to use CCP for multimedia semantic interaction.

Participants. Frank D. Valencia from COMETE, Camilo Rueda and the student Mauricio Toro from AVISPA, and Gerard Assayag from IRCAM.

Long-term research plans

We plan to develop robust theories and software tools based on the Concurrent Constraint Programming (CCP) model for dealing with applications in the areas of Security Protocols, Biology and Multimedia Semantic Interaction. In the long term, we expect both theoretical and practical results from our efforts on this proposal. Namely: (i) CCP Process Calculi to model and reason about phenomena in these areas. (ii) Tools to automatically simulate and verify the encoded applications. The plan includes PhD work to be carried by the COMETE students Jesus Aranda, Romain Beauxis and Carlos Olarte.

In the long term, we also plan to have a PhD student in co-supervision with Camilo Rueda to investigate (ii) above for the area of Multimedia Semantic Interaction.


Budget prévisionnel 2008

1. Co-financement

This project proposal is intended to be a PUJ (Pontificia Universidad Javeriana) - INRIA collaborative venture.

AVISPA holds a grant from the Colombian Science and Technology Agency (COLCIENCIAS) via the research project REACT to do research in the above-mentioned areas. These funds will be used for one trip to Colombia for Gerard Assayag, two trips to Paris for Camilo Rueda and a trip to Paris for the AVISPA students: Gustavo Gutierrez, Henry Perez and Mauricio Toro. We assume each trip to Paris costs 2,200€ (1,200€ for the flight + 1000€ for accommodation and meals) and that the trip to Colombia costs 1,500€ (1,200€ for the flight + 300€ for accommodation and meals). This gives us a total estimate of 12,500€

AVISPA existing funds from COLCIENCIAS 12,500€

2. Echanges

Summarizing, the COMETE team plans ten trips to Colombia during 2008: Eight trips for our PhD students and two trips for the co-ordinator of the French team. We assume each trip costs 1,500€ (1,200€ for the flight + 300€ for accomodation and meals). We estimate a total of 20.000€ with 15.000€ for the ten trips to Colombia and the remainder 5000€ for two conferences trips in Europe (estimated cost 1,500€) and one conference trip to USA or Latin America (estimated cost 2,000€).

Chercheurs confirmés  1  2x1,500€ (two trips to Colombia for French Co-ordinator)   3,000€
Doctorants  4  2x4x1,500€ (two trips each to Colombia)  2x1,500€(two European conferences) + 1x2,000€ (one North or Latin American conference) 17,000€


Autre (précisez): Trips funded by the Colombian Team
    5 x 2,200€ (five trips to Paris) + 1x1,500€(one trip to Colombia)    12,500€
- total des co-financements
Financement "Équipe Associée" demandé


[AADR98] C. Agon, G. Assayag, O. Delerue, and C. Rueda. Objects, time, and constraints in openmusic. In ICMC 98, 1998.
[AAFR94] C. Agon, G. Assayag, J. Fineberg, and C. Rueda. Kant: a critique of pure quantification. In ICMC 94, 1994.
[AD02] G. Assayag and S. Dubnov. Universal prediction applied to stylistic music generation. In Mathematic and Music, EMS Diderot Forum, 2002.
[AD04] G. Assayag and S. Dubnov. Using factor oracles for machine improvisation. Soft Comput., 8(9), 2004.
[ADLB03] G. Assayag, S. Dubnov, O. Lartillot, and G. Bejerano. Using machine-learning methods for musical style modeling. IEEE Computers, 36(10), 2003.
[ADR06] G. Assayag, S. Dubnov, and C. Rueda. A concurrent constraints factor oracle model for music improvisation. In CLEI 06, 2008.
[ALV03] R. Amadio, D. Lugiez, and V. Vanackère. On the symbolic reduction of processes with cryptographic functions. Theor. Comput. Sci., 290(1), 2003.
[ARL+99] G. Assayag, C. Rueda, M. Laurson, C. Agon, and O. Delerue. Computer-assisted composition at IRCAM: From Patchwork to OpenMusic. Comput. Music J., 23(3), 1999.
[ASO99] C. Agon, S.Dubnov, and O.Delerue. Guessing the composer's mind : Applying universal prediction to musical style. In ICMC 99, 1999.
[BB01a] G. Bella and S. Bistarelli. Soft constraints for security protocol analysis: Confidentiality. In PADL 01, 2001.
[BB01b] M. Boreale and M. Buscemi. A framework for the analysis ofsecurity protocols. In WSDAAL, 2001.
[BC02] A. Bockmayr and A. Courtois. Using hybrid concurrent constraint programming to model dynamic biological systems. In ICLP 02, 2002.
[BR98] A. Bonnet and C. Rueda. Situation: Un langage visuel basé sur les contraintes pour la composition musical. Recherches et applications en informatique musicale, 1998.
[CD99] K. Compton and S. Dexter. Proof techniques for cryptographic protocols. In ICAL 99, 1999.
[CRFS04] Nathalie Chabrier-Rivier, François Fages, and Sylvain Soliman. The biochemical abstract machine biocham. In CMSB, pages 172-191, 2004.
[CW01] F. Crazzolara and G. Winskel. Events in security protocols. In CCS 01, 2001.
[DL03] V. Danos and C. Laneve. Graphs for core molecular biology. In CMSB 03, 2003.
[dPMH04] María del Pilar Muñoz and Andrés René Hurtado. Programming robotic devices with a timed concurrent constraint language. In CP, page 803, 2004.
[DRV98] J. Diaz, C. Rueda, and F. Valencia. The pi+ calculus: A calculus for concurrent processes with constraints. CLEI Electronic Journal, 1(2), 1998.
[ERJ+04] D. Eveillard, D. Ropers, H. Jong, C. Branlant, and A. Bockmayr. A multi-scale constraint programming model of alternative splicing regulation. Theor. Comput. Sci., 325(1), 2004.
[FA01] M. Fiore and M. Abadi. Computing symbolic models for verifying cryptographic protocols. In CSFW 01, 2001.
[GPRV07] J. Gutiérrez, J. Pérez, C. Rueda, and F. Valencia. Timed concurrent constraint programming for analysing biological systems. Electron. Notes Theor. Comput. Sci., 171(2), 2007.
[LPP+06] H. López, C. Palamidessi, J. Pérez, C. Rueda, and F. Valencia. A declarative framework for security: Secure concurrent constraint programming. In ICLP 2006. 2006.
[Mil95] J. K. Millen. The interrogator model. In SP 95, 1995.
[NPV02] M. Nielsen, C. Palamidessi, and F. Valencia. Temporal concurrent constraint programming: Denotation, logic and applications. Nordic Journal of Computing, 9(1), 2002.
[NV02] Mogens Nielsen and Frank D. Valencia. Temporal concurrent constraint programming: Applications and behavior. In Formal and Natural Computing, pages 298-324, 2002.
[RAQ+01] C. Rueda, G. Alvarez, L. Quesada, G. Tamura, F. Valencia, J. Diaz, and G. Assayag. Integrating constraints and concurrent objects in musical applications: A calculus and its visual language. Constraints, 6(1), 2001.
[RV02] C. Rueda and F. Valencia. Proving musical properties using a temporal concurrent constraint calculus. In ICMC 02, 2002.
[RV04a] C. Rueda and F. Valencia. Non-viability deductions in arc-consistency computation. In ICLP 2004. 2004.
[RV04b] C. Rueda and F. Valencia. On validity in modelization of musical problems by CCP. Soft Comput., 8(9), 2004.
[Sar04] V. Saraswat. Euler: an applied lcc language for graph rewriting. Technical report, Technical report, IBM TJ Watson Research Center, 2004.
[Val05] F. Valencia. Decidability of infinite-state timed CCP process and first-order LTL. Theoretical Computer Science, 330(3), 2005.



© INRIA - mise à jour le 28/08/2007