Matías Lee defiende su Tesis Doctoral

Candidato a Doctorado: Matías D. Lee
Título de la tesis: Semánticas de procesos para sistemas interactivos y sistemas probabilísticos
Fecha: Miércoles 27 de marzo de 2013 a las 16:00 hs. Auditorio FaMAF.

Resumen:
Dado que los sistemas en la realidad presentan muchas complejidades se recurre a abstracciones para estudiar a los mismos. Estas abstracciones son denominadas procesos y las mismas tendrán distintas particularidades en función del estudio que se desee realizar. Una parte esencial de la Teoría de Procesos es definir cuando dos procesos deberían ser considerados iguales, porque procesos diferentes podrían exhibir el mismo comportamiento. Una semántica define formalmente el comportamiento observable de un proceso. Definido esto, podremos decir que dos procesos son equivalentes si presentan el mismo comportamiento observable.
Los Autómatas de Interfaces presentan un modelo basado en sistemas de transiciones con dos tipos de acciones observables: las acciones de entrada y las acciones de salida. Las acciones de entrada representan acciones que se realizan en el ambiente y generan un estímulo en el proceso; las acciones de salida, en cambio, representan acciones que genera el proceso y estimulan al ambiente. Entonces las acciones de entrada son controladas por el entorno y las acciones de salida son controladas por el proceso. Rob van Glabeek estudió en profundidad las distintas semánticas para sistemas de transiciones, para los cuales no existe la diferencia entre las acciones observables. Una vez establecidas las suposiciones que rigen a los modelos en los que estamos interesados se vuelve evidente que las semánticas definidas por van Glabbeek no son adecuadas para el nuevo contexto. Basados en su trabajo, realizamos un estudio sobre las posibles semánticas para éste.
Si las acciones observables de un autómata de interfaz son a su vez divididas en acciones de baja confidencialidad (acciones bajas) y acciones de alta confidencialidad (acciones altas), se obtiene una Interface Structure for Security (ISS). En este contexto, la propiedad de interés se denomina "No Interferencia". Si un proceso satisface esta propiedad, entonces un usuario que sólo puede interactuar con la interfaz a través de las acciones bajas no podrá deducir ningún tipo de información o actividad confidencial a través de las observaciones que realiza. En este trabajo se presentan dos variantes de la propiedad, se estudia cómo se relacionan estas variantes y cómo se comportan con la composición de interfaces. Además se presentan dos algoritmos: el primero decide si una interfaz satisface la propiedad; si la respuesta es negativa, el segundo, si es posible, refina una interfaz que sí satisface la propiedad a costa de simplificar la misma.
Los sistemas de transiciones pueden ser enriquecidos mediante la incorporación de elementos probabilísticos. Una posible opción para esto es que luego de ejecutar una acción el siguiente estado se elija de acuerdo a una distribución de probabilidad. Para especificar estos sistemas recurrimos a un enfoque algebraico, donde la semántica de los términos se definirá utilizando semántica operacional estructurada. Presentamos el formato de regla ntμfθ/ntμxθ el cual garantiza que la bisimulación es una congruencia para todo operador que se define utilizando el formato. Se presentan distintas reducciones del formato, entre ellas una reducción al formato probabilistic ntree. Se estudia además la construcción modular de especificaciones y se prueban algunos resultados estándares relacionados a extensiones conservativas. Finalmente se demuestra que la congruencia trazas para procesos con imagen finita inducida por nuestro formato es precisamente la bisimulación sobre este tipo particular de sistemas de transiciones.