Logica Temporal

De WikiRA

La lógica temporal es una extensión de la lógica clásica para permitir la formalización de enunciados que incluyan precisiones acerca del momento del tiempo en que han tenido lugar. Nos permite diferenciar si un hecho tiene lugar en el presente, en el pasado o en el futuro.

Algunos sistemas lógicos basados en lógica temporal son:

  • Lógica computacional en árbol (Computational tree logic, CTL)
  • Lógica linear temporal (Linear temporal logic, LTL)
  • Lógica temporal de intervalos (Interval temporal logic, ITL)
  • Lógica de acciones temporal (Temporal Logic of Actions, TLA).


Contenido

Historia

Breve historia de las lógicas temporales:

  • Fue estudiada por primera vez por Aristóteles.
  • Inicialmente fue propuesta en los años 50 para investigaciones filosóficas.
  • Pnueli (1977) fue el primero en proponerlas para verificación. El sistema se especificaba como un sistema de axiomas, y se probaban propiedades a partir de estos axiomas.
  • Clarke y Emerson (1981) automatizaron este proceso dise˜nando algoritmos de verificación eficientes para ciertas lógicas temporales.
  • Más tarde comenzó a estudiarse la complejidad de verificación de estas lógicas (model-checking, parametrized complexity, ...)


Sistemas de transición

Las lógicas temporales permiten hablar sobre las transiciones entre estados (es decir, de las secuencias de computación realizadas por el sistema). Los sistemas deben ser modelados entonces como sistemas de transición.

Cuando hablemos de lógicas temporales:

Un sistema de transición (o estructura de Kripke) sobre alfabeto finito Σ es una estructura M = (E, (Pa) a \in \Sigma, R), donde:

  • E\, es un conjunto finito de elementos (estados),
  • Cada Pa\, es una predicado en E\,, i.e. Pa \subseteq E, y
  • R\, es una relación binaria en E\, (llamada relación de transición), tal que para cada e \in S existe e' \in S tal que R(e, e')\, .


Ejemplo

ME es un sistema de transición sobre alfabeto {a, b, c}.

La lógica temporal CTL

Lógica computacional en árbol especifica propiedades del árbol de computación de un sistema de transición. Este árbol (infinito) se obtiene designando a un estado del sistema como la raíz (estado inicial), y muestra todas las posibles computaciones desde ese estado.

Ejemplo

El árbol de transición para ME designando al estado verde (en la imagen anterior) es el siguiente:



CTL está compuesta por operadores temporales y cuantificación sobre caminos. La cuantificación sobre caminos está dada por los cuantificadores A (para todo camino) y E (existe un camino). Estos cuantificadores son utilizados en un estado particular del sistema de transición, y evaluadas sobre el árbol de computación relacionado con ese estado.

La lógica consiste en fórmulas de estado (que se evalúan en un estado del sistema) y de camino (que se evalúan en una rama del árbol).


Sintaxis

Los operadores temporales sirven para describir propiedades de un camino en el árbol de computación.

Además de los operadores del cálculo proposicional (\neg, \vee, \wedge, \rightarrow y \leftrightarrow), se introducirán, a nivel sintáctico, nuevos operadores referidos a los momentos del tiempo. Estos son:


Operador Ejemplo Significado
X NEXT X p p es cierto en el próximo estado
U UNTIL p U q p es cierto por lo menos hasta que se cumple q
F FUTURE F p En el futuro se cumplirá p
G GLOBALLY G p Globalmente cierto. Siempre se cumple p
B BEFORE p B q p se cumple antes que q


A partir de los operadores X y U podemos expresar el resto de operadores:

  • F q \equiv True  U p
  • G q \equiv \neg F \neg p
  • p B q \equiv \neg ((\neg p) U q)


Referencias

  • Mordechai Ben-Ari. Mathematic Logic for Computer Science (second edition), cap. 11, (2003)
  • Anthony Galton, Temporal Logic in the Stanford Encyclopedia of Philosophy[1]
Herramientas personales