Direction des Relations et Internationales (DRI)

Programme INRIA "Equipes Associées"

I. DEFINITION

II. PREVISIONS 2008

Programme de travail

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

(1) CCP for Security Protocols.

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.

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

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 :

• real-time NTCC agent synchronization in the case of "polyphony" of virtual characters
• agent synchronization in the case of multiple-point of views modeled by multiple agents accessing past context non-locally
• Allowing interruption of processes and default strategies to "catch up" in time.

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

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

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€

ESTIMATION PROSPECTIVE DES CO-FINANCEMENTS
Organisme	Montant
AVISPA existing funds from COLCIENCIAS	12,500€
Total	12,500€

2. Echanges

• Camilo Rueda has scheduled a visit to Paris at the end February 2008 . This will be an occasion to set up a meeting with the purpose of establishing a detailed action plan.
• Later during spring 2008 we plan to organize a workshop at La Pontificia Universidad Javeriana (PUJ), of a duration of two or three days, in which the members of AVISPA and the members of the French team, except Palamidessi, are expected to participate and present their research interests and achievements related to the project. This will be an occasion for the members of the two teams to get introduced to each other, to identify common interests, and envisage possible collaborations on specific topics among inter-teams subgroups. These topics will include those detailed in the Programme de Travail, but it is possible that the stimulating atmosphere of a physical meeting will induce to discover further issues of interest for the project. The workshop will be followed by a few days visit, to articulate specific collaborations and get started on them. For participating to these events, all the members of the French team plan a trip of about one week to PUJ.
• The AVISPA members plan to visit the French partners for another week in June 2008, to continue the collaborations started with the previous meeting. We will organize a second workshop at École Polytechnique and invite the INRIA Contraintes group and the IRCAM Representations Musicales group.
• The COMETE members of the French team from the first visit to PUJ plan another trip to Colombia of about one week to complete the collaborations with the AVISPA partners. These trips will take place later in 2008, probably during fall.

REFERENCES