Robust theories for Emerging Applications in Concurrency Theory
A joint research effort between the AVISPA Research Group (Universidad Javeriana at Cali, Colombia), the Musical Representations Team at IRCAM and the INRIA Team Comète (LIX, École Polytechnique de Paris, France).
REACT is supported by COLCIENCIAS (The Colombian Agency for Science and Technology Development).
Concurrency theory has made progress by extending well established theories to capture new and wider phenomena. In particular, process calculi such as CSP, CCS and the pi-calculus, originally designed to reason about concurrent systems, have been extended or specialized to cope with the advents of new technology. For instance, spi-calculus extends the pi-calculus to reason about security; a phenomenon which now pervades the informational world. More recently, the pi-calculus has been tailored to model phenomena in biology, business process modeling (workflow) and web services.
Process calculi are used for modeling the above-mentioned phenomena for at least two reasons. First, since these calculi have careful, mathematical definitions, they can be used to provide careful and high-level meaning to the applications specified using them. Second, the theoreticians working on these calculi have developed rich reasoning methods to reason about meaning and properties of processes. From the application point-of-view, such reasoning methods can be used to infer important properties about encoded applications.
The above evidence suggests that for developing a theory of some phenomena a research strategy is to see if it can arise as an extension or specialization of an existing mature framework. This strategy, at least with a little hindsight, is what lead us to a research proposal on robust theories for complex emerging applications areas of concurrency theory. Namely,
Although these areas differ significantly from one another, we shall argue that there is a fundamental commonality in the nature of the analysis that one wants to achieve in them.
Concurrent Constraint Programming (CCP) is a mature formalism which combines the traditional operational view of process calculi with a declarative one of processes based upon logic. This combination allows CCP to benefit from the large body of techniques of both process calculi and logic. Our teams have developed and implemented a particular CCP timed process calculus which we called NTCC. The calculus offers reasoning techniques such as a linear-temporal specification logic and its corresponding proof system in which reachability analysis can be elegantly carried out.
Our teams have been using NTCC for analyzing security protocols, biological phenomena and applications from multimedia semantic interaction. Reachability analysis is central to all of them. In security protocols if there is a way to reach a state where some intruder knows your secret, then there is a secrecy breach. In bacterial transcription, one ones to know if there is a gene expression possible in a given gene regulatory network: this is a reachability analysis problem. Multimedia Semantic Interaction involve complex interactions in which we may wish to know that a certain undesirable property will eventually arise; again a reachability question.
Despite the success of our applications of NTCC to the above-mentioned areas, we have learned from our modeling experience and theoretical studies that the NTCC calculus 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. Also, the NTCC calculus also lacks probabilistic techniques. The modeling of the biological systems often requires to cope with uncertain and approximate information, which one can refine by statistical measurements, and which can then be naturally represented using a probabilistic formalism. Furthermore, we have identified complex non-regular audio processing temporal behaviour which cannot be expressed in NTCC.
Therefore, the main objectives of REACT focus on developing more robust CCP theories for dealing with applications in the areas of Security Protocols, Biology and Multimedia Semantic Interaction.
We propose to obtain our objectives by tailoring the CCP process calculus NTCC for each of these areas. We believe that our expertise in process calculi and our experience in modeling these sort of applications are fundamental for achieving this task.
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.