RT Dissertation/Thesis
T1 Técnicas Coalgebraicas y  Categóricas para el estudio de las semánticas de procesos
A1 Fábregas Alfaro, Ignacio
AB 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 mediantebisimulación y simulación (abreviadamente (bi)simulación). Además, los resultados que aquí aparecen están sustentados en gran parte por el marco general de la teoría decategorí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álgebras. 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)simulación coalgebraica permite disponer de un único concepto general cuyas instancias definen las nociones concretas para sistemas de transiciones (LTS), estructurasde Kripke, etc. No obstante no todo orden funtorial define una relación de similitud correcta pues, en concreto, es necesario que se cumpla la condición de estabilidad paraasegurar 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 esenciales en esta tesis: en la primera explotamos lapotencia 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 propuesto, 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 nocionescategóricas generales de (bi)simulación permiten traspasar propiedades 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 simulaciones. Nuestra conclusión es que, si bien para el caso de las bisimulaciones se obtiene la deseada generalización, para el caso de lasimulació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ón de las coálgebras entre los distintos funtores relacionados por la transformación natural. En particular, unificamos los sistemas probabilísticos y los sistemas de transiciones en el modelo de los sistemas de multitransiciones. Para finalizar la primera parte de la tesis, profundizamos en el estudio de la no ción de simulación coalgebraica y de la condición necesaria de estabilidad, para llegar a entender cómo se pueden definir nociones de simulación dentro del marco coalgebraico que definan relaciones de similitud con buenas propiedades. En concreto, ilustramos nuestros resultados teóricos definiendo dos nuevas nociones de simulación sobre sistemas de transiciones etiquetados: la simulación covariante-contravariante (cc-simulación) y lasimulación conforme. La segunda parte de la tesis está dedicada al estudio de las dos nociones de simulaciónque hemos nombrado. Para las dos nociones de simulación construimos su caracterización lógica y axiomática. Además, para el caso de la simulación covariante-contravariante,estudiamos también su estrecha relación con los refinamientos modales sobre sistemas de transiciones modales (MTS) construyendo transformaciones de los LTS módulo ccsimulación y los MTS módulo refinamiento modal, y viceversa. Asimismo, construimos las fórmulas características de los LTS módulo cc-simulación y cómo estas representan procesos, es decir, la representación gráfica de las fórmulas.
PB Universidad Complutense de Madrid
YR 2012
FD 2012-11-06
LK https://hdl.handle.net/20.500.14352/48372
UL https://hdl.handle.net/20.500.14352/48372
LA spa
NO Tesis inédita de la Universidad Complutense de Madrid, Facultad de Ciencias Matemáticas, Departamento de Sistemas Informáticos y Programación, leída el 16-03-2012
DS Docta Complutense
RD 4 abr 2025