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 como algo "). A veces también se usa para referirse a la lógica del tiempo , 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 por científicos informáticos , en particular Amir Pnueli , ylógicos .
La lógica temporal ha encontrado una aplicación importante en la verificación formal , donde se utiliza para establecer los requisitos de los sistemas de hardware o software. Por ejemplo, se puede querer decir que cada vez que se realiza una solicitud, eventualmente se otorga acceso a un recurso , pero nunca se otorga a dos solicitantes simultáneamente. Tal 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 declaración puede variar con el tiempo. A veces es verdadero y, a veces, 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. Las llamadas "lógicas del tiempo" lineales se limitan a este tipo de razonamiento. Las lógicas de ramificación, sin embargo, pueden razonar sobre múltiples líneas de tiempo. Esto presupone un entorno que puede actuar de manera impredecible. Para continuar con el ejemplo, en una lógica ramificada podemos afirmar que "existe la posibilidad de que me quede hambriento para siempre", y que "existe la posibilidad de que eventualmente ya no tenga hambre". Si no sabemos si es o no yo jamás serán alimentados, estas afirmaciones pueden ser ciertas ambas.
Historia
Aunque la lógica de Aristóteles está casi enteramente relacionada con la teoría del silogismo categórico , hay pasajes en su trabajo que ahora se ven como anticipaciones de la lógica temporal, y pueden implicar una forma temprana, parcialmente desarrollada de lógica binaria 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 "hay mañana será 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 denomina 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 daría lugar a una gran confusión; y todavía soy mucho de esa forma de pensar.
Arthur Prior estaba preocupado por las cuestiones 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. 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 este trabajo inicial, Prior consideraba que el tiempo era lineal. En 1958, sin embargo, recibió una carta de Saul Kripke , quien señaló que esta suposición tal vez sea injustificada. En un desarrollo que presagiaba uno similar en la informática, Prior tomó esto en cuenta y desarrolló dos teorías del tiempo de ramificación, a las que llamó "Ockhamist" y "Peircean". [2] [ aclaración necesaria ] Entre 1958 y 1965 Prior también mantuvo correspondencia 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 trabajo más maduro sobre el tema, el libro Past, Present, and Future en 1967. Murió dos años después. [3]
Los operadores temporales binarios Desde y Hasta fueron introducidos por Hans Kamp en su Ph.D. de 1968. tesis, [4] 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 . [5] [2] [6]
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 , una lógica de tiempo ramificado de Mordejai Ben-Ari , Zohar Manna y Amir Pnueli. EM Clarke y EA Emerson sugirieron un formalismo casi equivalente al CTL casi al mismo tiempo . El hecho de que la segunda lógica pueda decidirse de manera más eficiente que la primera no se refleja en las lógicas ramificadas y lineales en general, como a veces se ha argumentado. Más bien, Emerson y Lei muestran que cualquier lógica lineal puede extenderse a una lógica de ramificación que puede decidirse con la misma complejidad.
La lógica del tiempo de Prior (TL)
La lógica del tiempo oracional introducida en Time and Modality 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) . [7]
- P : "Fue el caso que ..." (P significa "pasado")
- F : "Será el caso de 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: [8]
- : "En un cierto punto, es cierto en todos los estados futuros del camino "
- : " es cierto en un número infinito de estados en el camino "
A partir de P y F se pueden definir G y H , y viceversa:
Sintaxis y semántica
Se especifica una sintaxis mínima para TL con la siguiente gramática BNF :
donde a es alguna fórmula atómica . [9]
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
Declaración | ... es cierto justo cuando |
---|---|
U ⊨ a [ u ] | V ( a , u ) = verdadero |
U ⊨¬ ϕ [ u ] | no U ⊨ ϕ [ u ] |
U ⊨ ( ϕ ∧ ψ ) [ u ] | U ⊨ ϕ [ u ] y U ⊨ ψ [ u ] |
U ⊨ ( ϕ ∨ ψ ) [ u ] | U ⊨ ϕ [ u ] o U ⊨ ψ [ u ] |
U ⊨ ( ϕ → ψ ) [ u ] | U ⊨ ψ [ u ] si U ⊨ ϕ [ u ] |
U ⊨G ϕ [ u ] | U ⊨ ϕ [ v ] para todo v con u < v |
U ⊨H ϕ [ u ] | U ⊨ ϕ [ v ] para todo v con v < u |
Dada una clase F de fotogramas, 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 todo u en T , U ⊨ ϕ [ u ]
- satisfactorio con respecto a F si hay 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 todo modelo U = ( T , <, V ) con ( T , <) en F y para todo 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
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 de axioma: [11]
- A donde A es una tautología de la lógica de primer orden
- G ( A → B ) → (G A → G B )
- H ( A → B ) → (H A → H B )
- A → GP A
- A → HF A
con las siguientes reglas de deducción:
- dado A → B y A , deducir B ( modus ponens )
- dada una tautología A , inferir G A
- dada una tautología A , inferir H A
Se pueden derivar las siguientes reglas:
- Regla de Becker : dado A → B , deducir T A → T B donde T es un tiempo verbal , cualquier secuencia formada por G, H, F y P.
- 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.
- 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 la lógica de predicados
Burgess da una traducción de Meredith de declaraciones en TL a declaraciones 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: [12]
dónde es la sentencia con todos los índices variables incrementados en 1 y es un predicado de un lugar definido por .
Operadores temporales
La lógica temporal tiene dos tipos de operadores: operadores lógicos y operadores modales [1] . Los operadores lógicos son operadores habituales de función de verdad (). Los operadores modales utilizados en lógica temporal lineal y lógica de árbol de cálculo se definen como sigue.
Textual | Simbólico | Definición | Explicación | Diagrama |
---|---|---|---|---|
Operadores binarios | ||||
φ U ψ | T asta: ψ posee en el actual o una posición futura, y φ tiene de mantener hasta esa posición. En esa posición φ no tiene que aguantar más. | |||
φ R ψ | R elease: φ libera ψ si ψ es verdadero hasta e incluyendo la primera posición en la que φ es verdadero (o para siempre si tal posición no existe). | |||
Operadores unarios | ||||
N φ | N ext: φ debe mantenerse en el siguiente estado. ( X se usa como sinónimo). | |||
F φ | F uture: φ finalmente tiene que sostener (en algún lugar en el camino posterior). | |||
G φ | G lobally: φ tiene que sostener en toda la trayectoria posterior. | |||
A φ | Todo : φ debe mantenerse en todas las rutas a partir del estado actual. | |||
E φ | E xistas: existe al menos una ruta a partir del estado actual donde φ se mantiene. |
Símbolos alternativos:
- el operador R a veces se denota por V
- El operador W es el débil hasta que el operador: es equivalente a
Los operadores unarios son fórmulas bien formadas siempre que B ( φ ) esté bien formado. 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 .
Lógicas temporales
Las lógicas temporales incluyen
- Lógica de intervalo temporal (ITL)
- Lógica temporal lineal (LTL)
- Lógica de árbol de cálculo (CTL)
- Lógica temporal de señal (STL) [13]
- Lógica temporal de marca de tiempo (TTL) [14]
- Lenguaje de especificación de propiedad (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) [15]
- Lógica temporal de intervalo métrico (MITL) [13]
- Lógica temporal proposicional temporizada (TPTL)
- Lógica temporal lineal truncada (TLTL) [16]
- Lógica hipertemporal (HyperLTL) [17]
Una variación, estrechamente relacionada con las lógicas temporales, cronológicas o tensas, son las lógicas modales basadas en la "topología", el "lugar" o la "posición espacial". [18] [19]
Ver también
- Formalismo HPO
- Estructura Kripke
- Teoría de los autómatas
- Gramática de Chomsky
- Sistema de transición estatal
- Cálculo de duración (DC)
- Lógica híbrida
- Lógica temporal en la verificación de estados finitos
- Lógica temporal de acciones (TLA)
- Publicaciones importantes en verificación formal (incluido el uso de lógica temporal en verificación formal )
- Lenguaje de coordinación Reo
- Lógica modal
- Materiales de investigación: Archivo de la Sociedad Max Planck
Notas
- ^ Vardi, 2008, p. 153
- ↑ a b c Vardi, 2008, p. 154
- ^ 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
- ^ "Lógica temporal (enciclopedia de filosofía de Stanford)" . Platón.stanford.edu . Consultado el 30 de julio de 2014 .
- ^ Walter Carnielli; Claudio Pizzi (2008). Modalidades y multimodalidades . Saltador. pag. 181. ISBN 978-1-4020-8589-5.
- ^ Sergio Tessaris; Enrico Franconi; Thomas Eiter (2009). Razonamiento 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 . Saltador. pag. 112. ISBN 978-3-642-03753-5.
- ^ Antes, Arthur Norman (2003). Tiempo y modalidad: las conferencias de John Locke para 1955-6, dictadas en la Universidad de Oxford . Oxford: The Clarendon Press. ISBN 9780198241584. OCLC 905630146 .
- ^ Lawford, M. (2004). "Introducción a las lógicas temporales" (PDF) . Departamento de Ciencias de la Computación de la Universidad McMaster .
- ^ Goranko, Valentin; Galton, Antony (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.
- ^ Müller, Thomas (2011). "Lógica tensa o temporal" (PDF) . En Horsten, Leon (ed.). El compañero continuo de la lógica filosófica . A&C Negro. pag. 329.
- ^ Burgess, John P. (2009). Lógica filosófica . Princeton, Nueva Jersey: Princeton University Press. pag. 21. ISBN 9781400830497. OCLC 777375659 .
- ^ Burgess, John P. (2009). Lógica filosófica . Princeton, Nueva Jersey: Princeton University Press. pag. 17. ISBN 9781400830497. OCLC 777375659 .
- ^ a b Maler, O .; Nickovic, D. (2004). "Monitorización de propiedades temporales de señales continuas". doi : 10.1007 / 978-3-540-30206-3_12 .
- ^ https://asu.pure.elsevier.com/en/publications/timestamp-temporal-logic-ttl-for-testing-the-timing-of-cyber-phys
- ^ Koymans, R. (1990). "Especificación de propiedades en tiempo real con lógica métrica temporal", Real-Time Systems 2 (4): 255–299. doi : 10.1007 / BF01995674 .
- ^ Li, Xiao, Cristian-Ioan Vasile y Calin Belta. "Aprendizaje reforzado con recompensas de lógica temporal". doi : 10.1109 / IROS.2017.8206234
- ^ https://link.springer.com/chapter/10.1007/978-3-642-54792-8_15
- ^ 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.
- ^ 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
- Mordejai Ben-Ari, Zohar Manna, Amir Pnueli: La lógica temporal del tiempo de ramificación . 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 C. 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 Ciencias de la Computación Teórica , Capítulo 16, MIT Press, 1990
- Una introducción práctica a PSL , Cindy Eisner, Dana Fisman
- Vardi, Moshe Y. (2008). "De Iglesia y Previo a PSL ". En Orna Grumberg; Helmut Veith (eds.). 25 años de revisió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 de 1957 poco conocido, en el que Church propuso una forma de realizar la verificación de 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 la sintaxis y la semántica, cuestiones de axiomatización. Tratando también 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 comprobadores de modelos genéricos para varias lógicas temporales
- PAT es un potente comprobador de modelos, comprobador LTL, simulador y comprobador de refinamiento gratuito para CSP y sus extensiones (con variables compartidas, matrices, amplia gama de equidad).