Técnicas coalgebraicas y categóricas para el estudio de las semánticas de procesos.

Resumen

De un modo general, esta tesis puede englobarse dentro del estudio de los sistemas de procesos y, muy especialmente, del estudio de las relaciones entre esos procesos mediante bisimulación y simulación (abreviadamente (bi)simulación). Además, los res ultados que aquí aparecen están sustentados en gran parte por el marco general de la teoría de categorías y, más concretamente, en el de las coálgebras en el que Jesse Hughes y Bart Jacobs propusieron una definición general de simulación entre coálge bras. La noción de simulación entre coálgebras se apoya en los conceptos de orden funtorial y alzamiento de relaciones; la bisimulación entre coálgebras es un caso particular de simulación (en la que el orden funtorial es la igualdad). La (bi)simula ción coalgebraica permite disponer de un único concepto general cuyas instancias definen las nociones concretas para sistemas de transiciones (LTS), estructuras de Kripke, etc. No obstante no todo orden funtorial define una relación de similitud corr ecta pues, en concreto, es necesario que se cumpla la condición de estabilidad para asegurar que la composición de simulaciones es también una simulación, y así garantizar que la similitud sea una relación transitiva. Podemos considerar dos partes e senciales en esta tesis: en la primera explotamos la potencia de la definición coalgebraica de simulación para obtener resultados generales, mientras que en la segunda nos centramos en el estudio de dos nuevas nociones de simulación que hemos propues to, pero en esta ocasión desde un punto de vista más clásico al estilo de los resultados de van Glabbeek. En primer lugar, estudiamos bajo qué condiciones las instancias de dichas nociones categóricas generales de (bi)simulación permiten traspasar p ropiedades entre las estructuras relacionadas, es decir, en qué condiciones se puede generalizar al mundo coalgebraico los resultados clásicos de reflexión y preservación de propiedades lógicas mediante bisimulaciones, y la preservación mediante simu laciones. Nuestra conclusión es que, si bien para el caso de las bisimulaciones se obtiene la deseada generalización, para el caso de la simulación es necesario restringir los órdenes que participan en la definición de simulación propuesta de Hughes y Jacobs, obteniéndose en este caso resultados parciales. También estudiamos cómo las transformaciones naturales entre funtores permiten unificar nociones de (bi)simulación entre distintos tipos de estructuras, obteniendo resultados de representació