En lógica , la lógica temporal lineal o la lógica temporal de tiempo 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 las rutas , por ejemplo, una condición eventualmente será verdadera, una condición será verdadera hasta que otro hecho se vuelva verdadero, etc. Es un fragmento del CTL * más complejo , que además permite la ramificación tiempo y cuantificadores. Posteriormente, LTL a veces se denomina lógica temporal proposicional , abreviado PTL . [3] En términos de poder expresivo, la lógica temporal lineal (LTL) es un fragmento de la lógica de primer orden . [4] [5]
El LTL fue propuesto por primera vez para la verificación formal de programas de computadora por Amir Pnueli en 1977. [6]
Sintaxis
LTL se construye a partir de un conjunto finito de variables proposicionales AP , los operadores lógicos ¬ y ∨, y los temporales operadores modales X (alguna literatura utiliza 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 ne x t y U se lee como u ntil. Aparte 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 manera sucinta. Los operadores lógicos adicionales son ∧, →, ↔, verdadero y falso . A continuación se muestran los operadores temporales adicionales.
- G para siempre ( g lobally)
- F para f inalmente
- R para r elease
- W por w eak hasta
- M para un lanzamiento fuerte
Semántica
Una fórmula LTL puede satisfacerse mediante una secuencia infinita de evaluaciones de verdad de variables en AP . Estas secuencias pueden verse como una palabra en una ruta de una estructura Kripke (una palabra ω sobre el alfabeto 2 AP ). Sea w = a 0 , a 1 , a 2 , ... una palabra an. 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 x t ψ debe ser verdadero)
- w ⊨ φ U ψ si existe i ≥ 0 tal que w i ⊨ Psi y para todos 0 ≤ k ,>w k ⊨ φ ( φ debe seguir siendo cierto u asta ψ se convierte en verdadera)
Decimos que una palabra w de ω 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 satisfactoria si existe una ω-palabra w tal que w ⊨ ψ . Una fórmula ψ es válida si para cada ω-palabra w sobre el alfabeto 2 AP , 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 como sigue:
- ψ R φ ≡ ¬ (¬ ψ U ¬ φ ) ( φ permanece verdadero hasta que, inclusive, una vez ψ se convierte en verdadero. Si ψ nunca se convierte en verdadero, φ debe permanecer verdadero para siempre).
- F ψ ≡ verdadero U ψ (eventualmente ψ se convierte en verdadero)
- G ψ ≡ falso R ψ ≡ ¬ F ¬ ψ ( ψ siempre permanece verdadero)
Débil hasta y fuerte liberación
Algunos autores también definen un operador binario hasta débil , denominado W , con una semántica similar a la del operador hasta, pero no se requiere que ocurra la condición de parada (similar a la liberación). [8] A veces es útil ya que tanto U como R pueden definirse en términos de los débiles hasta que:
- ψ W φ ≡ ( ψ U φ ) ∨ G ψ ≡ ψ U ( φ ∨ G ψ ) ≡ φ R ( φ ∨ ψ )
- ψ U φ ≡ F φ ∧ ( ψ W φ )
- ψ R φ ≡ φ W ( φ ∧ ψ )
El operador binario de liberación fuerte , denominado M , es el dual de débil hasta. Se define de forma similar al operador hasta, por lo que la condición de liberación debe mantenerse 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 pictóricamente de la siguiente manera.
Textual | Simbólico | Explicación | Diagrama |
---|---|---|---|
Operadores unarios : | |||
X φ | ne X t: φ debe mantenerse en el siguiente estado. | ||
F φ | F inalmente: φ finalmente tiene que sostener (en algún lugar en el camino posterior). | ||
G φ | G lobally: φ tiene que sostener en toda la trayectoria posterior. | ||
Operadores binarios : | |||
ψ U φ | T asta: ψ tiene que sostener al menos hasta que φ es verdadera, la cual debe contener a la corriente o una posición futura. | ||
ψ R φ | R elease: φ tiene que ser verdadero hasta e incluyendo el punto donde ψ primero se convierte en verdadero; si ψ nunca se convierte en verdad, φ debe seguir siendo verdad para siempre. |
| |
ψ W φ | W EAK hasta que: ψ tiene que sostener al menos hasta φ ; si φ nunca se convierte en verdad, ψ debe seguir siendo verdad para siempre. |
| |
ψ M φ | Versión fuerte: φ tiene que ser verdad hasta e incluyendo el punto donde ψ se convierte en primer verdadero, que debe contener a la corriente o una posición futura. |
Equivalencias
Sean φ, ψ y ρ fórmulas LTL. Las siguientes tablas enumeran algunas de las equivalencias útiles que amplían las equivalencias estándar entre los operadores lógicos habituales.
Distributividad | ||
---|---|---|
X (φ ∨ ψ) ≡ ( X φ) ∨ ( X ψ) | X (φ ∧ ψ) ≡ ( X φ) ∧ ( X ψ) | X (φ U ψ) ≡ ( X φ) U ( X ψ) |
F (φ ∨ ψ) ≡ ( F φ) ∨ ( F ψ) | G (φ ∧ ψ) ≡ ( G φ) ∧ ( G ψ) | |
ρ U (φ ∨ ψ) ≡ (ρ U φ) ∨ (ρ U ψ) | (φ ∧ ψ) U ρ ≡ (φ U ρ) ∧ (ψ U ρ) |
Propagación de la negación | |||
---|---|---|---|
X es auto-dual | F y G son duales | U y R son duales | W y M son duales |
¬ X φ ≡ X ¬φ | ¬ F φ ≡ G ¬φ | ¬ (φ U ψ) ≡ (¬φ R ¬ψ) | ¬ (φ W ψ) ≡ (¬φ M ¬ψ) |
¬ G φ ≡ F ¬φ | ¬ (φ R ψ) ≡ (¬φ U ¬ψ) | ¬ (φ M ψ) ≡ (¬φ W ¬ψ) |
Propiedades temporales especiales | ||
---|---|---|
F φ ≡ F F φ | G φ ≡ G G φ | φ U ψ ≡ φ U (φ U ψ) |
φ U ψ ≡ ψ ∨ (φ ∧ X (φ U ψ)) | φ W ψ ≡ ψ ∨ (φ ∧ X (φ W ψ)) | φ R ψ ≡ ψ ∧ (φ ∨ X (φ R ψ)) |
G φ ≡ φ ∧ X ( G φ) | F φ ≡ φ ∨ X ( F φ) |
Forma normal de negación
Todas las fórmulas de LTL se pueden transformar en forma normal de negación , donde
- todas las negaciones aparecen solo frente a las proposiciones atómicas,
- sólo pueden aparecer otros operadores lógicos verdadero , falso , ∧ y ∨, y
- sólo pueden aparecer los operadores temporales X , U y R.
Usando 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, que no son operadores fundamentales de LTL. Tenga en cuenta que la transformación a la forma normal de negación no aumenta el tamaño de la fórmula. Esta forma normal es útil en la traducción de LTL a autómata Büchi .
Relaciones con otras lógicas
Se puede demostrar que LTL es equivalente a la lógica de orden monádica de primer orden , FO [<] - un resultado conocido como teorema de Kamp - [9] o equivalentemente lenguajes libres de estrellas . [10]
La lógica de árbol de cálculo (CTL) y la lógica temporal lineal (LTL) son un subconjunto de CTL * , pero son incomparables. Por ejemplo,
- Ninguna fórmula en CTL puede definir el lenguaje definido por la fórmula LTL F ( G p).
- Ninguna fórmula en LTL puede definir el lenguaje definido por las fórmulas CTL AG (p → ( EX q ∧ EX ¬q)) o AG ( EF (p)).
Sin embargo, existe un subconjunto de CTL * que es un superconjunto adecuado de CTL y LTL.
Problemas computacionales
La verificación del modelo y la capacidad de satisfacer una fórmula LTL son problemas completos de PSPACE . La síntesis LTL y el problema de la verificación de juegos frente a una condición ganadora LTL es 2EXPTIME-complete . [11]
Aplicaciones
- Verificación del modelo lógico temporal lineal teórico de autómatas
- Una forma importante de verificar el modelo es expresar las propiedades deseadas (como las descritas anteriormente) utilizando operadores LTL y verificar si el modelo satisface esta propiedad. Una técnica es obtener un autómata Büchi que sea equivalente al modelo (acepta una palabra ω precisamente si es el modelo) y otra que sea equivalente a la negación de la propiedad (acepta una palabra ω precisamente satisface la negación propiedad) (cf. Lógica temporal lineal al autómata Büchi ). La intersección de los dos autómatas Büchi no deterministas está vacía si y solo si el modelo satisface la propiedad. [12]
- Expresando propiedades importantes en la verificación formal
- Hay dos tipos principales de propiedades que se pueden expresar usando la lógica temporal lineal: las propiedades de seguridad generalmente indican que algo malo nunca sucede ( G ¬ ϕ ), mientras que las propiedades de vivacidad establecen que algo bueno sigue sucediendo ( GF ψ o G ( ϕ → F ψ ). [13] De manera más general, las propiedades de seguridad son aquellas para las que cada contraejemplo tiene un prefijo finito de modo que, sin embargo, se extiende a un camino infinito, sigue siendo un contraejemplo. Para las propiedades de vivacidad, por otro lado, cada prefijo finito de un contraejemplo 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 propósito de la planificación basada en preferencias . [ cita requerida ]
Extensiones
La lógica temporal lineal paramétrica extiende LTL con variables en la modalidad hasta. [14]
Ver también
- Lenguaje de acción
- Lógica temporal métrica
Referencias
- ^ Lógica en ciencias de la computación: modelado y razonamiento de sistemas : página 175
- ^ "Lógica temporal de tiempo lineal" . Archivado desde el original el 30 de abril de 2017 . Consultado el 19 de marzo de 2012 .
- ^ Dov M. Gabbay ; A. Kurucz; F. Wolter; M. Zakharyaschev (2003). Lógicas modales multidimensionales: teoría y aplicaciones . Elsevier. pag. 46. ISBN 978-0-444-50826-3.
- ^ Diekert, Volker. "Lenguajes definibles de primer orden" (PDF) . Universidad de Stuttgart.
- ^ Kamp, Hans (1968). Lógica Tensa y Teoría del Orden Lineal (Doctorado). Universidad de California, Los Angeles.
- ^ Amir Pnueli , La lógica temporal de los programas. Actas del 18º Simposio Anual sobre Fundamentos de las Ciencias de la Computación (FOCS) , 1977, 46–57. doi : 10.1109 / SFCS.1977.32
- ^ Sec. 5.1 de Christel Baier y Joost-Pieter Katoen , Principles of Model Checking, MIT Press "Copia archivada" . Archivado desde el original el 4 de diciembre de 2010 . Consultado el 17 de mayo de 2011 .CS1 maint: copia archivada como título ( enlace )
- ^ Sec. 5.1.5 "Hasta Débil, Liberación y Forma Normal Positiva" de los Principios de Verificación del Modelo.
- ^ 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 . ISBN 9783642141614. Consultado el 30 de julio de 2014 .
- ^ Moshe Y. Vardi (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
- ^ "Sobre la síntesis de un módulo reactivo" .
- ^ Moshe Y. Vardi. Un enfoque teórico de los autómatas para la lógica temporal lineal. Actas del 8º Taller de Orden Superior de Banff (Banff'94). Notas de la conferencia en Ciencias de la Computación, vol. 1043, págs.238-266, Springer-Verlag, 1996. ISBN 3-540-60915-6 .
- ^ 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
- ^ Chakraborty, Souymodip; Katoen, Joost-Pieter (2014). Díaz, Josep; Lanese, Ivan; Sangiorgi, Davide (eds.). "LTL paramétrico en cadenas de Markov". Informática Teórica . Apuntes de conferencias en Ciencias de la Computación. Springer Berlín Heidelberg. 7908 : 207–221. arXiv : 1406,6683 . Código bibliográfico : 2014arXiv1406.6683C . doi : 10.1007 / 978-3-662-44602-7_17 . ISBN 978-3-662-44602-7.
- enlaces externos
- Una presentación de LTL
- Lógica temporal de tiempo lineal y autómatas Büchi
- LTL Diapositivas didácticas del profesor Alessandro Artale en la Universidad Libre de Bozen-Bolzano
- LTL a algoritmos de traducción Buchi una genealogía, del sitio web de Spot una biblioteca para la verificación de modelos.