Lógica temporal

Lógica temporal ( lógica temporal ; lógica temporal en inglés ) - lógica , en cuyas declaraciones se tiene en cuenta el aspecto temporal. Se utiliza para describir secuencias de eventos y su relación a lo largo de una escala de tiempo.

En la antigüedad, el uso de la lógica en el aspecto temporal fue estudiado por los filósofos de la escuela de Megara , en particular Diodoro Cronos , y los estoicos . La lógica temporal simbólica moderna, conceptualizada y formulada por primera vez en la década de 1950 por Arthur Pryor [1] sobre la base de la lógica modal , fue más ampliamente utilizada y desarrollada en informática gracias al trabajo del ganador del Premio Turing Amir Pnueli .

Ejemplo

El significado de la declaración: "Tengo hambre" no cambia con el tiempo, pero su verdad puede cambiar: en un momento particular en el tiempo puede ser verdadero o falso, pero no ambos. A diferencia de las lógicas no temporales, donde el valor de las afirmaciones no cambia con el tiempo, en la lógica temporal, el valor depende de cuándo se prueba. La lógica temporal te permite expresar afirmaciones como "Siempre tengo hambre ", "A veces tengo hambre" o "Tengo hambre hasta que como".

Operadores temporales

Hay dos tipos de operadores en lógica temporal : lógicos y modales. Los operadores modales utilizados en la lógica de tiempo lineal y la lógica de árbol de cálculo se definen a continuación. $\neg ,\lor ,\land ,\rightarrow$

Designación de texto	Designación de símbolo	Definición	Descripción
Operadores binarios
$\fi$ tu $\psi$	$\phi ~\mathcal{U}~ \psi$	$\begin{matriz}(B\,\mathcal{U}\,C)(\phi)= \\ (\exists i:C(\phi_i)\land(\forall j<i:B(\phi_j)) )\end{matriz}$	Hasta (fuerte): debe ejecutarse en algún estado en el futuro (posiblemente el actual), la propiedad debe ejecutarse en todos los estados hasta (sin incluir) el designado. $\psi$ $\fi$
$\fi$ R $\psi$ $\fi$ V $\psi$	$\phi ~\mathcal{R}~ \psi$ $\phi ~\mathcal{V}~ \psi$	$\begin{matriz}(B\,\mathcal{R}\,C)(\phi)= \\ (\forall i:C(\phi_i)\lor(\exists j<i:B(\phi_j)) )\end{matriz}$	R release: Libera si es verdadero hasta la primera vez que lo es (o siempre si no lo es). De lo contrario, debe volverse verdadero al menos una vez antes de que lo sea la primera vez. $\fi$ $\psi$ $\psi$ $\fi$ $\fi$ $\psi$
Operadores unarios
norte $\fi$ X $\fi$	$\circ \phi$	$\mathcal{N}B(\phi_i)=B(\phi_{i+1})$	N e X t: debe ser verdadero en el estado inmediatamente posterior al dado. $\fi$
F $\fi$	$\Diamante \phi$	$\mathcal{F}B(\phi)=(verdadero\,\mathcal{U}\,B)(\phi)$	Futuro : debe hacerse realidad en al menos un estado en el futuro. $\fi$
GRAMO $\fi$	$\Box \phi$	$\mathcal{G}B(\phi)=\neg\mathcal{F}\neg B(\phi)$	Globalmente : debe ser cierto en todos los estados futuros. $\fi$
A $\fi$	$\mathcal{A} \phi$	$\begin{matriz}(\mathcal{A}B)(\psi)= \\ (\forall \phi:\phi_0=\psi\to B(\phi))\end{matriz}$	A ll: Debe ejecutarse en todas las ramas a partir de esta. $\fi$
mi $\fi$	$\mathcal{E}\fi$	$\begin{matriz}(\mathcal{E}B)(\psi)= \\ (\existe \phi:\phi_0=\psi\land B(\phi))\end{matriz}$	E xiste: Hay al menos una rama que se está ejecutando. $\fi$

Otros operadores modales

Declaración W que significa Débil hasta : equivalente a $f peso$ $fUg\lor Gf$

Identidades duales

Al igual que las reglas de Morgan, existen propiedades de dualidad para los operadores temporales:

$\phi ~\mathcal{U}~ \psi = \neg(\neg \phi ~\mathcal{V}~ \neg \psi)$
$\neg \Diamante \phi = \Caja \neg \phi$
$\neg \mathcal{A} \phi = \mathcal{E} \neg \phi$

Aplicaciones

Las lógicas temporales se utilizan a menudo para expresar requisitos formales de verificación . Por ejemplo, propiedades como "si se recibe una solicitud, definitivamente recibirá una respuesta" o "la función no se llama más de una vez por cálculo" es conveniente formularlas utilizando lógicas temporales. Se utilizan varios autómatas para probar tales propiedades, por ejemplo, los autómatas de Büchi para probar propiedades expresadas en lógica de tiempo lineal LTL .

Opciones

La principal variante universal de la lógica temporal es el μ-cálculo modal ( Scott - de Bakker , 1969); incluye la lógica de Henessy-Milner y CTL* como un subconjunto , y las principales variantes utilizadas en informática, la lógica de tiempo lineal ( LTL ) y la lógica de árbol de cálculo ( CTL ), son fragmentos de CTL * .

Además, existen otras variantes de la lógica temporal que no son reducibles al cálculo μ modal, por ejemplo, la lógica temporal de intervalos y la lógica temporal métrica

Algunas opciones prácticas utilizan combinaciones de lógica temporal con otras lógicas, en particular, como es la lógica de acción temporal (creada para el lenguaje de especificación TLA⁺ ), que conecta la lógica temporal y la lógica de acción .

Notas

↑ Ricardo Caferra. Lógica para Ciencias de la Computación e Inteligencia Artificial. - John Wiley & Sons, 2013. - 537 p. — ISBN 978-1-118-60426-7 .

Literatura

Clark E. M., Gramberg O., Peled D. Verificación de modelos de programas. Comprobación de modelos. Moscú: MTsNMO. 2002. ISBN 5-94057-054-2

diccionarios y enciclopedias	gran ruso Britannica (en línea)

Lógicas

Filosofía • Semántica • Sintaxis • Historia

Grupos lógicos

lógica clásica	lógica aristotélica Lógica proposicional Lógica de primer orden Lógica de segundo orden lógica de orden superior
lógica matemática	teoría de conjuntos Teoría del modelo teoría de la computabilidad Teoría de la prueba y matemáticas constructivas lógica lineal sistema formal conclusión natural cálculo de secuencias Álgebra de la lógica Lógica relevante lógica deóntica lógica intuicionista cálculo de Lambek
Lógica no clásica	intuicionismo lógica difusa Lógica subestructural lógica Descripción lógica Lógica multivaluada Síntesis lógica Lógica vinculante Lógica temporal Lógica modal ( Lógica híbrida ) lógica epistémica
lógica filosófica	Pensamiento crítico lógica informal razonamiento deductivo

Componentes

Lista de símbolos booleanos