Lógica temporal lineal

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, uno puede codificar fórmulas sobre el futuro de los caminos, por ejemplo, una condición que eventualmente será verdadera, una condición que será verdadera hasta que otra de hecho se vuelva verdadera, etc. Es un fragmento del superconjunto más complejo CTL*, que además permite tiempo de ramificación y cuantificadores. Posteriormente, LTL a veces se llama lógica temporal proposicional, abreviada PTL.^[3]​ La lógica temporal lineal (LTL) es un fragmento de lógica de primer orden.^[4]​^[5]​

La LTL fue propuesta 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 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)

Semántica

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.

Equivalencias

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.

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 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 φ)

Negación forma normal

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 .

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]​^[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.

Problemas computacionales

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]​

Aplicaciones

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.

Extensiones

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

Véase también

• Lenguaje de acción

Referencias

1. Logic in Computer Science: Modelling and Reasoning about Systems: page 175
2. . Archivado desde el 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). Many-dimensional modal logics: theory and applications. Elsevier. p. 46. ISBN 978-0-444-50826-3. 
4. Diekert, Volker. «First-order Definable Languages». University of Stuttgart. 
5. (PhD). University of California Los Angeles. 1968.  Falta el |título= (ayuda)
6. Amir Pnueli, The temporal logic of programs. Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS), 1977, 46–57. doi 10.1109/SFCS.1977.32
7. Sec. 5.1 of Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press . Archivado desde el original el 4 de diciembre de 2010. Consultado el 17 de mayo de 2011. 
8. Sec. 5.1.5 "Weak Until, Release, and Positive Normal Form" of Principles of Model Checking.
9. Abramsky, Samson; Gavoille, Cyril; Kirchner, Claude; Spirakis, Paul (30 de junio de 2010). Automata, Languages and Programming: 37th International Colloquium, ICALP ... - Google Books. ISBN 9783642141614. Consultado el 30 de julio de 2014. 
10. Moshe Y. Vardi (2008). «From Church and Prior to PSL». En Orna Grumberg; Helmut Veith, eds. 25 years of model checking: history, achievements, perspectives. Springer. ISBN 978-3-540-69849-4.  preprint
11. «On the synthesis of a reactive module» (en inglés). 
12. Moshe Y. Vardi. An Automata-Theoretic Approach to Linear Temporal Logic. Proceedings of the 8th Banff Higher Order Workshop (Banff'94). Lecture Notes in Computer Science, vol. 1043, pp. 238--266, Springer-Verlag, 1996. ISBN 3-540-60915-6.
13. Chakraborty, Souymodip; Katoen, Joost-Pieter (2014). «Parametric LTL on Markov Chains». En Diaz, Josep, ed. Theoretical Computer Science. Lecture Notes in Computer Science (en inglés) (Springer Berlin Heidelberg) 7908: 207-221. Bibcode:2014arXiv1406.6683C. ISBN 978-3-662-44602-7. arXiv:1406.6683. doi:10.1007/978-3-662-44602-7_17. 

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
• una genealogía, desde el sitio web de Spot a library para la verificación de modelos.

•   Datos: Q98124076