Curso Dr. Jorge Pérez

Modelos Formales de Concurrencia: Lenguajes y Expresividad

 

Resumen

Concurrencia es un concepto predominante en informática. Los sistemas de cómputo concurrentes involucran múltiples agentes (procesos) que interactúan entre si; a diferencia de los sistemas secuenciales, estas interacciones pueden ser infinitas y difíciles de describir. Los cálculos de procesos permiten especificar y analizar sistemas concurren- tes de modo preciso: se trata de lenguajes formales que capturan aspectos esenciales de la computación concurrente.

El curso introduce los fundamentos de los cálculos de procesos, ofreciendo una combinación de resultados clásicos y recientes. Primero, se presentan dos de los cálculos más representativos (CCS, cálculo pi) y sus técnicas de análisis. En cada caso, herramientas de software que implementan dichas técnicas serán discutidas. Luego se presentan los cálculos de procesos de alto orden: variantes concurrentes del cálculo lambda que admiten el paso de procesos como parámetros en las comunicaciones. El curso enfatiza en la expresividad de los cálculos de procesos como una de sus propiedades fundamentales. Estudios de expresividad permiten, por ejemplo, caracterizar los sistemas que un cálculo puede representar, o transferir técnicas de análisis de un cálculo a otro.

 

Programa tentativo

El curso será dictado en castellano. Se asume familiaridad con conceptos básicos en lógica, matemáticas discretas, teoría de automátas, y cálculo lambda. Los conceptos teóricos serán reforzados por medio de casos de estudio que analizarán dichos conceptos en la práctica, por medio de herramientas y/o ejemplos extendidos.

  1. CCS: más alla de la computación secuencial: Sintaxis y semánticas (de reducción, etiquetada y sus diferencias) − Ejemplos y aplicaciones − Técnicas de análisis: bisimilaridad. Bisimilaridad fuerte y débil − Caso de estudio: The Edinburgh Concurrency Workbench
  2. Cálculo π: la necesidad de movilidad en concurrencia: Sintaxis y semántica (early vs. late) / Contraste con CCS − Visimilaridades en un contexto móvil − Subcálculos y extensiones − Casos de estudio: el lenguaje de programación PICT, The Mobility Workbench, The Spatial Logic Model Checker (SLMC).
  3. Cálculos de procesos de alto orden: comunicando programas concurrentes − Sintaxis y semántica / Contraste con CCS y π − Bisimilaridad en el alto orden: definiciones y comparación − Comunicación de alto orden al mínimo: el cálculo HOcore − Bisimilaridad en HOcore − Caso de estudio: la familia de cálculos Kell - lenguaje, semántica, aspectos de implementación.
  4. La expresividad de los cálculos de procesos: Definiciones básicas / Criterios de expresividad − Clases de resultados de expresividad y técnicas asociadas − Resultados de separación en CCS y π − Funciones como procesos I − Representando comunicación de alto orden en el cálculo π
  5. La expresividad de los cálculos de procesos de alto orden: Representando comportamiento infinito en cálculos de alto orden − Funciones como procesos II − Expresividad de HOcore y sus variantes (forwarding, asincronía vs. sincronía) − Caso de estudio: procesos adaptables y sus aplicaciones

 

Lenguajes y Herramientas

Los conceptos teóricos del curso se complementarán con la presentación de algunos lenguajes y herramientas que implementan dichos conceptos. Un listado tentativo de dichas herramientas es el siguiente:

− The Pict Programming Language http://www.cis.upenn.edu/~bcpierce/papers/pict/Html/Pict.html

− The Edinburgh Concurrency Workbench http://homepages.inf.ed.ac.uk/perdita/cwb/

− The Mobility Workbench http://www.it.uu.se/research/group/mobility/mwb

− The Spatial Logic Model Checker for Concurrency, Distribution and Mobility (SLMC) http://ctp.di.fct.unl.pt/SLMC/

 

Bibliografía recomendada

− Philippe Bidinger, Alan Schmitt, Jean-Bernard Stefani:An Abstract Machine forthe Kell Calculus. In Proceedings of FMOODS 2005: 31-46,  LNCS,  Springer.

− Mario Bravetti,  Cinzia Di Giusto,  Jorge A. Pérez,  Gianluigi Zavattaro: Adaptable Pro- cesses. In Proceedings of FMOODS/FORTE 2011: 90-105,  LNCS,  Springer.

− Daniele Gorla. Towards a unified approach to encodability and separation results for process calculi. Inf. Comput. 208(9): 1031-1053 (2010)

− Robin Milner. Communication and Concurrency. Prentice Hall,  1989. 

− Robin Milner: Functions as Processes. Math. Struct. in Comp. Science 2(2): 119-141 (1992) 

− Ivan Lanese, Jorge A. Pérez, Davide Sangiorgi, Alan Schmitt:On the expressiveness and decidability of higher-order process calculi. Inf. Comput. 209(2): 198-226 (2011) 

− Jorge A. Pérez. Higher-Order Concurrency: Expressiveness and Decidability Results. Ph.D. Thesis,  University of Bologna,  2010.

− Davide Sangiorgi and David Walker. The pi-calculus: a Theory of Mobile Processes. Cambridge University Press,  2001.

− Davide Sangiorgi. Expressing mobility in process algebras: First-order and higher-order paradigms. Ph.D. thesis,  University of Edinburgh,  1993.

− Alan Schmitt,  Jean-Bernard Stefani. The Kell Calculus: A Family of Higher-Order Dis- tributed Process Calculi. Global Computing 2004: 146-178,  LNCS,  Springer.

 

Un listado de referencias adicionales será ofrecido al final del curso.