Description
This course is an introduction to process calculi for modeling reallife systems such as for example Security Protocols and Biological Systems.
Información Básica

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.
Acerca del Curso
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 lambdacalculus 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 PiCalculus. 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 abovementioned calculi to reallife systems. The students will present this final part of the course.
Contenido
Temas 

Basic concepts for automata theory. 
Bisimilarity equivalence. 
General aspects of process calculi. 
Syntax and Semantics. 
Bisimilarity. 
Observable Behavior and other equivalences. 
Hennessy and Milner Logic. 
Verification and specification. 
Synchronous and asynchronous picalculus. 
Picalculus encodings. 
Evaluacion
Porcentaje  

Homeworks  70 % 
Final presentation  30 % 
Bibliografía

[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): 117137.© Elsevier. 2007

[NPV02] M Nielsen, C. Palamidessi and F. Valencia. Temporal Concurrent Constraint Programming: Denotation, Logic and Applications. Nord. J. Comput. 9(1): 145188. ©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): 641648. ©Springer. 2004.

Milner, R. (1989). Communication and Concurrency. International Series in Computer Science. Prentice Hall.

Milner, R. (2001). The picalculus. Cambridge University Press.
Material de este semestre