Lógica temporal

En lógica , la lógica temporal es cualquier sistema de reglas y simbolismo para representar y razonar sobre proposiciones calificadas en términos de tiempo (por ejemplo, " siempre tengo hambre", " eventualmente tendré hambre" o "tendré hambre"). hasta que coma algo"). A veces también se utiliza para referirse a la lógica tensa , un sistema de lógica temporal basado en la lógica modal introducido por Arthur Prior a finales de la década de 1950, con importantes contribuciones de Hans Kamp . Ha sido desarrollado aún más 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 podría decir que cada vez que se realiza una solicitud, finalmente se concede acceso a un recurso, pero nunca se concede a dos solicitantes simultáneamente. Semejante afirmación puede expresarse convenientemente en una lógica temporal.

Motivación

Considere 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 verdad y otras falso, pero nunca simultáneamente verdadero y falso. En una lógica temporal, un enunciado puede tener un valor de verdad que varía en el tiempo, en contraste con una lógica atemporal, que se aplica sólo a enunciados 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. La llamada lógica del "tiempo lineal" se limita a este tipo de razonamiento. Sin embargo, las lógicas de tiempo de ramificación pueden razonar sobre múltiples líneas de tiempo. Esto permite, en particular, tratar entornos que pueden actuar de forma 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 eventualmente ya no tenga hambre". Si no sabemos si alguna vez seré alimentado o no, ambas afirmaciones pueden ser ciertas.

Historia

Aunque la lógica de Aristóteles se ocupa casi por completo de 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 aplicara a enunciados sobre eventos futuros, es decir, que podamos decidir en el presente si un enunciado sobre un evento futuro es verdadero o falso, como por ejemplo "hay "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 suelen considerar que el tiempo es lo que se llama materia "extralógica". Nunca he compartido esta opinión. Pero he pensado que la lógica aún no había alcanzado el estado de desarrollo en el que la introducción de modificaciones temporales de sus formas no resultaría en gran confusión; y todavía soy muy de esa manera de pensar.

Sorprendentemente para Peirce , el primer sistema de lógica temporal se construyó, hasta donde sabemos, en la primera mitad del siglo XX. Aunque Arthur Prior es ampliamente conocido como 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. Así, 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 tensa de Prior, que utiliza operadores modales. El lenguaje de la lógica de Łoś utiliza más bien un operador de realización, específico 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 sólo temporal, por lo que las expresiones estaban ligadas a momentos o intervalos de tiempo específicos.

En los años siguientes se inició la investigación de la lógica temporal por parte de Arthur Prior . ^[4] Le preocupaban 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 de Wellington en 1954. ^[4] El sistema presentado por Prior era sintácticamente similar a la lógica de Łoś , aunque no fue hasta 1955 que lo hizo. se refiere 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, Time and Modality , en el que introdujo una lógica modal proposicional con dos conectivos temporales ( operadores modales ), F y P, correspondientes a "en algún momento del futuro" y "en algún momento del pasado". En estos primeros trabajos, Prior consideraba que el tiempo era lineal. Sin embargo, en 1958 recibió una carta de Saul Kripke , quien señalaba que esta suposición quizás no esté justificada. En un desarrollo que presagiaba uno similar en informática, Prior tomó esto en cuenta y desarrolló dos teorías del tiempo de ramificación, a las que llamó "ockhamista" y "peirceana". ^{[2] [ se necesita aclaración ]} Entre 1958 y 1965, Prior también mantuvo correspondencia con Charles Leonard Hamblin , y varios de los primeros desarrollos en el campo se pueden atribuir a esta correspondencia, por ejemplo, las implicaciones de Hamblin. Prior publicó su trabajo más maduro sobre el tema, el libro Pasado, presente y futuro en 1967. Murió dos años después. ^[5]

Junto con la lógica tensa, Prior construyó algunos sistemas de lógica posicional, que heredaron sus ideas principales de Łoś . ^[6] Nicholas Rescher continuó el trabajo en lógica temporal posicional en los años 60 y 70. En obras como Nota sobre lógica cronológica (1966), Sobre la lógica de las 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 de tiempo de Prior podían definirse utilizando un operador de realización en lógicas posicionales específicas. ^[6] Rescher , en su obra, también creó sistemas más generales de lógica posicional. Aunque los primeros se construyeron para usos puramente temporales, propuso el término lógica topológica para las lógicas que debían contener un operador de realización pero que no tenían axiomas temporales específicos, como el axioma del reloj.

Los operadores temporales binarios Desde y Hasta fueron introducidos por Hans Kamp en su doctorado de 1968. tesis, ^[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 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 Mordejai Ben-Ari , Zohar Manna y Amir Pnueli. Casi al mismo tiempo, EM Clarke y EA Emerson sugirieron un formalismo casi equivalente al CTL . El hecho de que la segunda lógica pueda decidirse de manera más eficiente que la primera no refleja las lógicas de tiempo lineal y de ramificación 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 decidirse con la misma complejidad.

La lógica posicional de Łoś

La lógica de Łoś se publicó 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 se tradujo al inglés hasta 1977, aunque Henryk Hiż presentó en 1951 una reseña 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. Teniendo eso en cuenta, proporcionó su sistema axiomático de lógica que encajaría como marco para los cánones de Mill junto con sus aspectos temporales.

Sintaxis

El lenguaje de la lógica publicado 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 \in S}$ ${\displaystyle \epsilon }$ ${\displaystyle \delta (\tau ,\epsilon )\in S}$

El conjunto de fórmulas (indicado 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 \in S}$ ${\displaystyle \phi }$ ${\displaystyle U_{\tau }(\phi )\in For}$
• si entonces ${\displaystyle \phi \in For}$ ${\displaystyle \neg \phi \in For}$
• si y , entonces ${\displaystyle \phi ,\psi \in For}$ ${\displaystyle \circ \in \{\wedge ,\vee ,\rightarrow ,\equiv \}}$ ${\displaystyle \phi \circ \psi \in For}$
• si y y υ es una variable proposicional, de momento o de intervalo, entonces ${\displaystyle \phi \in For}$ ${\displaystyle Q\in \{\forall ,\exists \}}$ ${\displaystyle Q_{\upsilon }\phi \in For}$

Sistema axiomático original

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}))}$

Lógica del tiempo de Prior (TL)

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

• P : "Fue el caso que..." (P significa "pasado")
• F : "Se dará el caso de que..." (F significa "futuro")
• G : "Siempre será el caso que..."
• H : "Siempre fue así que..."

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

• ${\displaystyle \pi \vDash FG\phi }$: "En cierto punto, 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 puede definir G y H , y viceversa:

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

Sintaxis y semántica

Se especifica una sintaxis mínima para TL 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 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 la tripleta ( 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 verdadera en un modelo U = ( T , <, V ) en el momento 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 todo modelo U =( T ,<, V ) con ( T ,<) en F y para cada u en T , U ⊨ ϕ [ u ]
• satisfactible con respecto a F si existe un modelo U =( T ,<, V ) con ( T ,<) en F tal que para alguna 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 ⊨ ϕ [ tú ]

Muchas oraciones sólo son válidas 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.

Una lógica axiomática mínima

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

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

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 , deduzca T A →T B donde T es un tiempo , cualquier secuencia formada por G, H, F y P.
2. Reflejo : dado un teorema A , deduzca su enunciado espejo A ^§ , que se obtiene reemplazando G por H (y por tanto F por P) y viceversa.
3. Dualidad : dado un teorema A , deduce su enunciado dual A *, que se obtiene intercambiando ∧ con ∨, G con F y H con P.

Traducción a lógica de predicados

Burgess ofrece una traducción de Meredith de declaraciones en TL a declaraciones 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 con todos los índices variables incrementados en 1 y es un predicado de un solo lugar definido por . ${\displaystyle A^{+}}$ ${\displaystyle A}$ ${\displaystyle a^{*}}$ ${\displaystyle x\mapsto V(a,x)}$

Operadores temporales

La lógica temporal tiene dos tipos de operadores: operadores lógicos y operadores modales. ^[17] Los operadores lógicos son operadores funcionales de verdad habituales ( ). Los operadores modales utilizados en la lógica temporal lineal y la lógica de árbol de cálculo se definen a continuación. ${\displaystyle \neg ,\lor ,\land ,\rightarrow }$

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 formados.

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 .

Lógicas temporales

Las lógicas temporales incluyen:

• Algunos sistemas de lógica posicional
• Lógica temporal lineal (LTL) sin líneas de tiempo ramificadas
• Lógica temporal de lógica de árbol de cálculo (CTL) con líneas de tiempo ramificadas
• Lógica temporal de intervalo (ITL)
• Lógica temporal de acciones (TLA)
• Lógica temporal de señal (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 la lógica temporal, cronológica o tensa, son las lógicas modales basadas en "topología", "lugar" o "posición espacial". ^{[23] [24]}

Ver también

• Portal de filosofía

• formalismo HPO
• estructura kripke
• Teoría de los autómatas
• gramática chomsky
• Sistema de transición estatal
• Cálculo de duración (DC)
• Lógica híbrida
• Lógica temporal en verificación de estados finitos
• Lenguaje de coordinación reo
• Lógica modal
• Materiales de investigación: Archivo de la Sociedad Max Planck

Notas

1. Vardi 2008, pag. 153
2. Vardi 2008, pag. 154
3. Łoś, Jerzy (1920-1998); Loś, Jerzy (1920-1998) (1947). "Podstawy análisis metodológicoznej kanonów Milla". Zasoby Biblioteki Głównej Umcs . nakł. Uniwersytetu Marii Curie-Skłodowskiej.{{cite journal}}: CS1 maint: numeric names: authors list (link)
4. Øhrstrøm, Peter (2019). "La importancia de las contribuciones de ANPrior y Jerzy Łoś en la historia temprana de la lógica temporal moderna". Lógica y filosofía del tiempo: más temas de Prior, volumen 2 . Lógica y Filosofía del Tiempo. ISBN 9788772102658.
5. Peter Øhrstrøm; Según FV Hasle (1995). Lógica temporal: de las ideas antiguas a la inteligencia artificial . Saltador. ISBN 978-0-7923-3586-3.págs. 176-178, 210
6. Rescher, Nicolás; Garson, James (enero de 1969). "Lógica topológica". La revista de lógica simbólica . 33 (4): 537–548. doi :10.2307/2271360. ISSN  0022-4812. JSTOR  2271360. S2CID  2110963.
7. "Lógica temporal (Enciclopedia de Filosofía de Stanford)". Platón.stanford.edu . Consultado el 30 de julio de 2014 .
8. Walter Carnielli; Claudio Pizzi (2008). Modalidades y Multimodalidades. Saltador. pag. 181.ISBN​ 978-1-4020-8589-5.
9. Sergio Tessaris; Enrico Franconi; Thomas Eiter (2009). Web de razonamiento. Tecnologías semánticas para sistemas de información: Quinta Escuela Internacional de Verano 2009, Brixen-Bressanone, Italia, 30 de agosto - 4 de septiembre de 2009, Conferencias tutoriales. Saltador. pag. 112.ISBN​ 978-3-642-03753-5.
10. Tkaczyk, Marcin; Jarmużek, Tomasz (2019). "Cálculo posicional de Jerzy Łoś y el origen de la lógica temporal". Lógica y Filosofía Lógica . 28 (2): 259–276. doi : 10.12775/LLP.2018.013 . ISSN  2300-9802.
11. Antes, Arthur Norman (2003). Tiempo y modalidad: las conferencias de John Locke de 1955 a 1956, impartidas en la Universidad de Oxford . Oxford: The Clarendon Press. ISBN 9780198241584. OCLC  905630146.
12. Lawford, M. (2004). "Una introducción a la lógica temporal" (PDF) . Departamento de Ciencias de la Computación Universidad McMaster .
13. Goranko, Valentín; Galton, Antonio (2015). Zalta, Edward N. (ed.). La Enciclopedia de Filosofía de Stanford (edición de invierno de 2015). Laboratorio de Investigación en Metafísica, Universidad de Stanford.
14. Muller, Thomas (2011). «Lógica tensa o temporal» (PDF) . En Horsten, León (ed.). El compañero continuo de la lógica filosófica . A&C Negro. pag. 329.
15. Burgess, John P. (2009). Lógica filosófica . Princeton, Nueva Jersey: Princeton University Press. pag. 21.ISBN​ 9781400830497. OCLC  777375659.
16. Burgess, John P. (2009). Lógica filosófica . Princeton, Nueva Jersey: Princeton University Press. pag. 17.ISBN​ 9781400830497. OCLC  777375659.
17. "Lógica temporal". Enciclopedia de Filosofía de Stanford . 7 de febrero de 2020 . Consultado el 19 de abril de 2022 .
18. Maler, O.; Nickovic, D. (2004). "Seguimiento de las propiedades temporales de señales continuas". doi :10.1007/978-3-540-30206-3_12.
19. Mehrabiano, Mohammadreza; Khayatian, Mohammad; Shrivastava, Aviral; Eidson, John C.; Derler, Patricia; Andrade, Hugo A.; Li-Baboud, Ya-Shian; Griffin, Eduardo; Weiss, Marc; Stanton, Kevin (2017). "Lógica temporal de marca de tiempo (TTL) para probar la sincronización de sistemas ciberfísicos". Transacciones ACM en sistemas informáticos integrados . 16 (5s): 1–20. doi : 10.1145/3126510 . S2CID  3570088.
20. Koymans, R. (1990). "Especificar propiedades en tiempo real con lógica temporal métrica", Real-Time Systems 2 (4): 255–299. doi :10.1007/BF01995674.
21. Li, Xiao, Cristian-Ioan Vasile y Calin Belta. "Aprendizaje por refuerzo con recompensas de lógica temporal". doi :10.1109/IROS.2017.8206234
22. Clarkson, Michael R.; Finkbeiner, Bernd; Koleini, Masoud; Micinski, Kristopher K.; Rabe, Markus N.; Sánchez, César (2014). "Lógicas temporales para hiperpropiedades". Principios de Seguridad y Confianza . Apuntes de conferencias sobre informática. vol. 8414, págs. 265–284. doi :10.1007/978-3-642-54792-8_15. ISBN 978-3-642-54791-1. S2CID  8938993.
23. Rescher, Nicolás (1968). "Lógica topológica". Temas de lógica filosófica . págs. 229–249. doi :10.1007/978-94-017-3546-9_13. ISBN 978-90-481-8331-9.
24. von Wright, Georg Henrik (1979). "Una lógica modal de lugar". La filosofía de Nicholas Rescher . págs. 65–73. doi :10.1007/978-94-009-9407-2_9. ISBN 978-94-009-9409-6.

Referencias

• Mordejai Ben-Ari, Zohar Manna, Amir Pnueli: La lógica temporal de la ramificación del tiempo . POPL 1981: 164-176
• Amir Pnueli: La lógica temporal de los programas FOCS 1977: 46–57
• Venema, Yde, 2001, "Temporal Logic", en Goble, Lou, ed., The Blackwell Guide to Philosophical Logic . 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", Manual de informática teórica , Capítulo 16, MIT Press, 1990
• Una introducción práctica al PSL, Cindy Eisner, Dana Fisman
• Vardi, Moshe Y. (2008). "De la Iglesia y antes del PSL ". En Orna Grumberg; Helmut Veith (eds.). 25 años de verificación de modelos: historia, logros, perspectivas . Saltador. ISBN 978-3-540-69849-4.preimpresión. Perspectiva histórica sobre cómo se unieron ideas aparentemente dispares en la 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 del hardware).

Otras lecturas

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

enlaces externos

• Enciclopedia de Filosofía de Stanford : "Lógica temporal", por Anthony Galton.
• Lógica temporal de Yde Venema, descripción formal de sintaxis y semántica, cuestiones de axiomatización. Tratando también los operadores temporales diádicos de Kamp (desde, hasta)
• Notas sobre juegos de 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, verificador LTL, simulador y verificador de refinamiento gratuito para CSP y sus extensiones (con variables compartidas, matrices y amplio rango de equidad).