Más sobre equivalencias lógicas y distancias entre procesos

Resumen

Esta tesis se enmarca en el amplio campo de la teoría de la concurrencia. Más específicamente, nos centramos en el estudio de las relaciones de similitud entre procesos concurrentes. Comenzamos estudiando la bisimulación, considerada la más importante de estas relaciones, y vemos después cómo podemos extender nuestros resultados al resto de las semánticas de procesos estudiadas durante las últimas décadas. En particular, nuestra contribución a la comunidad científica, se centra en dos puntos principales: - El desarrollo de una caracterización lógica uniforme de las semánticas de procesos: proponemos un esquema lógico común (enmarcado en la conocida lógica modal de Hennessy-Milner e incluimos las diferentes semánticas en este esquema, enfatizando las diferencias y similitudes entre ellas, que se presentan del modo más claro posible. - La presentación de una nueva noción de distancia, tanto entre procesos finitos como infinitos: la misma se diferencia de las anteriormente propuestas en su carácter global, que acumula las diferencias que aportan los distintos cómputos, en lugar de quedarnos con la máxima de ellas. La primera parte de nuestra investigación continúa la tarea comenzada por el Prof. Carlos Gregorio Rodríguez y mi propio director, el Prof. David de Frutos Escrig. Las distintas nociones de semánticas de procesos fueron recopiladas en los años noventa por Rob J. van Glabbeek, quien estableció las relaciones existentes entre ellas en su famoso linear time-branching time spectrum. C. Gregorio y D. de Frutos pusieron estas semánticas bajo un marco común, clarificando dichas relaciones. Su trabajo dotó al spectrum de R. J. van Glabbeek de una estructura mucho más ordenada, y permitió tener una visión unificada de las características de dichas semánticas. Nuestra caracterización lógica completa este trabajo unificador y nos permite descubrir nuevas semánticas desconocidas hasta la fecha. Además, explotando la dualidad existente entre nuestro marco lógico y el marco observacional (desarrollado por mis compañeros), se ponen aún más de manifiesto las características definidoras de cada una de las semánticas. Una vez que completamos el estudio de las relaciones entre las diferentes semánticas de procesos, apareció de forma natural la siguiente cuestión: ¿Qué ocurre con los procesos que no son equivalentes con respecto a la semántica considerada?. Distintas nociones de distancia entre procesos han sido estudiadas por diferentes autores a lo largo de los últimos años. Entre ellas destacan los estudios dirigidos por Thomas A. Henzinger y Ulrich Fahrenberg, que se apoyan en diversas variantes del llamado juego de bisimulación cuantitativo. Esta noción de distancia sólo tiene en cuenta la máxima diferencia entre los procesos y no todas ellas en su conjunto. Por ello, nosotros proponemos aquí una nueva noción de distancia, con la que somos capaces de realizar una medida más precisa de las diferencias entre procesos con respecto a las distintas semánticas del spectrum. Además podemos extenderla para trabajar con procesos infinitos, utilizando la coinducción como recurso básico para comparar los comportamientos infinitos.