Current Structure of FORCES.

 This research collaboration involves members of the INRIA team COMETE, the Music Representation Research Group (IRCAM) and the  AVISPA team (Colciencias).

The Colombian team at present is composed by the following members: 

Rapport scientifique de l'année 2009

Publications and Technical Reports.

• Project Overview

• Biological Systems

In [VAD09] we studied the expresiveness of the ntcc calculus for modeling, simulating and analyzing biological systems. In particular, we explored if it is possible to model membrane systems in ntcc. As the main contribution of this paper, we proposed a general mechanism for modeling membrane systems in ntcc. The application of this mechanism was illustrated with a model for the LDL cholesterol degradation pathway using membrane systems defined in ntcc. Simulations of the model of the LDL cholesterol degradation pathway were done by using ntccSim, a tool to run program specifications in ntcc. 

• Modeling and Verification of Security Protocols

In [FOP09], we extended the semantics of tcc to a "collecting" semantics for the utcc calculus [OV08a,OV08b] based on closure operators over sequences of constraints. Relying on this semantics, we formalized the first general framework for data flow analyses of tcc and utcc programs by abstract interpretation techniques [CC92]. The concrete and abstract semantics we proposed are compositional, thus allowing us to reduce the complexity of data flow analyses. We showed that our method is sound and parametric w.r.t. the abstract domain. Thus, different analyses can be performed by instantiating the framework. We illustrated how it is possible to reuse abstract domains previously defined for logic programming, e.g., to perform a groundness analysis for tcc programs. We showed the applicability of this analysis in the context of reactive systems. Furthermore, we made also use of the abstract semantics to exhibit a secrecy flaw in a security protocol.

We developed a prototype of our methodology and  implemented the abstract domain for security to perform automatically the secrecy analysis. The prototype is available here.

• Multimedia Interaction

• Dissonances in music have had a long evolution history dating back to days of strictly prohibition to times of enricheness of musical motives and forms. Nowadays, dissonances account for most of the musical expressiveness and contain a full application theory supporting their use making them a frequently adopted resource of composition. In [PS09] we partially described their theoretical background as well as their evolution in music. We also proposed a new NTCC-based model for their computational use.
• Writing multimedia interaction systems is not easy. Their concurrent processes usually access shared resources in a non-deterministic order, often leading to unpredictable behavior. Using Pure Data (Pd) and Max/MSP is possible to program concurrency, however, it is difficult to synchronize processes based on multiple criteria. Process calculi such as ntcc overcome that problem by representing multiple criteria as constraints. In [TRA09a] we used our framework Ntccrt (see M. Toro's Bs.C thesis) to manage concurrency in Pd and Max. Ntccrt is a real-time capable interpreter for ntcc. Using Ntccrt externals (binary plugins) in Pd we ran models for machine improvisation and signal processing.
• In [TRA09b] we present Gelisp, a new library to represent musical Constraint Satisfaction Problems and search strategies intuitively. Gelisp has two interfaces, a command-line one for Common Lisp and a graphical one for OpenMusic. Using Gelisp, we solved a problem of automatic music generation proposed by composer Michael Jarrell and we found solutions for the All-interval series.
• In [OR09] we argued for the utcc calculus as a declarative model for dynamic multimedia interaction systems. Firstly, we showed that the notion of constraints as partial information allowed us to neatly define temporal relations between interactive agents or events. Secondly, we showed that mobility in utcc allowed for the specification of more flexible and expressive systems. Thirdly, by relying on the underlying temporal logic in utcc, we showed how non-trivial temporal properties of the model can be verified. As compelling application we proposed a model for dynamic interactive scores where interactive points can be defined to adapt the hierarchical structure of the score depending on the information inferred from the environment. We then broaden the interaction mechanisms available for the composer in previous (more static) models

• In [AVV09] we studied the expressive power of restriction and its interplay with replication. We did this by considering several syntactic variants of CCS! (CCS with replication instead of recursion) which differ from each other in the use of restriction with respect to replication. We considered three syntactic variations of CCS! which do not allow the use of an unbounded number of restrictions: CCS-!v is the fragment of CCS! not allowing restrictions under the scope of a replication. CCS-v is the restriction-free fragment of CCS!. The third variant is CCS-!v!+pr which extends CCS-!v with Phillips' priority guards. We showed that the use of unboundedly many restrictions in CCS! is necessary for obtaining Turing expressiveness in the sense of Busi et al [BGZ04]. We did this by showing that there is no encoding of RAMs into CCS-!v which preserves and reflects convergence. We also proved that up to failures equivalence, there is no encoding from CCS! into CCS-!v nor from CCS-!v into CCS-!v. As lemmata for the above results we prove that convergence is decidable for CCS-!v and that language equivalence is decidable for CCS-v!. As corollary it follows that convergence is decidable for restriction-free CCS. Finally, we show the expressive power of priorities by providing an encoding of RAMs in CCS-!v!+pr.
• In [LOP09] we described a unified framework for the declarative analysis of structured communications. By relying on the utcc calculus, we showed that in addition to the usual operational techniques from process calculi, the analysis of structured communications can elegantly exploit logic-based reasoning techniques. We presented a concurrent constraint interpretation of the language for structured communications proposed by Honda, Vasconcelos, and Kubo. Distinguishing features of our approach are: the possibility of including partial information (constraints) in the session model; the use of explicit time for reasoning about session duration and expiration; a tight correspondence with logic, which formally relates session execution and linear-time temporal logic formulas.
• In [ARV09] we explored the possibility of using Event Structures [WIN07], a popular model for representing concurrency, to give an adequate semantics for each NTCC construct in a straightforward and understandable way. To give a precise representation by means of event structures we had to take into account several conditions such as guaranteeing true concurrency and establishing adequate representations for specific constructs. Finally, borrowing some concepts from Pratt, we constructed a triadic event structure which could fulfill our requirements.
• In [VDV09] we studied a constraint system based on Spatial logics. We showed that a fragment of the Ambients Calculus can be encoded into utcc using such a constraint system. This work was developed as part of the Master thesis of John Vargas from Universidad del Valle in collaboration with the french partners. Here the thesis proposal of John's thesis.
• In [TPR09] we presented a new simulation tool for Probabilistic ntcc (pntcc) and a prototype for verification of pntcc models. We included these tools in the Ntccrt framework. We also showed the formal basis for correctness of the ntcc simulation tool and we showed that the execution times of the simulation are still acceptable for real-time interaction using pntcc.