Lógica temporal

De Wikipedia, la enciclopedia libre
Saltar a: navegación, búsqueda

La lógica temporal es una extensión de la lógica modal, la cual es prácticamente usada en sistema de reglas, donde esta presente el tiempo. Existe una cierta relación con otras variedades de lógica, por ejemplo, la lógica modal. Su estudio tiene importancia en la parte de la informática hasta nuestros días.

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

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

Sistemas basados en lógica temporal[editar]

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

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
\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: f W g es equivalente a f U g \or G f

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

  1. fRg = \neg (\neg f U \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[editar]

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 (eR) se cumple p, y hay transiciones hacia el resto de los estados.
  2. En el estado verde (eV) q es verdadero, y las transciones van hacia el estado azul o el mismo estado.
  3. En el estado azul (eA) 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 eReAeVeV... , en el segundo estado (eA) 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, eV o eA.

Referencias[editar]

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

Enlaces externos[editar]