Objetivo General de la Materia
El objetivo general de este curso es el iniciar al alumno en el estudio de la comu-
nicación y concurrencia, enfatizando el uso de CCS [6], una álgebra de procesos,
para la especificación, desarrollo y análisis formal de sistemas de comunicación.
De manera secundario, el objetivo de este curso es familiarizar al alumno con el
uso de herramientas en este dominio, tales como el "Concurrency Workbench"
[1], PAM [4] y el Concurrency Factory (http://www.cs.sunysb.edu/ concurr/.)

Objetivos Generales por Tema

1.Introducir aspectos básicos de la comunicación, así como algunos modelos
propuestos para su estudio, motivando el curso;.

2.Introducir CCS ("a Calculus of Communicating Systems") a través de
teoría y ejemplos; CCS es un álgebra de procesos diseñada para modelar
y analizar sistemas de comunicación;

3.Motivar el por qué requerimos definir el concepto de equivalencia de pro-
cesos y el cuándo debemos considerar dos procesos equivalentes; además,
introducir una teoría basada en observaciones, la cual produce una rela-
ción intuitiva de equivalencia entre procesos capaz de discernir aspectos
operacionales y de comportamiento de suma importancia;

4.Introducir relaciones de equivalencia entre procesos más generosas y que
disfrutan de propiedades teóricas más interesantes, desde un punto de vista
práctico; aplicar el álgebra de procesos y los conceptos de equivalencia en la
especificación, desarrollo y estudio de sistemas de comunicación de interés
industrial;
 

5.Ejercitar el uso de leyes algebraicas en la verificación de sistemas, en par-
ticular en aquellos sistemas cuya naturaleza operacional imponen restric-
ciones al uso de bisimulación como un método de demostración;

6.Resolver problemas de interés, al mismo tiempo que se introduce una
taxonomía de procesos; y
 

7.Discutir problemas, teóricos y prácticos, que actualmente se estudian en
varios centros de investigación.
 

 
 
Temario
 

 
1.Sistemas de Comunicación: Diferentes Modelos
 

(a) Medios de comunicación
 

(b) Aspectos de comunicación
 

(c) Igualdad de procesos: una teoría basada en observaciones
 

Referencias bibliográficas: [6, 3, 2]
 

2.CCS: Definiciones Básicas
 

(a) Acción
 

(b) Sincronisación
 

(c) Sintaxis
 

(d) Semántica: Sistemas de transición etiquetado
 

(e) Derivativas, árboles de transición y gráfos de transición
 

(f) Tipos
 

(g) Recursión
 

(h) Ejemplo 1: Un buffer de longitud arbitraria
 

(i)Ejemplo 2: Un protocolo simple de comunicación
 

Referencias bibliográficas: [6, 10, 5]
 

3.Bisimulación Fuerte y Equivalencia Fuerte
 

(a) ¿Qué significa que dos procesos sean equivalentes?
- No-determinismo
 

(b) Bisimulación fuerte
 

(c) Equivalencia fuerte
 

(d) Propiedades de la equivalencia fuerte
 

(e) Una bisimulación es un punto fijo
 

(f) Ejemplos
 

Referencias bibliográficas: [6]
 

4.Bisimulación, Equivalencia Observacional e Igualdad
 

(a) Bisimulación
 

(b) Equivalencia observacional o bisimilaridad
 

(c) El checar bisimilaridad es un juego
 

(d) Propiedades de bisimilaridad
 

(e) Ejemplos
 

- especificación de una agenda
 

- desarrollo de una agenda
 

- verificación de la agenda
 

(f) Igualdad u observación congruente
 

(g) Propiedades de la igualdad
 

(h) Mas ejemplos
 

Referencias bibliográficas: [6, 8, 9]
 

5.Leyes Ecuacionales: Aplicación
 

(a) Clasificación de combinadores
 

(b) Leyes dinámicas
 

- Ley de expansión
 

(c) Leyes estáticas
 

(d) Solución única de ecuaciones
 

Referencias bibliográficas: [6]
 

6.Ejemplos
 

(a) Sistemas con estructura dinámica
 

(b) Sistemas con estructura inductiva
 

(c) Verificación de un protocolo de comunicaciones
 

Referencias bibliográficas: [6, 7]
 

7.Tópicos selectos
 

 
 
Objetivos Específicos de Aprendizaje
 

 
1.Sistemas de Comunicación: Diferentes Modelos
 

(a) Medios de comunicación: Introducir conceptos asociados con medios
de comunicación.
 

(b) Aspectos de comunicación: Explorar modelos que permitan construir
una teoría que capture ideas operacionales sobre el proceso de comu-
nicaciones.
 

(c) Igualdad de procesos: mostrar que la noción de observar un dispositi-
vo produce una teoría poderosa pero simple para modelar, de manera
algebraica, las características básicas de un sistema de comunicacio-
nes.
 

2.CCS: Definiciones Básicas
 

(a) Acción: Introducir el elemento básico del lenguaje, la acción discreta;
mostrar cómo usar acciones para mostrar los aspectos externos de
comportamiento de un proceso.
 

(b) Sincronisación: Distinguir la sincronización como la ejecución si-
multánea de una acción discreta por dos procesos independientes.
Mostrar por qué estas acciones no pueden observarse; es decir, son
internas, por lo que intuitivamente no contribuyen a los aspectos ex-
ternos en el comportamiento de un proceso.
 

(c) Sintaxis: Introducir formalmente la sintaxis del lenguaje, mostrada
previamente mediante ejemplos
 

(d) Semántica: Sistemas de transición etiquetado: El alumno entenderá
cómo un sistema de transiciones puede usarce para darle vida a las
expresiones del lenguaje.
 

(e) Derivativas, árboles de transición y gráfos de transición: El alumno
aplicará la semántica del lenguaje para calcular las transiciones de
un proceso y distinguirá por qué tales transiciones representan el
comportamiento de un proceso. Para ello, el alumno hará uso de
grafos.
 

(f) Tipos: El alumno aprenderá a calcular el tipo de un proceso, distin-
guiendo la diferencia entre tipo y tipo sintáctico.
 

(g) Recursión: El alumno usará la semántica del lebguaje para expresar
aspectos de comportamiento repetitivo e invariante en el tiempo.
 

El alumno usará apropiadamente el material revisado en clase para
conducir algunos experimentos en una de las herramientas arriba
mencionadas (se recomienda el "Concurrency Workbench" - CWB)
 

3.Bisimulación Fuerte y Equivalencia Fuerte
 

(a) ¿Qué significa que dos procesos sean equivalentes?: Motivar por qué
en el análisis de procesos necesitamos una relación de equivalencia
distinta a sus predecesoras, enfatizando el comportamiento entre pro-
cesos.
 

(b) Bisimulación fuerte: En esta sección y las posteriores introducimos
una relación de equivalencia basada en comportamiento; esta relación
es preliminar en el sentido de que, aún cuando capta ideas básicas
de operación, no es capaz de tratar a las acciones de sincronización
como invisibles o no-observables.
 

(c) Equivalencia fuerte
 

(d) Propiedades de la equivalencia fuerte
 

(e) Una bisimulación es un punto fijo
 

(f) Ejemplos
 

Al culminar este tema, el alumno será capaz de usar el CWB para mostrar
equivalencia fuerte entre procesos.
 

4.Bisimulación, Equivalencia Observacional e Igualdad
 

(a) Bisimulación: El objetivo de este subtema y los tres siguientes es
introducir al alumno en la teoría de equivalencia observacional: de-
finición de bisimulación, bisimilaridad y sus propiedades, y métodos
para decidir bisimilaridad.
 

(b) Equivalencia observacional o bisimilaridad
 

(c) El checar bisimilaridad es un juego
 

(d) Propiedades de bisimilaridad
 

(e) Ejemplos: El objetivo de este subtema es el adecuar y entrenar al
alumno en el uso correcto de los métodos arriba mencionados para
conducir la tarea de la equivalencia entre procesos y el problema de
verificación.
 

(f) Igualdad u observación congruente: En esta sección mostramos que
bisimilaridad, pese a poseer propiedades operacionales interesantes
carece de la propiedad teórica de ser congruente; definimos igual-
dad como la máxima relación de equivalencia congruente incluida en
bisimilaridad.
 

(g) Propiedades de la igualdad
 

Al concluir este tema, el alumno habrá conducido al menos dos experi-
mentos en la verificación de procesos de tamaño considerable.
 

5.Leyes Ecuacionales: Aplicación
 

(a) Clasificación de combinadores: Clasificar los operadores en ter'minos
de su interpretación.
 

(b) Leyes dinámicas: Usando la clasificación arriba descrita, en este sub-
tema y su sucesor mostramos leyes fundamentales algebraicas que
estos operadores poseen. Concluimos el tema respondiendo a la pre-
gunta >Cuál sería el conjunto mínimo de leyes algebraicas que debe-
mos incluir en un sistema que tenga el mismo poder de deducción
que el método para decidir equivalencia basado en bisimulaciones?
 

(c) Leyes estáticas
 

(d) Solución única de ecuaciones: Introducir al alumno una regla de in-
ferencia que permite mostrar, a través de ecuaciones, sí dos procesos
son iguales o nó.
 

6.Ejemplos: El objetivo específico de este tema es el entrenar al alumno en
el uso correcto de las técnicas estudiadas a lo largo del curso en sistemas
con aspectos diferentes de comportamiento externo. El aprendizaje se
conduce por casos; el ejercicio es verificación de sistemas de comunicación
y se sugiere uso activo de herramientas.
 

7.Tópicos selectos: Los temas incluidos en esta sección son abiertos, se-
leccionados a discreción del instructor. El propósito de este ejercicio es
discutir, a nivel estado del arte, aquellos temas en que el instructor halla
notado mayor cautivación en los alumnos.
 

 
 
Bibliografía
 

 
El libro de Robin Milner, [6], es el libro de texto; el resto de las referencias
bibliográficas constituyen material de apoyo.
 

 
 
Tiempo Estimado por Tema
 

 
 
Evaluación del Curso
 

 
 
Referencias
 

[1]R. Cleaveland, P. J., and B. Steffen. The concurrency workbench: A semantics-
based verification tool for finite-state systems. In Proceedings of the Workshop on
Automated Verification Methods for Finite-State Systems. Springer-Verlag, 1989.
[2]M. Hennessy. Algebraic Theory of Processes. The MIT Press, Cambridge, Mass,
1988.
[3]C. A. Hoare. Communicating Sequential Processes. Communications of the As-
sociation for Computing Machinery, 21(8):666-677, 1978.
[4]H. Lin. PAM: A Process Algebra Manipulator. Formal Methods in System Design,
7:243-259, 1995.
[5]R. Milner. Operational and Algebraic Semantics of Concurrent Processes. LFCcS
Report Series ECS-LFCS-88-46, Department of Computer Science, University of
Edinburgh, 1988. Chapter for the Handbook of Theoretical Computer Science.
[6]R. Milner. Communication and Concurrency. Prentice Hall, London, 1989.
[7]R. Monroy. Planning Proofs of Correctness of CCS Systems. PhD thesis, Edin-
burgh University, 1997. Defended on 9th January, 1998.
[8]C. Stirling. An Introduction to Modal and Temporal Logics for CCS. In 1989
UK/Japan workshop on concurrency, Lecture Notes in Conputer Science, v.491,
pages 2-20. Springer-Verlag, 1990.
[9]C. Stirling. Modal and Temporal logics for Processes. LFCS Report Series ECS-
LFCS-92-221, Department of Computer Science, University of Edinburgh, 1992.
Lecture notes for the VIIIth Banff higher-order workshop: Logics for concurrency:
Structure vs Automata, August 1994.
[10]D. Walker. Introduction to a Calculus of Communicating Systems. Report ECS-
LFCS-86-22, Department of Computer Science, University of Edinburgh, August
1988.