Lógica temporal

De Wikipedia, la enciclopedia libre

El término lógica temporal, dentro de la lógica se usa 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.

[editar] 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.

[editar] 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).

[editar] 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,\or,\and,\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
$φ$ U $ψ$	$\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: $ψ$ holds at the current or a future position, and $φ$ has to hold until that position. At that position $φ$ does not have to hold any more.
$φ$ R $ψ$	$\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: $φ$ releases $ψ$ if $ψ$ is true until the first position in which $φ$ is true (or forever if such a position does not exist).
Operadores unarios
X $φ$	$\circ \phi$	$\mathcal{N}B(\phi_i)=B(\phi_{i+1})$	Next: $φ$ has to hold at the next state. (X is used synonymously.)
F $φ$	$\Diamond \phi$	$\mathcal{F}B(\phi)=(true\mathcal{U}B)(\phi)$	Finally: $φ$ eventually has to hold (somewhere on the subsequent path).
G $φ$	$\Box \phi$	$\mathcal{G}B(\phi)=\neg\mathcal{F}\neg B(\phi)$	Globally: $φ$ has to hold on the entire subsequent path.
A $φ$		$\begin{matrix}(\mathcal{A}B)(\psi)= \\ (\forall \phi:\phi_0=\psi\to B(\phi))\end{matrix}$	All: $φ$ has to hold on all paths starting from the current state.
E $φ$		$\begin{matrix}(\mathcal{E}B)(\psi)= \\ (\exists \phi:\phi_0=\psi\land B(\phi))\end{matrix}$	Exists: there exists at least one path starting from the current state where $φ$ holds.

Símbolos alternativos:

operador R es algunas veces denotado por V
El operador W' es el operador weak until: $f W g$ es equivalente a $f U g \or G f$

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