Hispanopedia Wiki
Articulo de referencia

Lógica temporal

En lógica , una lógica temporal es cualquier sistema de reglas y simbolismos para representar y razonar sobre proposiciones calificadas en términos de tiempo (por ejemplo, " Sie...

Hispanopedia WikiContenido en espanolLectura gratuita

En lógica , una lógica temporal es cualquier sistema de reglas y simbolismos para representar y razonar sobre 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").

La lógica temporal ha encontrado una aplicación importante en la verificación formal , donde se utiliza para definir los requisitos de los sistemas de hardware o software. Por ejemplo, se puede especificar que, siempre que se realice una solicitud, se concede acceso a un recurso , pero nunca a dos solicitantes simultáneamente. Esta afirmación se puede expresar fácilmente mediante la lógica temporal.

El término lógica temporal también se utiliza a veces para referirse específicamente a la lógica temporal , 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 posteriormente por científicos informáticos , en particular Amir Pnueli , y lógicos .

Motivación

Consideremos la afirmación "Tengo hambre". Si bien su significado es constante en el tiempo, su valor de verdad puede variar. A veces es verdadera y a veces falsa, pero nunca simultáneamente . En una lógica temporal, una afirmación puede tener un valor de verdad que varía con el tiempo, a diferencia de una lógica atemporal, que se aplica únicamente a afirmaciones cuyos valores de verdad son constantes. 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 permite razonar sobre una línea de tiempo. Las llamadas lógicas de "tiempo lineal" se limitan a este tipo de razonamiento. Sin embargo, las lógicas de tiempo ramificado pueden razonar sobre múltiples líneas de tiempo. Esto permite, en particular, el tratamiento de entornos que pueden comportarse de forma impredecible. Siguiendo con el ejemplo, en una lógica de tiempo ramificado podemos afirmar que "existe la posibilidad de que tenga hambre para siempre" y que "existe la posibilidad de que, con el tiempo, deje de tener hambre". Si desconocemos si alguna vez seré alimentado, ambas afirmaciones pueden ser verdaderas.

Historia

Aunque la lógica de Aristóteles se centra casi exclusivamente en la teoría del silogismo categórico , existen pasajes en su obra que hoy se consideran anticipaciones de la lógica temporal y que podrían implicar una forma temprana y parcialmente desarrollada de lógica bivalente modal temporal de primer orden . Aristóteles se preocupó particularmente 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 pudiéramos decidir en el presente si un enunciado sobre un evento futuro es verdadero o falso, como por ejemplo «mañana habrá una batalla naval». [ 1 ]

Antes del trabajo de Arthur Prior , había habido poco desarrollo durante milenios, señaló Charles Sanders Peirce en el siglo XIX: [ 2 ]

Los lógicos suelen considerar el tiempo como lo que se denomina materia «extralógica». Nunca he compartido esta opinión. Sin embargo, siempre he creído que la lógica no había alcanzado un grado de desarrollo tal que la introducción de modificaciones temporales en sus formas no generara gran confusión; y sigo manteniendo en gran medida esa postura.

El primer sistema de lógica temporal fue publicado en 1947 por el lógico polaco Jerzy Łoś . [ 3 ] En su obra Podstawy Analizy Metodologicznej Kanonów Milla ( 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 puso énfasis 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 funciones temporales. La lógica podría considerarse un subproducto del objetivo principal de Łoś, [ 4 ] aunque fue la primera lógica posicional que, como marco, se utilizó posteriormente 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 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 era únicamente temporal, por lo que las expresiones se vinculaban a momentos o intervalos de tiempo específicos.

Arthur Prior se interesó por las implicaciones filosóficas del libre albedrío y la predestinación . Según su esposa, consideró formalizar la lógica temporal por primera vez en 1953. Los resultados de su investigación se presentaron por primera vez en la conferencia de Wellington en 1954. [ 4 ] El sistema que presentó Prior era sintácticamente similar a la lógica de Łoś, aunque no fue hasta 1955 que se refirió explícitamente al trabajo previo de Łoś, en la última sección del Apéndice 1 de la Lógica Formal de Prior . [ 4 ] Junto con la lógica temporal, Prior construyó algunos sistemas de lógica posicional, que heredaron sus ideas principales de Łoś. [ 5 ]

Prior dio conferencias sobre el tema en la Universidad de Oxford en 1955-56, y en 1957 publicó 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 inicial, Prior consideró que el tiempo era lineal. Sin embargo, en 1958, recibió una carta de Saul Kripke , quien señaló que esta suposición quizás no estaba justificada. En un desarrollo que anticipó uno similar en la ciencia de la computación, Prior tomó nota de esto y desarrolló dos teorías del tiempo ramificado, que llamó "Ockhamista" y "Peirceana". [ 2 ] Entre 1958 y 1965, Prior también se carteó con Charles Leonard Hamblin , y varios desarrollos iniciales en el campo pueden rastrearse 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. [ 6 ]

Nicholas Rescher continuó su trabajo en lógicas temporales posicionales en las décadas de 1960 y 1970. 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. [ 5 ] 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 pretendí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 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 candidatos en verificaciones formales fueron la lógica temporal lineal , una lógica de tiempo lineal propuesta por Amir Pnueli , y la lógica de árbol de computación (CTL), una lógica de tiempo ramificado propuesta por Mordechai Ben-Ari , Zohar Manna y Amir Pnueli. Un formalismo casi equivalente a CTL fue sugerido casi al mismo tiempo por EM Clarke y EA Emerson . El hecho de que la segunda lógica pueda resolverse de manera más eficiente que la primera no refleja la naturaleza general de las lógicas de tiempo ramificado y lineal, como a veces se ha argumentado. En cambio, Emerson y Lei demuestran que cualquier lógica de tiempo lineal puede extenderse a una lógica de tiempo ramificado que puede resolverse 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 ( Fundamentos de un análisis metodológico de los métodos de Mill ). [ 10 ] Sus conceptos filosóficos y formales podrían considerarse una continuación 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 breve pero informativa reseña en el Journal of Symbolic Logic . Esta reseña 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 era 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. Partiendo de esa base, proporcionó su sistema lógico axiomático que serviría de marco para los cánones de Mill, junto con sus aspectos temporales.

Sintaxis

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 1 ,p 2 ,p 3 ,...
  • variables que denotan los momentos de tiempo t 1 ,t 2 ,t 3 ,...
  • variables que denotan intervalos de tiempo n 1 ,n 2 ,n 3 ,...

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τ∈S{\displaystyle \tau \in S}yϵ{\displaystyle \epsilon }es una variable de intervalo de tiempo, entoncesδ(τ,ϵ)∈S{\displaystyle \delta (\tau ,\epsilon )\in S}

El conjunto de fórmulas (denotado porPara{\displaystyle {\text{Para}}}) se construye de la siguiente manera: [ 10 ]

  • Todas las fórmulas lógicas de primer orden están enPara{\displaystyle {\text{Para}}}
  • siτ∈S{\displaystyle \tau \in S}yϕ{\displaystyle \phi }es una variable proposicional, entoncesUτ(ϕ)∈Para{\displaystyle U_{\tau }(\phi )\in {\text{Para}}}
  • siϕ∈For{\displaystyle \phi \in Para}, entonces¬ϕ∈Para{\displaystyle \neg \phi \in {\text{Para}}}
  • siϕ,ψ∈Para{\displaystyle \phi ,\psi \in {\text{Para}}}y∘∈{∧,∨,→,≡}{\displaystyle \circ \in \{\wedge ,\vee ,\rightarrow ,\equiv \}}, entoncesϕ∘ψ∈Para{\displaystyle \phi \circ \psi \in {\text{Para}}}
  • siϕ∈Para{\displaystyle \phi \in {\text{Para}}}yQ∈{∀,∃}{\displaystyle Q\in \{\forall ,\exists \}}yυ{\displaystyle \upsilon }es una variable proposicional, de momento o de intervalo, entoncesQυϕ∈Para{\displaystyle Q_{\upsilon }\phi \in {\text{Para}}}

Sistema axiomático original

  1. Ut1¬pag1≡¬Ut1pag1{\displaystyle U_{t_{1}}\neg p_{1}\equiv \neg U_{t_{1}}p_{1}}
  2. Ut1(pag1→pag2)→(Ut1pag1→Ut1pag2){\displaystyle U_{t_{1}}(p_{1}\rightarrow p_{2})\rightarrow (U_{t_{1}}p_{1}\rightarrow U_{t_{1}}p_{2})}
  3. Ut1((pag1→pag2)→((pag2→pag3)→(pag1→pag3))){\displaystyle U_{t_{1}}((p_{1}\rightarrow p_{2})\rightarrow ((p_{2}\rightarrow p_{3})\rightarrow (p_{1}\rightarrow p_{3})))}
  4. Ut1(pag1→(¬pag1→pag2)){\displaystyle U_{t_{1}}(p_{1}\rightarrow (\neg p_{1}\rightarrow p_{2}))}
  5. Ut1((¬pag1→pag1)→pag1){\displaystyle U_{t_{1}}((\neg p_{1}\rightarrow p_{1})\rightarrow p_{1})}
  6. ∀t1Ut1pag1→pag1{\displaystyle \forall _{t_{1}}U_{t_{1}}p_{1}\rightarrow p_{1}}
  7. ∀t1∀norte1∃t2∀pag1(Uδ(t1,norte1)pag1≡Ut2pag1){\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. ∀t1∀norte1∃t2∀pag1(Uδ(t2,norte1)pag1≡Ut1pag1){\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. ∀t1∃pag1∀t2(Ut2pag1≡∀pag2(Ut1pag2≡Ut2pag2)){\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 temporal de Prior (TL)

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

  • P : "Fue el caso que..." (P significa "pasado")
  • F : "Sucederá que..." (F significa "futuro")
  • G : "Siempre será así..."
  • H : "Siempre ha sido así..."

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

  • π⊨FGRAMOϕ{\displaystyle \pi \vDash FG\phi }: "En cierto punto,ϕ{\displaystyle \phi }"Esto es cierto en todos los estados futuros de la trayectoria".
  • π⊨GRAMOFϕ{\displaystyle \pi \vDash GF\phi }: "ϕ{\displaystyle \phi }"Esto es cierto en infinitos estados del camino".

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

F≡¬GRAMO¬PAG≡¬H¬{\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 :

ϕ::=a|⊥|¬ϕ|ϕ∨ϕ|GRAMOϕ|Hϕ{\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 viene dado por una tripleta ( T , <, V ) de un marco y una función V llamada valuació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 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 ]
  • Satisfactorio con respecto a F si existe un modelo U =( T ,<, V ) con ( T ,<) en F tal que para algún u en T , U ⊨ ϕ [ u ]
  • una consecuencia de una sentencia ψ 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 solo 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, basadas en el siguiente esquema axiomático: [ 15 ]

  1. A donde A es una tautología de la lógica de primer orden.
  2. G( A → B )→(G A →G B )
  3. H( A → B )→(H A →H B )
  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 , infiera G A.
  3. Dada una tautología A , infiera H A.

Se pueden derivar las siguientes reglas:

  1. Regla de Becker : dado A → B , deduce T A →T B donde T es un tiempo verbal , 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 lo tanto F por P) y viceversa.
  3. Dualidad : dado un teorema A , deduzca su enunciado dual A *, que se obtiene intercambiando ∧ con ∨, G con F y H con P.

Traducción a lógica de predicados

Burgess proporciona una traducción de Meredith de enunciados en TL a enunciados en lógica de primer orden con una variable libre x 0 (que representa el momento presente). Esta traducción M se define recursivamente como sigue: [ 16 ]

METRO(a)=a∗incógnita0METRO(¬ϕ)=¬METRO(ϕ)METRO(ϕ∧ψ)=METRO(ϕ)∧METRO(ψ)METRO(GRAMOϕ)=∀incógnita1(incógnita0<incógnita1→METRO(A+))METRO(Hϕ)=∀incógnita1(incógnita1<incógnita0→METRO(A+)){\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}}}

dóndeA+{\displaystyle A^{+}}es la oración A con todos los índices de variables incrementados en 1 ya∗{\displaystyle a^{*}}es un predicado de un solo lugar definido porincógnita↦V(a,incógnita){\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 los operadores veritativo-funcionales usuales (¬,∨,∧,→{\displaystyle \neg ,\lor ,\land ,\rightarrow }). Los operadores modales utilizados en la lógica temporal lineal y la lógica de árbol de computación se definen de la siguiente manera.

Símbolos alternativos:

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

Los operadores unarios son fórmulas bien formadas siempre que B( φ ) sea una fórmula bien formada. Los operadores binarios son fórmulas bien formadas siempre que B( φ ) y C( φ ) sean fórmulas bien formadas.

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

Lógicas temporales

Las lógicas temporales incluyen:

Una variante, estrechamente relacionada con las lógicas temporales, cronológicas o de tiempo verbal, son las lógicas modales basadas en la "topología", el "lugar" o la "posición espacial". [ 23 ] [ 24 ]

Véase también

Notas

  1. ↑ Vardi 2008, pág. 153
  2. 1 2 3 Vardi 2008, pág. 154
  3. ^ Loś , Jerzy (1947). "Podstawy análisis metodológicoznej kanonów Milla" . Zasoby Biblioteki Głównej Umcs (en polaco). nakł. Uniwersytetu Marii Curie-Skłodowskiej.
  4. 1 2 3 Ø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: Temas adicionales de Prior, Volumen 2. Lógica y filosofía del tiempo. ISBN 9788772102658.
  5. 1 2 Rescher, Nicholas; Garson, James (enero de 1969). " Lógica topológica" . The Journal of Symbolic Logic . 33 (4): 537– 548. doi : 10.2307/2271360 . ISSN 0022-4812 . JSTOR 2271360. S2CID 2110963 .   
  6. ↑ 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.págs.  176–178, 210
  7. ↑ "Lógica temporal (Enciclopedia de filosofía de Stanford)" . Plato.stanford.edu . Consultado el 30 de julio de 2014 .
  8. ↑ Walter Carnielli; Claudio Pizzi (2008). Modalidades y multimodalidades . Springer. pág. 181. ISBN  978-1-4020-8589-5.
  9. ↑ Sergio Tessaris; Enrico Franconi; Thomas Eiter (2009). Reasoning Web. Tecnologías semánticas para sistemas de información: 5.ª Escuela Internacional de Verano 2009, Brixen-Bressanone, Italia, 30 de agosto - 4 de septiembre de 2009, Conferencias tutoriales . Springer. pág. 112. ISBN  978-3-642-03753-5.
  10. 1 2 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. ↑ Prior, Arthur Norman (2003). Tiempo y modalidad: las conferencias John Locke de 1955-1956, impartidas en la Universidad de Oxford . Oxford: The Clarendon Press. ISBN 9780198241584OCLC 905630146​​ 
  12. ↑ Lawford, M. (2004). "Una introducción a las lógicas temporales" (PDF) . Departamento de Ciencias de la Computación, Universidad McMaster .
  13. ↑ Goranko, Valentin; Galton, Antony (2015). "Lógica temporal". En 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. ↑ Müller, Thomas (2011). "Lógica temporal o de tiempo" (PDF) . En Horsten, Leon (ed.). The Continuum Companion to Philosophy Logic . A&C Black. pág. 329. 
  15. ↑ Burgess, John P. (2009). Lógica filosófica . Princeton, Nueva Jersey: Princeton University Press. pág. 21. ISBN  9781400830497OCLC 777375659​​ 
  16. ↑ Burgess, John P. (2009). Lógica filosófica . Princeton, Nueva Jersey: Princeton University Press. pág. 17. ISBN  9781400830497OCLC 777375659​​ 
  17. ↑ "Lógica temporal" . Enciclopedia de filosofía de Stanford . 7 de febrero de 2020. Consultado el 19 de abril de 2022 .
  18. 1 2 Maler, O.; Nickovic, D. (2004). "Monitoring temporal properties of continuous signals". doi : 10.1007/978-3-540-30206-3_12 .
  19. ↑ Mehrabian, Mohammadreza; Khayatian, Mohammad; Shrivastava, Aviral; Eidson, John C.; Derler, Patricia; Andrade, Hugo A.; Li-Baboud, Ya-Shian; Griffor, Edward; Weiss, Marc; Stanton, Kevin (2017). "Lógica temporal de marca de tiempo (TTL) para probar la sincronización de sistemas ciberfísicos" . ACM Transactions on Embedded Computing Systems . 16 (5s): 1– 20. doi : 10.1145/3126510 . S2CID 3570088 . 
  20. ↑ Koymans, R. (1990). "Especificación de 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, Nicholas (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 del 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

  • 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., The Blackwell Guide to Philosophical Logic . Blackwell.
  • EA Emerson y Chin-Laung Lei, " Modalidades para la verificación de modelos: la lógica temporal ramificada 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
  • Introducción práctica al PSL , Cindy Eisner, Dana Fisman
  • Vardi, Moshe Y. (2008). «De la Iglesia y el Preámbulo a 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 confluyeron en la informática y la ingeniería. (La mención de Church en el título de este artículo hace referencia a un trabajo poco conocido de 1957, en el que Church propuso un método para realizar la verificación de hardware).

Lecturas adicionales

  • 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.
  • 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 por Ian Hodkinson, incluyendo 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 y un amplio rango de equidad).