Jugando con el tiempo.

Tesis doctoral de Llana Diaz Luis Fernando

En el presente trabajo hemos estudiado la semantica de pruebas para algebras de procesos temporizadas. En primer lugar hemos estudiado un algebra de procesos temporizada basica, se trata de un lenguaje recursivo, secuencial no determinista. Puesto que las semanticas de pruebas son poco manejables, se hace necesario dar una caracterizacion alternativa de la misma; nosotros hemos dado una caracterizacion que depende unicamente de la semantica operacional de algebra. A continuacion hemos dotado al algebra de una semantica denotacional, que ha resultado ser completamente abstracta con respecto a la semantica de pruebas. Seguidamente hemos estudiado una semantica axiomatica, puesto que conseguimos probar que esta ultima es correcta y completa con respecto a la semantica denotacional tenemos inmediatamente que tambien sera correcta y completa con respecto a la semantica de pruebas. puesto que todo lo anterior lo habiamos hecho con un algebra bastante simple, es necesario introducir operadores mas complejos. En concreto hemos estudiado una serie de operadores que aparecen en la mayoria de las algebras de procesos temporizadas: . El operador de paralelo, . El operador de ocultamiento, y . El operador de prefijo mediante accion visible con intervalo de tiempo. por ultimo hemos estudiado un operador de eleccion tipo ccs, que tiene los problemas tipicos con respecto a la congruencia.

 

Datos académicos de la tesis doctoral «Jugando con el tiempo.«

  • Título de la tesis:  Jugando con el tiempo.
  • Autor:  Llana Diaz Luis Fernando
  • Universidad:  Complutense de Madrid
  • Fecha de lectura de la tesis:  01/01/1996

 

Dirección y tribunal

  • Director de la tesis
    • Frutos Escrig David De
  • Tribunal
    • Presidente del tribunal: Mario Rodríguez Artalejo
    • Fernando Orejas Valdés (vocal)
    • Javier Esparza Esaun (vocal)
    • Javier Campos Laclaustra (vocal)

 

Deja un comentario

Tu dirección de correo electrónico no será publicada. Los campos obligatorios están marcados con *

Scroll al inicio