Tesis doctoral de Carlos Rossi Jimenez
En este trabajo se definen dos lógicas temporales proposicionales sobre tiempo discreto, llamadas lnint y lnint-e respectivamente, que, en nuestra opinión, suponen un avance significativo al lograr integrar de modo natural puntos e intervalos, las visiones absoluta y relativa del tiempo y el tratamiento de eventos, procesos y hechos. Además, en la lógica lnint-e se introducen los conceptos de clases y ejecuciones de eventos. Su semántica es topológica, una destacada novedad respecto a la bibliografía existente en lógica de intervalos. Esta semántica aporta una gran simplificación a la demostración de los resultados teóricos y facilita el desarrollo en demostración automática de teoremas. en el área de razonamiento temporal, completamos dos de las tareas necesarias para la construcción de un demostrador automático de teoremas para lnint-e. concretamente, se eligen adecuadamente las fórmulas de lnint-e. Además, describimos un algoritmo eficiente que dada una fórmula arbitraria de lnint-e, la transforma en una fórmula equivalente que es una forma normal. La definición de forma normal se basa en un conjunto de transformaciones que simplifican las fórmulas de diferentes formas como, por ejemplo, la eliminación de constantes, la eliminación de conectivas binarias o la reducción del rango de éstas. por último, y para contrastar la utilidad de nuestras lógicas en computación, presentamos una especificación en lnint-e de la técnica de los diagramas de transición de estados. Aunque en la literatura se encuentran diversas formalizaciones de los diagramas de estados, ninguna de las que conocemos plantea la utilización de conectivas temporales de intervalos. Nuestra aproximación también es novedosa por la riqueza en la especificación de acciones asociadas a estados y transiciones.
Datos académicos de la tesis doctoral «Logica temporal de intervalos formalización de diagramas de estados«
- Título de la tesis: Logica temporal de intervalos formalización de diagramas de estados
- Autor: Carlos Rossi Jimenez
- Universidad: Málaga
- Fecha de lectura de la tesis: 12/01/2001
Dirección y tribunal
- Director de la tesis
- Inmaculada Perez De Guzman Molina
- Tribunal
- Presidente del tribunal: Francisco Trigueros ruiz
- federico Barber sanchis (vocal)
- david Pearce (vocal)
- alfredo Burrieza muñoz (vocal)