Lógica temporal lineal

En lógica , la lógica temporal lineal o lógica temporal de tiempo lineal ^[1]^[2] ( LTL ) es una lógica temporal modal con modalidades que hacen referencia al tiempo. En LTL, se pueden codificar fórmulas sobre el futuro de los caminos , 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 más compleja CTL* , que además permite ramificar el tiempo y los cuantificadores . A veces, la LTL se denomina lógica temporal proposicional , abreviada como 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]

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

Sintaxis

La LTL se construye a partir de un conjunto finito de variables proposicionales AP , los operadores lógicos ¬ y ∨, y los operadores modales temporales 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 \in AP$ entonces p es una fórmula LTL;
si $ψ$ y $φ$ son fórmulas LTL, entonces $\neg ψ, φ \lor ψ, X ψ$ y $φ U ψ$ son fórmulas LTL. ^[7]

X se lee como ne x t y U se lee como hasta . 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 manera sucinta. Los operadores lógicos adicionales son ∧, →, ↔, true y false . A continuación se presentan los operadores temporales adicionales.

G por siempre ( g globalmente)
F por finalmente
R para liberación
W por débil hasta
M por mi poderosa liberación

Semántica

Una fórmula LTL puede satisfacerse mediante 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 ₀ ,a ₁ ,a ₂ ,... una de esas ω-palabras. Sea w ( i ) = a _i . Sea w ⁱ = 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 ¹ ⊨ ψ (en el siguiente paso de tiempo t ψ debe ser verdadero)
$w ⊨ φ U ψ$ si existe i ≥ 0 tal que w ⁱ ⊨ ψ 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 verdadero hasta que ψ se vuelva verdadero inclusive. Si ψ nunca se vuelve verdadero, φ debe permanecer verdadero para siempre. ψ r libera φ .)
$F ψ \equiv 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 hasta débil , denotado W , con una semántica similar a la del operador hasta pero no se requiere que se cumpla la condición de detención (similar a la liberación). ^[8] A veces es útil ya que tanto U como R pueden definirse en términos del hasta débil:

$ψ W φ \equiv (ψ U φ) \lor GRAMO ψ \equiv ψ U (φ \lor GRAMO ψ) \equiv φ R (φ \lor ψ)$
$ψ U φ \equiv F φ \land (ψ W φ)$
$ψ R φ \equiv φ W (φ \land ψ)$

El operador binario de liberación fuerte , denotado M , es el dual del operador hasta débil. Se define de manera similar al operador hasta, 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 φ \equiv \neg(\neg ψ W \neg φ) \equiv (ψ R φ) \land F ψ \equiv ψ R (φ \land F ψ) \equiv φ U (ψ \land φ)$

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 amplían las equivalencias estándar entre los operadores lógicos habituales.

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 sólo delante de 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.

Utilizando las equivalencias anteriores para la propagación de la negación, es posible derivar la forma normal. Esta forma normal permite que R , true , false y ∧ aparezcan en la fórmula, que no son operadores fundamentales de LTL. Nótese que la transformación a la forma normal de negación no aumenta la longitud de la fórmula. Esta forma normal es útil en la traducción de una fórmula LTL a un autómata 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 sin 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 definido por las fórmulas CTL AG ( p → ( EX q ∧ EX ¬q) ) o AG ( EF (p)).

Problemas computacionales

La comprobació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 ganadora LTL son 2EXPTIME-completos . ^[11]

Aplicaciones

Comprobación del modelo de lógica temporal lineal basado 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 de teoría de autómatas, tanto el sistema de interés como una especificación se expresan como máquinas de estados finitos separadas , o autómatas, y luego se comparan para evaluar si se garantiza que el sistema tenga 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 es obtener un autómata Büchi que sea equivalente al modelo (acepta una ω-palabra precisamente si es el modelo) y otro que sea equivalente a la negación de la propiedad (acepta una ω-palabra precisamente si satisface la propiedad negada) (cf. Lógica temporal lineal para autómata Büchi ). En este caso, si hay una superposición en el conjunto de ω-palabras aceptadas por los dos autómatas, implica que el modelo acepta algunos comportamientos que violan la propiedad deseada. Si no hay superposición, no hay comportamientos que violen la propiedad que sean aceptados por el modelo. Formalmente, la intersección de los dos autómatas Büchi no deterministas está 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 utilizando lógica temporal lineal: las propiedades de seguridad generalmente establecen que algo malo nunca sucede ( G ¬ ϕ ), mientras que las propiedades de vitalidad 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 caiga por un acantilado, o que un producto de software nunca permita un inicio de sesión exitoso con una contraseña incorrecta. Una propiedad de vitalidad 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 de modo que, independientemente de cómo se extienda a un camino infinito, sigue siendo un contraejemplo. En cambio, para las propiedades de vitalidad, 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 del dominio de planificación con el propósito de una planificación basada en preferencias . ^{[ cita requerida ]}

Extensiones

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

Véase también

Wikimedia Commons alberga una categoría multimedia sobre Lógica temporal lineal .

Referencias

^ Lógica en informática: modelado y razonamiento sobre sistemas: página 175
^ "Lógica temporal en 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. p. 46. ISBN 978-0-444-50826-3.
^ Diekert, Volker. "Lenguajes definibles de primer orden" (PDF) . Universidad de Stuttgart.
^ Kamp, Hans (1968). Lógica temporal y teoría del orden lineal (PhD). Universidad de California en Los Ángeles.
^ 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
^ Sección 5.1 de Christel Baier y Joost-Pieter Katoen , Principles of Model Checking , MIT Press "Principles of Model Checking - the MIT Press". Archivado desde el original el 2010-12-04 . Consultado el 2011-05-17 .
^ Sec. 5.1.5 "Débil hasta, liberación y forma normal positiva" de Principios de verificación de modelos.
^ Abramsky, Samson ; Gavoille, Cyril; Kirchner, Claude; Spirakis, Paul (30 de junio de 2010). Autómatas, lenguajes y programación: 37.º coloquio internacional, ICALP... - Google Libros. ISBN 9783642141614. Recuperado el 30 de julio de 2014 .
^ Moshe Y. Vardi (2008). "De la Iglesia y antes de la 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
^ 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 lenguajes de programación (POPL '89). Association for Computing Machinery, Nueva York, NY, EE. UU., 179-190. https://doi.org/10.1145/75277.75293
^ Moshe Y. Vardi. Un enfoque teórico 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, págs. 238-266, Springer-Verlag, 1996. ISBN 3-540-60915-6 .
^ Bowen Alpern, Fred B. Schneider , Definición de vitalidad , 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). Diaz, Josep; Lanese, Ivan; Sangiorgi, Davide (eds.). "LTL paramétrico en cadenas de Markov". Ciencias de la computación teóricas . Apuntes de clase en ciencias de la computación. 7908. Springer Berlin Heidelberg: 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.S2CID 12538495 .

Enlaces externos

Una presentación de LTL
Lógica temporal lineal y autómatas de Büchi
Diapositivas didácticas de LTL del profesor Alessandro Artale en la Universidad Libre de Bolzano-Bozen
Algoritmos de traducción de LTL a Buchi: una genealogía, del sitio web de Spot, una biblioteca para verificación de modelos.