Lógica temporal

Lógica temporal: La lógica temporal es una extensión de la lógica modal, la cual es practicamente 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.

Contenido

1 Historia

2 Sistemas basados en lógica temporal

3 Operadores temporales

4 Equivalencias

5 Ejemplo

6 Referencias

7 Véase también

8 Enlaces externos

Historia

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

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,\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: $ψ$ se cumple en el estado actual o uno posterior, y $ϕ$ se tiene que cumplir hasta esa posición. A partir de esa posición $ϕ$ no es necesario que se siga cumpliendo.

$ϕ$ 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 $ψ$ si $ψ$ se cumple hasta que la primera posición en la cual $ϕ$ se cumple (o siempre si dicha posición no existe).

Operadores unarios

X $ϕ$ $\circ \phi$ $\mathcal{N}B(\phi_i)=B(\phi_{i+1})$ Next: $ϕ$ se cumple en el siguiente estado. (X es usado como sinónimo.)

F $ϕ$ $\Diamond \phi$ $\mathcal{F}B(\phi)=(true\mathcal{U}B)(\phi)$ Finally: $ϕ$ eventualmente se cumple (en algún lugar del camino).

G $ϕ$ $\Box \phi$ $\mathcal{G}B(\phi)=\neg\mathcal{F}\neg B(\phi)$ Globally: $ϕ$ se tiene que cumplir en todo el camino.

A $ϕ$ $\begin{matrix}(\mathcal{A}B)(\psi)= \\ (\forall \phi:\phi_0=\psi\to B(\phi))\end{matrix}$ All: $ϕ$ se tiene que cumplir en todos los caminos empezando en el estado actual.

E $ϕ$ $\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 $ϕ$ 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( $ϕ$ ) 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.

Equivalencias

$fRg = \neg (\neg f U \neg g )$

$Gf = \neg F(\neg f)$

$F f = V U f$ donde V = verdadero

$Af = \neg E(\neg f)$

$AXf = \neg EX(\neg f)$

Ejemplo

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

En el estado rojo (e_R) se cumple p, y hay transiciones hacia el resto de los estados.

En el estado verde (e_V) q es verdadero, y las transciones van hacia el estado azul o el mismo estado.

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.

Categoría:
Sistemas lógicos

Игры ⚽ Нужен реферат?

Mira otros diccionarios:

Lógica (desambiguación) — Saltar a navegación, búsqueda Lógica libre Lógica aristotélica Lógica binaria Lógica bivalente Lógica combinatoria Lógica computacional Lógica de control Lógica de descripción Lógica de primer orden Lógica de segundo orden Lógica deóntica Lógica… … Wikipedia Español
Lógica modal — Una lógica modal es un sistema formal que intenta capturar el comportamiento deductivo de algún grupo de operadores modales.[1] Los operadores modales son expresiones que califican la verdad de los juicios.[1] Por ejemplo, en la oración es… … Wikipedia Español
Lógica — La lógica es una ciencia formal y una rama de la filosofía que estudia los principios de la demostración e inferencia válida. La palabra deriva del griego antiguo λογική (logike), que significa «dotado de razón, intelectual, dialéctico,… … Wikipedia Español
Lógica proposicional — En lógica, la lógica proposicional es un sistema formal diseñado para analizar ciertos tipos de argumentos. En lógica proposicional, las fórmulas representan proposiciones y las conectivas lógicas son operaciones sobre dichas fórmulas, capaces de … Wikipedia Español
Lógica de bucle temporal — La Lógica de Bucle Temporal (aunque recurrencia temporal es mas correcto) es un sistema de computación que requiere una computadora capaz de enviar datos hacia atrás en el tiempo, se fundamenta en el Principio de autoconsistencia de Novikov para… … Wikipedia Español
Constante lógica — En lógica, una constante lógica es una expresión que cuya presencia y posición determina la forma lógica de una proposición,[1] y por extensión la validez o invalidez de los argumentos.[1] Dentro de un lenguaje formal con una semántica formal,… … Wikipedia Español
Historia de la lógica — La historia de la lógica documenta el desarrollo de la lógica en varias culturas y tradiciones a lo largo de la historia. Aunque muchas culturas han empleado intrincados sistemas de razonamiento, e, incluso, el pensamiento lógico estaba ya… … Wikipedia Español
Unidad aritmético-lógica — ► locución INFORMÁTICA Parte de un ordenador que ejecuta las operaciones aritméticas o lógicas sobre los datos. * * * Se denomina Unidad Aritmético Lógica (UAL) o ALU (Arithmetic and logical unit) a la unidad incluida en la CPU encargada de… … Enciclopedia Universal
Model checking — Con el nombre Model checking se conoce a un método automático de verificación de un sistema formal, en la mayoría de las ocasiones derivado del hardware o del software de un sistema informático. El sistema es descrito mediante un modelo, que debe … Wikipedia Español
Nuel Belnap — Nuel D. Belnap, Jr. (n. 1930) es un filósofo y lógico norteamericano que ha realizado importantes aportes en el campo de la filosofía de la lógica, lógica temporal, y teoría de la demostración estructural. Desee 1961 dicta cátedra en la… … Wikipedia Español

Los diccionarios y las enciclopedias sobre el Académico

Lógica temporal

Contenido

Historia

Sistemas basados en lógica temporal

Operadores temporales

Equivalencias

Ejemplo

Referencias

Véase también

Enlaces externos

Mira otros diccionarios:

Compartir el artículo y extractos

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: $ψ$ se cumple en el estado actual o uno posterior, y $ϕ$ se tiene que cumplir hasta esa posición. A partir de esa posición $ϕ$ no es necesario que se siga cumpliendo.
$ϕ$ 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 $ψ$ si $ψ$ se cumple hasta que la primera posición en la cual $ϕ$ se cumple (o siempre si dicha posición no existe).
Operadores unarios
X $ϕ$	$\circ \phi$	$\mathcal{N}B(\phi_i)=B(\phi_{i+1})$	Next: $ϕ$ se cumple en el siguiente estado. (X es usado como sinónimo.)
F $ϕ$	$\Diamond \phi$	$\mathcal{F}B(\phi)=(true\mathcal{U}B)(\phi)$	Finally: $ϕ$ eventualmente se cumple (en algún lugar del camino).
G $ϕ$	$\Box \phi$	$\mathcal{G}B(\phi)=\neg\mathcal{F}\neg B(\phi)$	Globally: $ϕ$ se tiene que cumplir en todo el camino.
A $ϕ$		$\begin{matrix}(\mathcal{A}B)(\psi)= \\ (\forall \phi:\phi_0=\psi\to B(\phi))\end{matrix}$	All: $ϕ$ se tiene que cumplir en todos los caminos empezando en el estado actual.
E $ϕ$		$\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 $ϕ$ se cumple.

Los diccionarios y las enciclopedias sobre el Académico

Wikipedia Español

Lógica temporal

Contenido

Historia

Sistemas basados en lógica temporal

Operadores temporales

Equivalencias

Ejemplo

Referencias

Véase también

Enlaces externos

Mira otros diccionarios:

Compartir el artículo y extractos

Link directo