Hispanopedia Wiki
Articulo de referencia

Lógica temporal lineal

En lógica , la lógica temporal lineal o lógica temporal lineal [ 1 ] [ 2 ] ( LTL ) es una lógica temporal modal con modalidades que se refieren al tiempo. En LTL, se pueden codi...

Hispanopedia WikiContenido en espanolLectura gratuita

En lógica , la lógica temporal lineal o lógica temporal lineal [ 1 ] [ 2 ] ( LTL ) es una lógica temporal modal con modalidades que se refieren al tiempo. En LTL, se pueden codificar fórmulas sobre el futuro de trayectorias , por ejemplo, una condición eventualmente será verdadera, una condición será verdadera hasta que otro hecho se vuelva verdadero, etc. Es un fragmento de la CTL * más compleja , que además permite tiempo ramificado y cuantificadores . A veces se denomina lógica temporal proposicional ( PTL ). [ 3 ] En términos de poder expresivo , LTL es un fragmento de la lógica de primer orden . [ 4 ] [ 5 ]

LTL fue propuesto por primera vez para la verificación formal de programas informáticos por Amir Pnueli en 1977. [ 6 ]

Sintaxis

LTL se construye a partir del conjunto de variables proposicionales AP , los operadores lógicos ¬ y ∨, y los operadores modales temporales X (algunas publicaciones usan O o N ) y U. Formalmente, el conjunto de fórmulas LTL sobre AP se define inductivamente de la siguiente manera:

  • Si p ∈ AP, entonces p es una fórmula LTL;
  • si ψ y φ son fórmulas LTL, entonces ¬ ψ , φ ∨ ψ , X ψ y φ U ψ son fórmulas LTL. [ 7 ]

X se lee como next y U se lee como until . Además de estos operadores fundamentales, existen operadores lógicos y temporales adicionales definidos en términos de los operadores fundamentales, para escribir fórmulas LTL de forma concisa. Los operadores lógicos adicionales son ∧, →, ↔, true y false . A continuación se muestran los operadores temporales adicionales.

  • G de siempre ( globalmente )
  • F para finalmente​
  • R de liberación​
  • W de semana hasta
  • M de lanzamiento poderoso

La gramática libre de contexto de LTL es la siguiente: φ  ::= ⊤ | ⊥ | pag | (¬ φ ) | ( φ ∧ φ ) | ( φ ∨ φ ) | ( φ → φ ) | ( X φ ) | ( GRAMO φ ) | ( F φ ) | ( φ U φ ) | ( φ W φ ) | ( φ R φ ) | ( φ M φ )

Semántica

Una fórmula LTL puede ser satisfecha por una secuencia infinita de valoraciones de verdad de variables en AP . Estas secuencias pueden verse como una palabra en un camino de una estructura de Kripke (una ω-palabra sobre el alfabeto 2 AP ). Sea w = a 0 ,a 1 ,a 2 ,... una ω-palabra de este tipo. Sea w ( i ) = a i . Sea w i = a i , a i +1 ,..., que es un sufijo de w . Formalmente, la relación de satisfacción ⊨ entre una palabra y una fórmula LTL se define de la siguiente manera:

  • w ⊨ p si p ∈ w (0)
  • w ⊨ ¬ ψ si w ⊭ ψ
  • w ⊨ φ ∨ ψ si w ⊨ φ o w ⊨ ψ
  • w ⊨ X ψ si w 1 ⊨ ψ (en el siguiente paso de tiempo ψ debe ser verdadero)
  • w ⊨ φ U ψ si existe i ≥ 0 tal que w i ⊨ ψ y para todo 0 ≤ k < i, w k ⊨ φ ( φ debe permanecer verdadero hasta que ψ se vuelva verdadero)

Decimos que una ω-palabra w satisface una fórmula LTL ψ cuando w ⊨ ψ . El ω-lenguaje L ( ψ ) definido por ψ es { w | w ⊨ ψ }, que es el conjunto de ω-palabras que satisfacen ψ . Una fórmula ψ es satisfacible si existe una ω-palabra w tal que w ⊨ ψ . Una fórmula ψ es válida si para cada ω-palabra w sobre el alfabeto 2 AP , tenemos w ⊨ ψ .

Los operadores lógicos adicionales se definen de la siguiente manera:

  • φ ∧ ψ ≡ ¬(¬ φ ∨ ¬ ψ )
  • φ → ψ ≡ ¬ φ ∨ ψ
  • φ ↔ ψ ≡ ( φ → ψ ) ∧ ( ψ → φ )
  • verdadero ≡ p ∨ ¬ p , donde p ∈ AP
  • falso ≡ ¬ verdadero

Los operadores temporales adicionales R , F y G se definen de la siguiente manera:

  • ψ R φ ≡ ¬(¬ ψ U ¬ φ ) ( φ permanece verdadera hasta que ψ se vuelve verdadera. Si ψ nunca se vuelve verdadera, φ debe permanecer verdadera para siempre. ψ r libera φ .)
  • F ψ ≡ verdadero U ψ (eventualmente ψ se vuelve verdadero)
  • G ψ ≡ falso R ψ ≡ ¬ F ¬ ψ ( ψ siempre permanece verdadero)

Débil hasta y fuerte liberación

Algunos autores también definen un operador binario débil de hasta , denotado W , con una semántica similar a la del operador hasta, pero no se requiere que ocurra la condición de parada (similar a release). [ 8 ] A veces es útil ya que tanto U como R pueden definirse en términos del operador débil de hasta:

  • ψ W φ ≡ ( ψ U φ ) ∨ GRAMO ψ ≡ ψ U ( φ ∨ GRAMO ψ ) ≡ φ R ( φ ∨ ψ )
  • ψ U φ ≡ F φ ∧ ( ψ W φ )
  • ψ R φ ≡ φ W ( φ ∧ ψ )

El operador binario de liberación fuerte , denotado por M , es el dual del operador débil de hasta que. Se define de forma similar al operador de hasta que, de modo que la condición de liberación debe cumplirse en algún momento. Por lo tanto, es más fuerte que el operador de liberación.

  • ψ M φ ≡ ¬(¬ ψ W ¬ φ ) ≡ ( ψ R φ ) ∧ F ψ ≡ ψ R ( φ ∧ F ψ ) ≡ φ U ( ψ ∧ φ )

La semántica de los operadores temporales se presenta gráficamente de la siguiente manera.

Equivalencias

Sean φ, ψ y ρ fórmulas LTL. Las siguientes tablas enumeran algunas de las equivalencias útiles que extienden las equivalencias estándar entre los operadores lógicos habituales.

Negación en forma normal

Todas las fórmulas de LTL se pueden transformar en forma normal de negación , donde

  • Todas las negaciones aparecen únicamente delante de las proposiciones atómicas,
  • Solo pueden aparecer los operadores lógicos verdadero , falso , ∧ y ∨, y
  • Solo pueden aparecer los operadores temporales X , U y R.

Utilizando las equivalencias anteriores para la propagación de la negación, es posible derivar la forma normal. Esta forma normal permite que R , verdadero , falso y ∧ aparezcan en la fórmula, operadores que no son fundamentales en LTL. Cabe destacar que la transformación a la forma normal de negación no aumenta considerablemente la longitud de la fórmula. Esta forma normal resulta útil para la traducción de una fórmula LTL a un autómata de Büchi .

Relaciones con otras lógicas

Se puede demostrar que LTL es equivalente a la lógica monádica de primer orden de orden , FO[<] — un resultado conocido como el teorema de Kamp — [ 9 ] o equivalentemente a los lenguajes libres de estrellas . [ 10 ]

La lógica de árbol computacional (CTL) y la lógica temporal lineal (LTL) son ambas un subconjunto de CTL* , pero son incomparables. Por ejemplo,

  • Ninguna fórmula en CTL puede definir el lenguaje que está definido por la fórmula LTL F ( G p).
  • Ninguna fórmula en LTL puede definir el lenguaje que está definido por las fórmulas CTL AG ( p → ( EX q ∧ EX ¬q) ) o AG ( EF (p)).

Problemas computacionales

La verificación de modelos y la satisfacibilidad frente a una fórmula LTL son problemas PSPACE-completos . La síntesis LTL y el problema de verificación de juegos frente a una condición de victoria LTL son 2EXPTIME-completos . [ 11 ]

Aplicaciones

Verificación de modelos de lógica temporal lineal basada en la teoría de autómatas
Las fórmulas LTL se utilizan comúnmente para expresar restricciones, especificaciones o procesos que un sistema debe seguir. El campo de la verificación de modelos tiene como objetivo verificar formalmente si un sistema cumple con una especificación dada. En el caso de la verificación de modelos basada en la teoría de autómatas, tanto el sistema de interés como la especificación se expresan como máquinas de estados finitos o autómatas independientes, y luego se comparan para evaluar si el sistema garantiza la propiedad especificada. En informática, este tipo de verificación de modelos se utiliza a menudo para verificar que un algoritmo esté estructurado correctamente.
Para comprobar las especificaciones LTL en ejecuciones infinitas del sistema, una técnica común consiste en obtener un autómata de Büchi equivalente al modelo (que acepta una palabra ω precisamente si es el modelo) y otro equivalente a la negación de la propiedad (que acepta una palabra ω precisamente si satisface la propiedad negada) (véase Lógica temporal lineal aplicada al autómata de Büchi ). En este caso, si existe una superposición en el conjunto de palabras ω aceptadas por ambos autómatas, implica que el modelo acepta ciertos comportamientos que violan la propiedad deseada. Si no hay superposición, no existen comportamientos que violen la propiedad y que sean aceptados por el modelo. Formalmente, la intersección de los dos autómatas de Büchi no deterministas es vacía si y solo si el modelo satisface la propiedad especificada. [ 12 ]
Expresar propiedades importantes en la verificación formal
Hay dos tipos principales de propiedades que se pueden expresar usando lógica temporal lineal: las propiedades de seguridad generalmente establecen que algo malo nunca sucede ( G ¬ ϕ ), mientras que las propiedades de vivacidad establecen que algo bueno sigue sucediendo ( GF ψ o G ( ϕ → F ψ )). [ 13 ] Por ejemplo, una propiedad de seguridad puede requerir que un rover autónomo nunca se precipite por un precipicio, o que un producto de software nunca permita un inicio de sesión exitoso con una contraseña incorrecta. Una propiedad de vivacidad puede requerir que el rover siempre continúe recopilando muestras de datos, o que un producto de software envíe repetidamente datos de telemetría.
En términos más generales, las propiedades de seguridad son aquellas para las que cada contraejemplo tiene un prefijo finito tal que, independientemente de cómo se extienda a un camino infinito, sigue siendo un contraejemplo. Por otro lado, para las propiedades de vivacidad, cada camino finito puede extenderse a un camino infinito que satisfaga la fórmula.
Lenguaje de especificación
Una de las aplicaciones de la lógica temporal lineal es la especificación de preferencias en el lenguaje de definición de dominio de planificación con el fin de realizar una planificación basada en preferencias .

Extensiones

La lógica temporal lineal paramétrica extiende LTL con variables en la modalidad until. [ 14 ]

Véase también

Referencias

  1. ↑ Lógica en Ciencias de la Computación: Modelado y Razonamiento sobre Sistemas : página 175
  2. ↑ "Lógica temporal de tiempo lineal" . Archivado del original el 30 de abril de 2017. Consultado el 19 de marzo de 2012 .
  3. ↑ Dov M. Gabbay ; A. Kurucz; F. Wolter; M. Zakharyaschev (2003). Lógicas modales multidimensionales: teoría y aplicaciones . Elsevier. pág. 46. ISBN  978-0-444-50826-3.
  4. ↑ Diekert, Volker. "Lenguajes definibles de primer orden" (PDF) . Universidad de Stuttgart.
  5. ↑ Kamp, Hans (1968). Lógica temporal y teoría del orden lineal (Tesis doctoral). Universidad de California en Los Ángeles.
  6. ↑ Amir Pnueli , La lógica temporal de los programas. Actas del 18.º Simposio Anual sobre Fundamentos de la Informática (FOCS) , 1977, 46-57. doi : 10.1109/SFCS.1977.32
  7. ↑ Sec. 5.1 de Christel Baier y Joost-Pieter Katoen , Principles of Model Checking , MIT Press "Principles of Model Checking - the MIT Press" . Archivado del original el 4 de diciembre de 2010. Recuperado el 17 de mayo de 2011 .
  8. ↑ Sec. 5.1.5 "Weak Until, Release, and Positive Normal Form" de los Principios de Verificación de Modelos.
  9. ↑ Abramsky, Samson ; Gavoille, Cyril; Kirchner, Claude; Spirakis, Paul (30 de junio de 2010). Autómatas, lenguajes y programación: 37.º Coloquio Internacional, ICALP... - Google Books . Springer. ISBN 9783642141614. Consultado el 30 de julio de 2014 .
  10. ↑ Moshe Y. Vardi (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
  11. ↑ A. Pnueli y R. Rosner. «Sobre la síntesis de un módulo reactivo». En Actas del 16.º Simposio ACM SIGPLAN-SIGACT sobre Principios de los lenguajes de programación (POPL '89). Association for Computing Machinery, Nueva York, NY, EE. UU., 179-190. https://doi.org/10.1145/75277.75293
  12. ↑ Moshe Y. Vardi. Un enfoque basado en la teoría de autómatas para la lógica temporal lineal. Actas del 8.º Taller de Orden Superior de Banff (Banff'94). Lecture Notes in Computer Science , vol. 1043, pp. 238–266, Springer-Verlag, 1996. ISBN 3-540-60915-6.
  13. ↑ Bowen Alpern, Fred B. Schneider , Defining Liveness , Information Processing Letters , Volumen 21, Número 4, 1985, Páginas 181-185, ISSN 0020-0190, https://doi.org/10.1016/0020-0190(85)90056-0
  14. ↑ Chakraborty, Souymodip; Katoen, Joost-Pieter (2014). "LTL paramétrico en cadenas de Markov". En Diaz, Josep; Lanese, Ivan; Sangiorgi, Davide (eds.). Informática teórica . Lecture Notes in Computer Science. Vol. 7908. Springer Berlin Heidelberg. pp. 207–221 . arXiv : 1406.6683 . Bibcode : 2014arXiv1406.6683C . doi : 10.1007/978-3-662-44602-7_17 . ISBN   978-3-662-44602-7. S2CID 12538495 . 
  • Una presentación de LTL
  • Lógica temporal de tiempo lineal y autómatas de Büchi
  • Diapositivas didácticas del profesor Alessandro Artale en la Universidad Libre de Bozen-Bolzano.
  • Algoritmos de traducción de LTL a Buchi: una genealogía, del sitio web de Spot , una biblioteca para la verificación de modelos.
  • Tempus fugit , un juego para navegador sobre operadores de transporte de carga fraccionada (incluidas modalidades pasadas).