Diferencias

Muestra las diferencias entre dos versiones de la página.

Enlace a la vista de comparación

materias:modelamiento_computacional_de_procesos [2011/03/14 11:27]
abarco [Contenido]
materias:modelamiento_computacional_de_procesos [2011/03/14 11:31] (actual)
abarco [Material de este semestre]
Línea 1: Línea 1:
 +====== Modelamiento Computacional de Procesos ====== 
  
 +===== Description =====
 +
 +This course is an introduction to process calculi for modeling  real-life systems  such as for example Security Protocols and Biological Systems.
 +===== Información Básica =====
 +  * Profesor: [[mailto:frank.valencia@lix.polytechnique.fr|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  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. 
 +
 +
 +===== Contenido =====
 +
 +
 +^Temas ^Sesión
 +| 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 pi-calculus. |
 +| Pi-calculus 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): 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.
 +
 +
 +===== Material de este semestre =====
 +
 +{{:materias:puj-ccs-2010.pdf|Slides}}
 
materias/modelamiento_computacional_de_procesos.txt · Última modificación: 2011/03/14 11:31 por abarco
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki