Lógica temporal

En lógica , la lógica temporal es cualquier sistema de reglas y simbolismo para representar y razonar proposiciones calificadas en términos de tiempo (por ejemplo, " siempre tengo hambre", " algún día tendré hambre" o "tendré hambre hasta que coma algo"). A veces también se usa para referirse a la lógica temporal , un sistema de lógica temporal basado en la lógica modal introducido por Arthur Prior a fines de la década de 1950, con importantes contribuciones de Hans Kamp . Ha sido desarrollado posteriormente por científicos informáticos , en particular Amir Pnueli , y lógicos .

La lógica temporal ha encontrado una aplicación importante en la verificación formal , donde se utiliza para indicar los requisitos de los sistemas de hardware o software. Por ejemplo, se puede decir que siempre que se realiza una solicitud, se concede el acceso a un recurso , pero nunca se concede a dos solicitantes simultáneamente. Tal afirmación se puede expresar convenientemente en una lógica temporal.

Consideremos la afirmación "tengo hambre". Aunque su significado es constante en el tiempo, el valor de verdad de la afirmación puede variar con el tiempo. A veces es verdadera y a veces falsa, pero nunca simultáneamente verdadera y falsa. En una lógica temporal, una afirmación puede tener un valor de verdad que varía con el tiempo, en contraste con una lógica atemporal, que se aplica solo a afirmaciones cuyos valores de verdad son constantes en el tiempo. Este tratamiento del valor de verdad a lo largo del tiempo diferencia la lógica temporal de la lógica verbal computacional.

La lógica temporal siempre tiene la capacidad de razonar sobre una línea de tiempo. Las llamadas lógicas de "tiempo lineal" se limitan a este tipo de razonamiento. Las lógicas de tiempo ramificado, sin embargo, pueden razonar sobre múltiples líneas de tiempo. Esto permite, en particular, el tratamiento de entornos que pueden actuar de manera impredecible. Para continuar con el ejemplo, en una lógica de tiempo ramificado podemos afirmar que "existe la posibilidad de que siga teniendo hambre para siempre" y que "existe la posibilidad de que, con el tiempo, ya no tenga hambre". Si no sabemos si alguna vez seré alimentado o no, ambas afirmaciones pueden ser verdaderas.

Aunque la lógica de Aristóteles se centra casi exclusivamente en la teoría del silogismo categórico , hay pasajes en su obra que ahora se consideran anticipaciones de la lógica temporal y pueden implicar una forma temprana, parcialmente desarrollada, de lógica bivalente modal temporal de primer orden . Aristóteles estaba particularmente preocupado por el problema de los contingentes futuros , donde no podía aceptar que el principio de bivalencia se aplique a afirmaciones sobre eventos futuros, es decir, que podamos decidir en el presente si una afirmación sobre un evento futuro es verdadera o falsa, como "mañana habrá una batalla naval". ^[1]

Hubo poco desarrollo durante milenios, señaló Charles Sanders Peirce en el siglo XIX: ^[2]

Los lógicos han considerado habitualmente que el tiempo es lo que se denomina materia «extralógica». Yo nunca he compartido esta opinión, pero he pensado que la lógica no había alcanzado todavía el estado de desarrollo en el que la introducción de modificaciones temporales de sus formas no provocaría una gran confusión; y todavía soy muy partidario de esa manera de pensar.

Sorprendentemente para Peirce , el primer sistema de lógica temporal fue construido, hasta donde sabemos, en la primera mitad del siglo XX. Aunque Arthur Prior es ampliamente conocido como el fundador de la lógica temporal, la primera formalización de dicha lógica fue proporcionada en 1947 por el lógico polaco Jerzy Łoś . ^[3] En su obra Podstawy Analizy Metodologicznej Kanonów Milla ( Los fundamentos de un análisis metodológico de los métodos de Mill ) presentó una formalización de los cánones de Mill . En el enfoque de Łoś , se hizo hincapié en el factor tiempo. Por lo tanto, para alcanzar su objetivo, tuvo que crear una lógica que pudiera proporcionar medios para la formalización de las funciones temporales. La lógica podría verse como un subproducto del objetivo principal de Łoś , ^[4] aunque fue la primera lógica posicional que, como marco, se utilizó más tarde para las invenciones de Łoś en lógica epistémica . La lógica en sí tiene una sintaxis muy diferente a la lógica temporal de Prior, que utiliza operadores modales. El lenguaje de la lógica de Łoś utiliza más bien un operador de realización, propio de la lógica posicional, que vincula la expresión con el contexto específico en el que se considera su valor de verdad. En la obra de Łoś , este contexto considerado era solo temporal, por lo que las expresiones estaban vinculadas a momentos o intervalos de tiempo específicos.

En los años siguientes, Arthur Prior comenzó a investigar la lógica temporal . ^[4] Se interesó por las implicaciones filosóficas del libre albedrío y la predestinación . Según su esposa, consideró por primera vez formalizar la lógica temporal en 1953. Los resultados de su investigación se presentaron por primera vez en la conferencia en Wellington en 1954. ^[4] El sistema que presentó Prior era similar sintácticamente a la lógica de Łoś , aunque no fue hasta 1955 que se refirió explícitamente al trabajo de Łoś , en la última sección del Apéndice 1 de la Lógica formal de Prior . ^[4]

Prior dio conferencias sobre el tema en la Universidad de Oxford en 1955-6, y en 1957 publicó un libro, Tiempo y modalidad , en el que introdujo una lógica modal proposicional con dos conectivos temporales ( operadores modales ), F y P, correspondientes a "en algún momento en el futuro" y "en algún momento en el pasado". En este trabajo temprano, Prior consideró que el tiempo es lineal. Sin embargo, en 1958, recibió una carta de Saul Kripke , quien señaló que esta suposición quizás no esté justificada. En un desarrollo que prefiguró uno similar en la ciencia de la computación, Prior tomó esto en consideración y desarrolló dos teorías del tiempo ramificado, que llamó "Ockhamista" y "Peirceana". ^{[2] [ aclaración necesaria ]} Entre 1958 y 1965 Prior también se carteó con Charles Leonard Hamblin , y una serie de desarrollos tempranos en el campo se pueden rastrear a esta correspondencia, por ejemplo, las implicaciones de Hamblin. Prior publicó su obra más madura sobre el tema, el libro Pasado, presente y futuro, en 1967. Murió dos años después. ^[5]

Junto con la lógica temporal, Prior construyó algunos sistemas de lógica posicional, que heredaron sus ideas principales de Łoś . ^[6] El trabajo en lógicas temporales posicionales fue continuado por Nicholas Rescher en los años 60 y 70. En obras como Nota sobre lógica cronológica (1966), Sobre la lógica de proposiciones cronológicas (1968) , Lógica topológica (1968) y Lógica temporal (1971) investigó las conexiones entre los sistemas de Łoś y Prior . Además, demostró que los operadores temporales de Prior podían definirse utilizando un operador de realización en lógicas posicionales específicas. ^[6] Rescher , en su trabajo, también creó sistemas más generales de lógicas posicionales. Aunque los primeros se construyeron para usos puramente temporales, propuso el término lógicas topológicas para lógicas que estaban destinadas a contener un operador de realización pero no tenían axiomas temporales específicos, como el axioma del reloj.

Los operadores temporales binarios Since y Until fueron introducidos por Hans Kamp en su tesis doctoral de 1968, ^[7] que también contiene un resultado importante que relaciona la lógica temporal con la lógica de primer orden , un resultado ahora conocido como el teorema de Kamp. ^{[8] [2] [9]}

Dos de los primeros contendientes en las verificaciones formales fueron la lógica temporal lineal , una lógica de tiempo lineal de Amir Pnueli , y la lógica de árbol de cálculo (CTL), una lógica de tiempo de ramificación de Mordechai Ben-Ari , Zohar Manna y Amir Pnueli. Un formalismo casi equivalente a CTL fue sugerido por la misma época por EM Clarke y EA Emerson . El hecho de que la segunda lógica pueda ser decidida de manera más eficiente que la primera no se refleja en las lógicas de tiempo de ramificación y lineal en general, como a veces se ha argumentado. Más bien, Emerson y Lei muestran que cualquier lógica de tiempo lineal puede extenderse a una lógica de tiempo de ramificación que puede ser decidida con la misma complejidad.

La lógica de Łoś fue publicada como su tesis de maestría de 1947 Podstawy Analizy Metodologicznej Kanonów Milla ( Los fundamentos de un análisis metodológico de los métodos de Mill ). ^[10] Sus conceptos filosóficos y formales podrían verse como continuaciones de los de la Escuela de Lógica de Lviv-Varsovia , ya que su supervisor fue Jerzy Słupecki , discípulo de Jan Łukasiewicz . El artículo no fue traducido al inglés hasta 1977, aunque Henryk Hiż presentó en 1951 una revisión breve, pero informativa, en el Journal of Symbolic Logic . Esta revisión contenía conceptos centrales del trabajo de Łoś y fue suficiente para popularizar sus resultados entre la comunidad lógica. El objetivo principal de este trabajo fue presentar los cánones de Mill en el marco de la lógica formal. Para lograr este objetivo, el autor investigó la importancia de las funciones temporales en la estructura del concepto de Mill. Con esto en mente, proporcionó su sistema axiomático de lógica que serviría como marco para los cánones de Mill junto con sus aspectos temporales.

El lenguaje de la lógica publicada por primera vez en Podstawy Analizy Metodologicznej Kanonów Milla ( Los fundamentos de un análisis metodológico de los métodos de Mill ) consistía en: ^[3]

• operadores lógicos de primer orden '¬', '∧', '∨', '→', '≡', '∀' y '∃'
• operador de realización U
• símbolo funcional δ
• variables proposicionales p ₁ ,p ₂ ,p ₃ ,...
• variables que denotan momentos de tiempo t ₁ ,t ₂ ,t ₃ ,...
• variables que denotan intervalos de tiempo n ₁ ,n ₂ ,n ₃ ,...

El conjunto de términos (denotado por S) se construye de la siguiente manera:

• Las variables que denotan momentos o intervalos de tiempo son términos
• Si y es una variable de intervalo de tiempo, entonces${\displaystyle \tau \en S}$${\displaystyle \épsilon}$${\displaystyle \delta (\tau ,\epsilon )\in S}$

El conjunto de fórmulas (denotado por For) se construye de la siguiente manera: ^[10]

• Todas las fórmulas lógicas de primer orden son válidas.
• Si y es una variable proposicional, entonces${\displaystyle \tau \en S}$${\estilo de visualización \phi}$${\displaystyle U_{\tau }(\phi )\in Para}$
• Si , entonces${\displaystyle \phi \in Para}$${\displaystyle \neg \phi \in Para}$
• Si y , entonces${\displaystyle \phi ,\psi \in Para}$${\displaystyle \circ \in \{\cuña,\vee,\flecha derecha,\equiv \}}$${\displaystyle \phi \circ \psi \in Para}$
• si y y υ es una variable proposicional, de momento o de intervalo, entonces${\displaystyle \phi \in Para}$${\displaystyle Q\en \{\paratodos,\existe \}}$${\displaystyle Q_{\upsilon }\phi \in Para}$

1. ${\displaystyle U_{t_{1}}\neg p_{1}\equiv \neg U_{t_{1}}p_{1}}$
2. ${\displaystyle U_{t_{1}}(p_{1}\rightarrow p_{2})\rightarrow (U_{t_{1}}p_{1}\rightarrow U_{t_{1}}p_{2})}$
3. ${\displaystyle U_{t_{1}}((p_{1}\rightarrow p_{2})\rightarrow ((p_{2}\rightarrow p_{3})\rightarrow (p_{1}\rightarrow p_{3})))}$
4. ${\displaystyle U_{t_{1}}(p_{1}\rightarrow (\neg p_{1}\rightarrow p_{2}))}$
5. ${\displaystyle U_{t_{1}}((\neg p_{1}\rightarrow p_{1})\rightarrow p_{1})}$
6. ${\displaystyle \forall _{t_{1}}U_{t_{1}}p_{1}\rightarrow p_{1}}$
7. ${\displaystyle \forall _{t_{1}}\forall _{n_{1}}\exists _{t_{2}}\forall _{p_{1}}(U_{\delta (t_{1},n_{1})}p_{1}\equiv U_{t_{2}}p_{1})}$
8. ${\displaystyle \forall _{t_{1}}\forall _{n_{1}}\exists _{t_{2}}\forall _{p_{1}}(U_{\delta (t_{2},n_{1})}p_{1}\equiv U_{t_{1}}p_{1})}$
9. ${\displaystyle \forall _{t_{1}}\exists _{p_{1}}\forall _{t_{2}}(U_{t_{2}}p_{1}\equiv \forall _{p_{2}}(U_{t_{1}}p_{2}\equiv U_{t_{2}}p_{2}))}$

La lógica del tiempo oracional introducida en Tiempo y Modalidad tiene cuatro operadores modales (no funcionales a la verdad ) (además de todos los operadores funcionales a la verdad habituales en la lógica proposicional de primer orden ). ^[11]

• P : "Fue el caso que..." (P significa "pasado")
• F : "Será el caso que..." (F significa "futuro")
• G : "Siempre será el caso que..."
• H : "Siempre fue el caso que..."

Estos se pueden combinar si dejamos que π sea un camino infinito: ^[12]

• ${\displaystyle \pi \vDash FG\phi }$:"En un punto determinado, es cierto en todos los estados futuros del camino"${\displaystyle \phi }$
• ${\displaystyle \pi \vDash GF\phi }$: " es cierto en infinitos estados del camino"${\displaystyle \phi }$

A partir de P y F se pueden definir G y H , y viceversa:

${\displaystyle {\begin{aligned}F&\equiv \lnot G\lnot \\P&\equiv \lnot H\lnot \end{aligned}}}$

Una sintaxis mínima para TL se especifica con la siguiente gramática BNF :

${\displaystyle \phi ::=a\;|\;\bot \;|\;\lnot \phi \;|\;\phi \lor \phi \;|\;G\phi \;|\;H\phi }$

donde a es alguna fórmula atómica . ^[13]

Los modelos de Kripke se utilizan para evaluar la verdad de las oraciones en TL. Un par ( T , <) de un conjunto T y una relación binaria < en T (llamada "precedencia") se llama marco . Un modelo está dado por el triple ( T , <, V ) de un marco y una función V llamada valoración que asigna a cada par ( a , u ) de una fórmula atómica y un valor temporal algún valor de verdad. La noción " ϕ es verdadero en un modelo U = ( T , <, V ) en el tiempo u " se abrevia U ⊨ ϕ [ u ]. Con esta notación, ^[14]

Dada una clase F de marcos, una oración ϕ de TL es

• válido con respecto a F si para cada modelo U =( T ,<, V ) con ( T ,<) en F y para cada u en T , U ⊨ ϕ [ u ]
• satisfacible con respecto a F si hay un modelo U =( T ,<, V ) con ( T ,<) en F tal que para algún u en T , U ⊨ ϕ [ u ]
• una consecuencia de una oración ψ con respecto a F si para cada modelo U =( T ,<, V ) con ( T ,<) en F y para cada u en T , si U ⊨ ψ [ u ], entonces U ⊨ ϕ [ u ]

Muchas oraciones son válidas únicamente para una clase limitada de marcos. Es común restringir la clase de marcos a aquellos con una relación < que sea transitiva , antisimétrica , reflexiva , tricotómica , irreflexiva , total , densa o alguna combinación de estas.

Burgess describe una lógica que no hace suposiciones sobre la relación <, pero permite deducciones significativas, basadas en el siguiente esquema axiomático: ^[15]

1. A donde A es una tautología de lógica de primer orden
2. G( A → B )→( GA → GB )
3. H( A → B )→( HA → HB )
4. A →GP A
5. A → HFA

con las siguientes reglas de deducción:

1. dado A → B y A , deducir B ( modus ponens )
2. Dada una tautología A , inferir G A
3. Dada una tautología A , inferir H A

Se pueden derivar las siguientes reglas:

1. Regla de Becker : dado A → B , deducir T A →T B donde T es un tiempo , cualquier secuencia formada por G, H, F y P.
2. Reflejo : dado un teorema A , deducir su enunciado reflejado A ^§ , que se obtiene reemplazando G por H (y por tanto F por P) y viceversa.
3. Dualidad : dado un teorema A , deducir su enunciado dual A *, que se obtiene intercambiando ∧ con ∨, G con F y H con P.

Burgess ofrece una traducción Meredith de enunciados en lógica de primer orden a enunciados en lógica de primer orden con una variable libre x ₀ (que representa el momento presente). Esta traducción M se define recursivamente de la siguiente manera: ^[16]

${\displaystyle {\begin{aligned}&M(a)&&=a^{*}x_{0}\\&M(\lnot \phi )&&=\lnot M(\phi )\\&M(\phi \land \psi )&&=M(\phi )\land M(\psi )\\&M({\mathsf {G}}\phi )&&=\forall x_{1}(x_{0}<x_{1}\rightarrow M(A^{+}))\\&M({\mathsf {H}}\phi )&&=\forall x_{1}(x_{1}<x_{0}\rightarrow M(A^{+}))\end{aligned}}}$

donde es la oración A con todos los índices variables incrementados en 1 y es un predicado de un lugar definido por .${\displaystyle A^{+}}$${\displaystyle a^{*}}$${\displaystyle x\mapsto V(a,x)}$

La lógica temporal tiene dos tipos de operadores: operadores lógicos y operadores modales. ^[17] Los operadores lógicos son operadores veritativo-funcionales habituales ( ). Los operadores modales utilizados en la lógica temporal lineal y la lógica de árboles computacionales se definen de la siguiente manera.${\displaystyle \neg ,\lor ,\land ,\rightarrow }$

Textual	Simbólico	Definición	Explicación	Diagrama
Operadores binarios
φUψ ​ ​	${\displaystyle \phi ~{\mathcal {U}}~\psi }$	${\displaystyle (B\,{\mathcal {U}}\,C)(\phi )=\ (\exists i:C(\phi _{i})\land (\forall j<i:B(\phi _{j})))}$	Hasta que: ψ se mantiene en la posición actual o en una posición futura, y φ debe mantenerse hasta esa posición. En esa posición, φ ya no tiene por qué mantenerse.
φ R ψ	${\displaystyle \phi ~{\mathcal {R}}~\psi }$	${\displaystyle (B\,{\mathcal {R}}\,C)(\phi )=\ (\forall i:C(\phi _{i})\lor (\exists j<i:B(\phi _{j})))}$	Liberación : φ libera ψ si ψ es verdadero hasta la primera posición inclusive en la que φ es verdadero (o para siempre si dicha posición no existe).
Operadores unarios
norte ​	${\displaystyle \bigcirc \phi }$	${\displaystyle {\mathcal {N}}B(\phi _{i})=B(\phi _{i+1})}$	Siguiente : φ debe mantenerse en el siguiente estado. ( X se utiliza como sinónimo).
F φ	${\displaystyle \Diamond \phi }$	${\displaystyle {\mathcal {F}}B(\phi )=(true\,{\mathcal {U}}\,B)(\phi )}$	Futuro : φ eventualmente tiene que mantenerse (en algún lugar del camino subsiguiente).
G φ	${\displaystyle \Box \phi }$	${\displaystyle {\mathcal {G}}B(\phi )=\neg {\mathcal {F}}\neg B(\phi )}$	A nivel global: φ debe mantenerse en todo el camino subsiguiente.
Un φ	${\displaystyle \forall \phi }$	${\displaystyle ({\mathcal {A}}B)(\psi )=\ (\forall \phi :\phi _{0}=\psi \to B(\phi ))}$	A l l: φ debe cumplirse en todas las rutas a partir del estado actual.
mi φ	${\displaystyle \exists \phi }$	${\displaystyle ({\mathcal {E}}B)(\psi )=\ (\exists \phi :\phi _{0}=\psi \land B(\phi ))}$	E xiste: existe al menos un camino que parte del estado actual donde se cumple φ .

Símbolos alternativos:

• El operador R a veces se denota por V
• El operador W es el operador débil hasta : es equivalente a${\displaystyle f\mathbf {W} g}$${\displaystyle f\mathbf {U} g\lor \mathbf {G} f}$

Los operadores unarios son fórmulas bien formadas siempre que B( φ ) esté bien formada. Los operadores binarios son fórmulas bien formadas siempre que B( φ ) y C( φ ) estén bien formadas.

En algunas lógicas, algunos operadores no se pueden expresar. Por ejemplo, el operador N no se puede expresar en la lógica temporal de acciones .

Las lógicas temporales incluyen:

• Algunos sistemas de lógica posicional
• Lógica temporal lineal (LTL) lógica temporal sin líneas de tiempo ramificadas
• Lógica de árbol de cálculo (CTL) lógica temporal con líneas de tiempo ramificadas
• Lógica temporal de intervalos (ITL)
• Lógica temporal de acciones (TLA)
• Lógica temporal de señales (STL) ^[18]
• Lógica temporal de marca de tiempo (TTL) ^[19]
• Lenguaje de especificación de propiedades (PSL)
• CTL* , que generaliza LTL y CTL
• Lógica de Hennessy-Milner (HML)
• Cálculo μ modal , que incluye como subconjunto HML y CTL*
• Lógica temporal métrica (MTL) ^[20]
• Lógica temporal de intervalo métrico (MITL) ^[18]
• Lógica temporal proposicional cronometrada (TPTL)
• Lógica temporal lineal truncada (TLTL) ^[21]
• Lógica hipertemporal (HyperLTL) ^[22]

Una variación, estrechamente relacionada con las lógicas temporales, cronológicas o de tiempo, son las lógicas modales basadas en la “topología”, el “lugar” o la “posición espacial”. ^{[23] [24]}

• Formalismo HPO
• Estructura de Kripke
• Teoría de autómatas
• Gramática de Chomsky
• Sistema de transición de estados
• Cálculo de duración (DC)
• Lógica híbrida
• Lógica temporal en la verificación de estados finitos
• Lenguaje de coordinación reo
• Lógica modal
• Materiales de investigación: Archivo de la Sociedad Max Planck

• Mordechai Ben-Ari, Zohar Manna, Amir Pnueli: La lógica temporal del tiempo ramificado . POPL 1981: 164–176
• Amir Pnueli: La lógica temporal de los programas FOCS 1977: 46–57
• Venema, Yde, 2001, "Lógica temporal", en Goble, Lou, ed., La guía Blackwell para la lógica filosófica . Blackwell.
• EA Emerson y Chin-Laung Lei, "Modalidades para la verificación de modelos: la lógica del tiempo de ramificación contraataca", en Science of Computer Programming 8, págs. 275-306, 1987.
• EA Emerson, "Lógica temporal y modal", Handbook of Theoretical Computer Science , Capítulo 16, MIT Press, 1990
• Introducción práctica al lenguaje de señas, Cindy Eisner, Dana Fisman
• Vardi, Moshe Y. (2008). "De la Iglesia y antes de la PSL ". En Orna Grumberg; Helmut Veith (eds.). 25 años de verificación de modelos: historia, logros, perspectivas . Springer. ISBN 978-3-540-69849-4.Preimpresión. Perspectiva histórica sobre cómo ideas aparentemente dispares se unieron en la ciencia informática y la ingeniería. (La mención de Church en el título de este artículo es una referencia a un artículo poco conocido de 1957, en el que Church propuso una forma de realizar la verificación de hardware).

• Peter Øhrstrøm; Per FV Hasle (1995). Lógica temporal: de las ideas antiguas a la inteligencia artificial . Springer. ISBN 978-0-7923-3586-3.

Wikimedia Commons tiene medios relacionados con Lógica temporal .

• Enciclopedia de Filosofía de Stanford : "Lógica temporal", por Anthony Galton.
• Lógica temporal de Yde Venema, descripción formal de la sintaxis y la semántica, cuestiones de axiomatización. También se tratan los operadores temporales diádicos de Kamp (desde, hasta)
• Notas sobre juegos en lógica temporal de Ian Hodkinson, incluida una descripción formal de la lógica temporal de primer orden
• CADP: proporciona verificadores de modelos genéricos para diversas lógicas temporales
• PAT es un potente verificador de modelos gratuito, verificador LTL, simulador y verificador de refinamiento para CSP y sus extensiones (con variables compartidas, matrices, amplio rango de equidad).