Ir al contenido

Documat


Lógica temporal de intervalos, formalización de diagramas de estados

  • Autores: Carlos Rossi Árbol académico
  • Directores de la Tesis: Inmaculada Pérez de Guzmán Molina (dir. tes.) Árbol académico, Manuel Enciso García-Oliveros (dir. tes.) Árbol académico
  • Lectura: En la Universidad de Málaga ( España ) en 2001
  • Idioma: español
  • Tribunal Calificador de la Tesis: Francisco Andrés Triguero Ruiz (presid.) Árbol académico, Antonio Jesús Guevara Plaza (secret.) Árbol académico, David Pearce (voc.) Árbol académico, Federico Barber Sanchís (voc.) Árbol académico, Alfredo Burrieza Muñiz (voc.) Árbol académico
  • Texto completo no disponible (Saber más ...)
  • Resumen
    • 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.


Fundación Dialnet

Mi Documat

Opciones de tesis

Opciones de compartir

Opciones de entorno