Semánticas de pruebas para álgebras de procesos probabilísticos

Laburpena

En esta tesis presentamos un algebra de procesos que ha sido extendida con información probabilística. Definimos una semántica operacional para nuestro lenguaje, y a continuación definimos una semántica de pruebas parametrizadas por una cierta familia de pruebas. La caracterización vendrá dada por la probabilidad con la que los procesos pasan las pruebas del conjunto dado. Una vez definido el marco general, consideraremos dos conjuntos de pruebas los cuales estarán asociados a una interpretación de los modelos reactivos y generativo respectivamente. Para la interpretación del modelo reactivo daremos una caracterización alternativa de la semántica pruebas, la cual esta basada en trazas probabilísticas. Dado que el operador de elección externa no es congruente, definimos una semántica denotacional para el lenguaje en el que no se considera la elección externa. Esta semántica denotacional es completamente abstracta con respecto a la semántica de pruebas. Para la interpretación generativa, definimos una caracterización alternativa basada en conjuntos de aceptación probabilísticos y una semántica denotacional basada en árboles de aceptación probabilísticos. Además, para este modelo definimos una semántica axiomatica. Demostramos que todas estas semánticas son equivalentes a la semántica de pruebas para el modelo generativo. A continuación damos una serie de ejemplos en los cuales mostramos la utilidad de nuestro lenguaje a la hora de especificar sistemas concurrentes que dependen de información probabilística. Finalizamos extendiendo nuestro lenguaje con un operador de composición paralela y discutiendo los problemas que presenta incluir un operador de restricción.