Lógica temporal

La lógica temporal fue estudiada por Aristóteles, en algunos de sus escritos hay expresiones que guardan una cierta analogía con la lógica temporal de primer orden; es de esta manera como aparecen expresiones con cuantificadores existenciales y cuantificadores universales

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 lineal 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).

La lógica temporal tiene dos clases de operadores: operadores lógicos y operadores modales . Los operadores lógicos son usualmente operadores truth-functional (${\displaystyle \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
${\displaystyle \phi }$ U ${\displaystyle \psi }$	${\displaystyle \phi ~{\mathcal {U}}~\psi }$	${\displaystyle {\begin{matrix}(B{\mathcal {U}}C)(\phi )=\\(\exists i:C(\phi _{i})\land (\forall j<i:B(\phi _{j})))\end{matrix}}}$	Until: ${\displaystyle \psi }$ se cumple en el estado actual o uno posterior, y ${\displaystyle \phi }$ se tiene que cumplir hasta esa posición. A partir de esa posición ${\displaystyle \phi }$ no es necesario que se siga cumpliendo.
${\displaystyle \phi }$ R ${\displaystyle \psi }$	${\displaystyle \phi ~{\mathcal {R}}~\psi }$	${\displaystyle {\begin{matrix}(B{\mathcal {R}}C)(\phi )=\\(\forall i:C(\phi _{i})\lor (\exists j<i:B(\phi _{j})))\end{matrix}}}$	Release: ${\displaystyle \phi }$ releases ${\displaystyle \psi }$ si ${\displaystyle \psi }$ se cumple hasta que la primera posición en la cual ${\displaystyle \phi }$ se cumple (o siempre si dicha posición no existe).
Operadores unarios
X ${\displaystyle \phi }$	${\displaystyle \circ \phi }$	${\displaystyle {\mathcal {N}}B(\phi _{i})=B(\phi _{i+1})}$	Next: ${\displaystyle \phi }$ se cumple en el siguiente estado. (X es usado como sinónimo.)
F ${\displaystyle \phi }$	${\displaystyle \Diamond \phi }$	${\displaystyle {\mathcal {F}}B(\phi )=(true{\mathcal {U}}B)(\phi )}$	Finally: ${\displaystyle \phi }$ finalmente se cumple (en algún lugar del camino).
G ${\displaystyle \phi }$	${\displaystyle \Box \phi }$	${\displaystyle {\mathcal {G}}B(\phi )=\neg {\mathcal {F}}\neg B(\phi )}$	Globally: ${\displaystyle \phi }$ se tiene que cumplir en todo el camino.
A ${\displaystyle \phi }$		${\displaystyle {\begin{matrix}({\mathcal {A}}B)(\psi )=\\(\forall \phi$ :\phi _{0}=\psi \to B(\phi ))\end{matrix}}}	All: ${\displaystyle \phi }$ se tiene que cumplir en todos los caminos empezando en el estado actual.
E ${\displaystyle \phi }$		${\displaystyle {\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 ${\displaystyle \phi }$ se cumple.

Símbolos alternativos:

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

Operadores unarios son well-formed formulas cuandoquiera que B(${\displaystyle \phi }$) es bien formado. Los operadores binarios son fórmulas bien formadas cuandoquiera que B(${\displaystyle \phi }$) y C(${\displaystyle \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.

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

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 transiciones 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.

• 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

• Lógica modal
• Lógica temporal lineal

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