Jugando con el tiempo : semántica de pruebas para algebras de procesos temporizadas

Abstract

en el presente trabajo hemos estudiado la semántica de pruebas para alebras de procesos temporizadas. En primer lugar hemos estudiado un álgebra de procesos temporizada básica, se trata de un lenguaje recursivo, secuencial no determinista. Puesto que las semánticas de pruebas son poco manejables, se hace necesario dar una caracterización alternativa de la misma; nosotros hemos dado una caracterizacion que depende unicamente de la semántica operacional de álgebra. A continuación hemos dotado al álgebra de una semántica denotacional, que ha resultado ser completamente abstracta con respecto a la semántica de pruebas. Seguidamente hemos estudiado una semántica axiomática, puesto que conseguimos probar que esta ultima es correcta y completa con respecto a la semántica detonaciones tenemos inmediatamente que tambien será correcta y completa con respecto a la semántica de pruebas. Puesto que todo lo anterior lo habíamos hecho con un álgebra bastante simple, es necesario introducir operadores mas complejos. En concreto hemos estudiado una serie de operadores que aparecen en la mayoria de las alebras de procesos temporizadas: . El operador de paralelo. El operador de ocultamiento, y. El operador de prefijo mediante acción visible con intervalo de tiempo. Por ultimo hemos estudiado un operador de elección tipo ccs, que tiene los problemas típicos con respecto a la congruencia