This course is an introduction to process calculi for modeling real-life systems such as for example Security Protocols and Biological Systems.

• Profesor: Frank Darwin Valencia
• Créditos: 3
• Horas de Clase: 3 / semana
• Horas de trabajo independiente: 6 / semana
• Prerequisitos: Conocimiento básico de autómatas, lógica y concurrencia.

Process calculi are formalisms which allows to reason about properties of concurrent systems (i.e. systems of multiple agents, called processes, that interact with one another). A common feature of these calculi is that they treat processes much like the lambda-calculus treats computable functions. For example, a typical process term is the parallel composition P | Q, which is built from the terms P and Q with the constructor | and represents the process that results from the parallel execution of the processes P and Q. An operational semantics may dictate that if P can reduce to (or evolve into) P’, written P → P’, then we can also have the reductions P |Q → P’ | Q.

We shall begin by introducing and motivating the most standard and basic process calculi departing from Automata Theory. Namely CCS and the Pi-Calculus. We shall study in detail the theory underlying these calculi; process equivalences, logic and verification techniques.

We shall then focus on a particular process calculus for modeling timed reactive systems, namely ntcc [NPV02]. The ntcc calculus was developed by researchers from the CNRS Laboratory for Informatics LIX at Ecole Polyechnique de Paris, IRCAM (“Institut de Recherche et Coordination Acoustique/Musique”), La Universidad Javerana Cali and La Universidad del Valle and it was carried under the auspices of COLCIENCIAS, via the project REACT, and the French National Institute for Research in Computer Science and Control (INRIA), via the project FORCES.

The ntcc calculus is founded upon solid mathematical principles and it has attained a wide range of applications in emergent areas such as Security, Biology and Multimedia Semantic Interaction. Indeed, ntcc provides rich verification techniques allowing the inference of important temporal properties satisfied by the encoded applications, e.g., security breaches in cryptographic protocols [OV08a], prediction of organic malfunctions [GPRF07] and rhythmic coherence in music improvisation [RV04].

Finally we shall conclude the course by describing applications of the above-mentioned calculi to real-life systems. The students will present this final part of the course.

• [GPRF07] J. Gutierrez, J. Perez, C. Rueda and F. Valencia. Timed Concurrent Constraint Programming for Analyzing Biological Systems. Electr. Notes Theor. Comput. Sci. 171(2): 117-137.© Elsevier. 2007
• [NPV02] M Nielsen, C. Palamidessi and F. Valencia. Temporal Concurrent Constraint Programming: Denotation, Logic and Applications. Nord. J. Comput. 9(1): 145-188. ©NJC. 2002.
• [OV08a] C. Olarte and F. Valencia. The expressivity of universal timed CCP: Undecidability of monadic FLTL and closure operators for security. In PPDP. ©ACM, 2008.
• [OV08b] C. Olarte and F. Valencia.Universal concurrent constraint programing: Symbolic semantics and applications to security. In SAC. ©ACM, 2008.
• [RV04] C. Rueda and F. Valencia. On validity in modelization of musical problems by CCP. Soft Comput. 8(9): 641-648. ©Springer. 2004.
• Milner, R. (1989). Communication and Concurrency. International Series in Computer Science. Prentice Hall.
• Milner, R. (2001). The pi-calculus. Cambridge University Press.

Slides