Resumen de Lógica temporal de intervalos, formalización de diagramas de estados
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.
