Lógica temporal lineal

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 usa 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 próximo (next) y U se lee como "hasta" (until). Además de estos operadores fundamentales, hay operadores lógicos y temporales adicionales definidos en términos de operadores fundamentales para escribir fórmulas LTL de manera sucinta. Los operadores lógicos adicionales son ∧, →, ↔, verdadero y falso . Los siguientes son los operadores temporales adicionales.

• G para "siempre" (globalmente)
• F para "eventualmente" (en el futuro)
• R para liberación (release)
• W por débil hasta (weak until)
• M para liberación fuerte (strong release)

Una fórmula LTL puede satisfacerse mediante una secuencia infinita de evaluaciones de verdad de variables en AP. Estas secuencias se pueden ver como una palabra en el camino de una estructura de Kripke (una ω-palabra sobre el alfabeto 2^AP). Sea w = a₀,a₁,a₂, ... una ω-palabra. 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 ${\displaystyle \vDash }$ entre una palabra y una fórmula LTL se define de la siguiente manera:

• w ${\displaystyle \vDash }$ p si p ∈ w(0)
• w ${\displaystyle \vDash }$ ¬ψ si w ${\displaystyle \nvDash }$ ψ
• w ${\displaystyle \vDash }$ φ ∨ ψ si w ${\displaystyle \vDash }$ φ o w ${\displaystyle \vDash }$ ψ
• w ${\displaystyle \vDash }$ X ψ si w¹ ${\displaystyle \vDash }$ ψ (en el próximo paso ψ debe ser verdadero)
• w ${\displaystyle \vDash }$ φ U ψ si existe i ≥ 0 tal que wⁱ ${\displaystyle \vDash }$ ψ y para todo 0 ≤ k <i, w ^k ${\displaystyle \vDash }$ φ (φ debe permanecer verdadero hasta (u) que ψ se convierte en verdadera)

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

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

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

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

• ψ R φ ≡ ¬ (¬ψ U ¬φ) (φ permanece verdadero e incluso una vez que ψ se vuelve verdadero. Si ψ nunca se vuelve verdad, φ debe permanecer así para siempre. )
• F ψ ≡ verdadero U ψ (eventualmente ψ se vuelve verdadero)
• G ψ ≡ falso R ψ ≡ ¬ F ¬ψ (ψ siempre permanece verdadero)

Liberación "hasta débil" y "hasta fuerte"

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 es necesario que se produzca la condición de detención (similar a la liberación).[8] A veces es esto es útil ya que U y R pueden definirse en términos de hasta débil:

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

El operador binario de liberación fuerte, denotado M, es el dual del hasta débil. Se define de manera 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 para los operadores temporales se presenta gráficamente de la siguiente manera.

Textual	Simbólico	Explicación	Diagrama
Operadores unarios :
X φ	${\displaystyle \bigcirc \varphi }$	PróXimo: φ tiene que mantenerse en el siguiente estado.
F φ	${\displaystyle \Diamond \varphi }$	Finalmente: φ tiene que sostenerse (en algún lugar en el camino posterior).
G φ	${\displaystyle \Box \varphi }$	Globalmente: φ tiene que mantenerse todo el camino posterior.
Operadores binarios :
ψ U φ	${\displaystyle \psi \;{\mathcal {U}}\,\varphi }$	Hasta(U): ψ debe mantenerse al menos hasta que φ se convierta en verdadero en una posición actual o futura.
ψ R φ	${\displaystyle \psi \;{\mathcal {R}}\,\varphi }$	LibeRación: φ tiene que ser verdadero hasta e incluyendo el punto donde ψ se vuelve verdadero por primera vez; si ψ nunca se convierte en verdad, φ debe permanecer así verdadero para siempre.
ψ W φ	${\displaystyle \psi \;{\mathcal {W}}\,\varphi }$	Hasta débil (W): ψ tiene que sostenerse al menos hasta φ; si φ nunca se convierte en verdad, ψ debe permanecer así para siempre.
ψ M φ	${\displaystyle \psi \;{\mathcal {M}}\,\varphi }$	Liberación fuerte: φ tiene que ser verdadero hasta e incluyendo el punto donde ψ se convierte en verdadero, el cual debe mantenerse en la posición actual o futura.

Sea φ, ψ 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.

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

• todas las negaciones aparecen solo frente a las proposiciones atómicas,
• solo pueden aparecer otros operadores lógicos verdadero, falso, ∧ y ∨, y
• solo los operadores temporales X, U y R pueden aparecer.

Usando las equivalencias anteriores para la propagación de 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 hace explotar el tamaño de la fórmula. Esta forma normal es útil en la traducción de LTL a autómata Büchi .

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][10]

• 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.

La comprobación del modelo y el problema de satisfacción con una fórmula LTL es PSPACE-completo . La síntesis de LTL y el problema de la verificación de los juegos contra las condiciones ganadoras de LTL es 2EXPTIME-completo.[11]

Comprobación del modelo de lógica temporal lineal de la teoría 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 cumple con esta propiedad. Una técnica es obtener un autómata Büchi que sea equivalente al modelo y otro que sea equivalente a la negación de la propiedad. La intersección de los dos autómatas Büchi no deterministas está vacía si el modelo satisface la propiedad.[12]

Expresación de propiedades importantes en la verificación formal

Hay dos tipos principales de propiedades que pueden expresarse utilizando la lógica temporal lineal: las propiedades de seguridad generalmente indican que algo malo nunca sucede ( G ${\displaystyle \neg }$${\displaystyle \varphi }$ ), mientras que las propiedades de vitalidad indican que algo bueno sigue sucediendo ( GF ${\displaystyle \psi }$ o G ${\displaystyle (\varphi \rightarrow }$ F ${\displaystyle \psi )}$ ) En términos más generales, las propiedades de seguridad son aquellas para las cuales cada contraejemplo tiene un prefijo finito de tal manera que, aunque se extienda a una ruta infinita, siga siendo un contraejemplo. Para propiedades de vitalidad, por otro lado, cada prefijo finito de un contraejemplo puede extenderse a un camino infinito que satisfaga la fórmula.

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

• Lenguaje de acción

Enlaces externos

• Una presentación de LTL
• Lógica temporal de tiempo lineal y autómatas de Büchi
• Diapositivas de enseñanza LTL del profesor Alessandro Artale en la Universidad Libre de Bozen-Bolzano
• Algoritmos de traducción de LTL a Buchi una genealogía, desde el sitio web de Spot a library para la verificación de modelos.