Lógica temporal

La lógica temporal es un tipo de lógica modal usada para describir un sistema de reglas y simbolismos para la representación y el razonamiento sobre proposiciones en las que tiene presencia el factor tiempo. Existe una cierta relación con otras variedades de lógica, por ejemplo, la lógica modal. Su estudio tiene una cierta importancia dentro del estudio de la informática, en particular los desarrollos introducidos por Amir Pnueli.

Por ejemplo, tomemos la sentencia: "Tengo hambre"; aunque su significado es independiente del tiempo, el valor de verdad o falsedad de la misma puede variar con el tiempo en un determinado sistema que incluya acciones de comer; así, en función del sistema, algunas veces será cierta y otras falsa, aunque nunca será cierta y falsa simultáneamente.

Historia

La lógica temporal fue estudiada por primera vez por Aristóteles, en algunos de sus escritos aparecen expresiones que guardan una semejanza con una lógica temporal de primer orden; así aparecen expresiones con cuantificadores existenciales y cuantificadores universales, junto a secuencias de estados de un orden temporal, lo que, en la práctica es una lógica temporal.

Sistemas basados en lógica temporal

En lógica temporal aparecen los mismos operadores que en una lógica de primer orden, junto con otros nuevos, entre los que se pueden encontrar: Siempre, algunas veces y nunca.

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) y Lógica temporal de intervalos (Interval temporal logic, ITL). Lógica de acciones temporal (Temporal Logic of Actions, TLA).

Operadores temporales

La lógica temporal tiene dos clases de operadores: operadores lógicos y operadores modales [1]. Los operadores lógicos son usualmente operadores truth-functional ($\neg ,\lor ,\land ,\rightarrow$). Los operadores modales usan el Linear Temporal Logic y Computation Tree Logic son definidos como sigue.

Textual	Símbólico	Definición	Explicación	Diagrama'
Operadores binarios
$\phi$ U $\psi$	$\phi ~{\mathcal {U}}~\psi$	${\begin{matrix}(B{\mathcal {U}}C)(\phi )=\\(\exists i:C(\phi _{i}))\land (\forall j<i:B(\phi _{j}))\end{matrix}}$	Until: $\psi$ se cumple en el estado actual o uno posterior, y $\phi$ se tiene que cumplir hasta esa posición. A partir de esa posición $\phi$ no es necesario que se siga cumpliendo.
$\phi$ R $\psi$	$\phi ~{\mathcal {R}}~\psi$	${\begin{matrix}(B{\mathcal {R}}C)(\phi )=\\(\forall i:C(\phi _{i}))\lor (\exists j<i:B(\phi _{j}))\end{matrix}}$	Release: $\phi$ releases $\psi$ si $\psi$ se cumple hasta que la primera posición en la cual $\phi$ se cumple (o siempre si dicha posición no existe).
Operadores unarios
X $\phi$	$\circ \phi$	${\mathcal {N}}B(\phi _{i})=B(\phi _{i+1})$	Next: $\phi$ se cumple en el siguiente estado. (X es usado como sinónimo.)
F $\phi$	$\Diamond \phi$	${\mathcal {F}}B(\phi )=(true{\mathcal {U}}B)(\phi )$	Finally: $\phi$ eventualmente se cumple (en algún lugar del camino).
G $\phi$	$\Box \phi$	${\mathcal {G}}B(\phi )=\neg {\mathcal {F}}\neg B(\phi )$	Globally: $\phi$ se tiene que cumplir en todo el camino.
A $\phi$		${\begin{matrix}({\mathcal {A}}B)(\psi )=\\(\forall \phi :\phi _{0}=\psi \to B(\phi ))\end{matrix}}$	All: $\phi$ se tiene que cumplir en todos los caminos empezando en el estado actual.
E $\phi$		${\begin{matrix}({\mathcal {E}}B)(\psi )=\\(\exists \phi :\phi _{0}=\psi \land B(\phi ))\end{matrix}}$	Exists: existe al menos un camino que parte en el estado actual en el cual $\phi$ se cumple.

Símbolos alternativos:

• El operador R es algunas veces denotado por V
• El operador W es el operador weak until: $fWg$ es equivalente a $fUg\lor Gf$

Opearadores unarios son well-formed formulas cuandoquiera que B($\phi$) es bien formado. Los operadores binarios son fórmulas bien formadas cuandoquiera que B($\phi$) y C($\phi$) son bien formadas.

En algunas lógicas, algunos operadores no pueden se expresados. Por ejemplo, el operador N no puede ser expresado en la Temporal Logic of Actions.

Equivalencias

1. $fRg=\neg (\neg fU\neg g)$
2. $Gf=\neg F(\neg f)$
3. $Ff=VUf$ donde V = verdadero
4. $Af=\neg E(\neg f)$
5. $AXf=\neg EX(\neg f)$

Ejemplo

Estructura de Kripke de ejemplo

En la figura se muestra una estructura de Kripke de tres estados. Se puede describir de la siguiente manera:

1. En el estado rojo (e_R) se cumple p, y hay transiciones hacia el resto de los estados.
2. En el estado verde (e_V) q es verdadero, y las transciones van hacia el estado azul o el mismo estado.
3. En el estado azul (e_A) son verdaderas q y r, y tiene una única transición, hacia el estado verde.

Si se considera arbitrariamente al estado rojo como estado inicial, se cumple lo siguiente:

• EXr : pues tomando el camino e_Re_Ae_Ve_V... , en el segundo estado (e_A) r es verdadero, con lo que se encontró un camino que cumple Xr.
• AFq: pues para cualquier camino que se escoja inevitablemente habrá que entrar en los estados que hacen cumplir q, es decir, e_V o e_A.

Referencias

• Venema, Yde, 2001, "Temporal Logic," in Goble, Lou, ed., The Blackwell Guide to Philosophical Logic. Blackwell.

• E. A. Emerson and C. Lei, modalities for model checking: branching time logic strikes back, in Science of Computer Programming 8, p 275-306, 1987.

• E.A. Emerson, Temporal and modal logic, Handbook of Theoretical Computer Science, Chapter 16, the MIT Press, 1990

Véase también

• Lógica modal

Enlaces externos

• Anthony Galton, Temporal Logic in the Stanford Encyclopedia of Philosophy.