Resumen de Pnal. Un modelo algebraico para procesos probabilísticos y no deterministas
En esta tesis presentamos un modelo algebraico para procesos probabilisticos y no deterministas (PNAL), que extiende el modelo EPL de M, Hennessy(Algebraic Theory of Processes, MIT Press, 1988).
La sintexis de PNAL es una extension de la de EPL que mantiene los dos operadores clasicos de eleccion (eleccion interna y eleccion externa) y ademas introduce un nuevo operador de eleccion, la eleccion probabilistica.
Hemos definido la semantica operacional de PNAL, por medio de un sistema de transicion etiquetado en donde aparecen 3 grupos de reglas de transicion, cada uno de los esta cuales relacionado con uno de los tipos de transicion, posibles : probabilistica, observales y no observables.
Tomando como base la semantica operacional, definimos una semantica de pruebas que consiste, como es habitual, en estudiar las respuestas de los procesos a los tests. La existencia en nuestro modelo de una eleccion probabilistica introduce una nueva variable en el problema, ya que ahora no nos bastara con saber si un proceso puede o debe satisfacer un test, sino que ahora debemos generalizar el problema y "calcular" con que probabilidad (o conjunto de probabilidades) un proceso satisface un test.
Posteriormente hemos definido una semantica denotacional en la que los objetos del dominio semantico, los arboles de aceptacion probabilisticos o PAT, constituyen una extension muy intuitiva de los arboles de aceptacion AT dfinidos en [Hen88]. Se han obtenido dos resultados: en primer lugar que procesos equivalentes en EPL siguen siendolo en nuestro modelo, y en segundo lugar que la semantica denotacional y la semantica de pruebas identifican los mismos procesos.
Finalmente, se aborda el estudio del estudio del sistema de axiomas y reglas.
Tomando como punto de partida el sistema de prueba para EPL, hemos estudiado que ecuaciones, inecuaciones y reglas seguian siendo validas en el caso probabilistico. Posteriormente hemos añadido los axiomas relacionadoso
