Top Qs
Línea de tiempo
Chat
Contexto
Lógica temporal lineal
De Wikipedia, la enciclopedia libre
Remove ads
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]
Remove ads
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)
Remove ads
Semántica
Resumir
Contexto
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 2AP). Sea w = a0,a1,a2, ... una ω-palabra. Sea w(i) = ai . Sea wi = ai, ai+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 w1 ψ (en el próximo paso ψ debe ser verdadero)
- w φ U ψ si existe i ≥ 0 tal que wi ψ y para todo 0 ≤ k <i, w k φ (φ debe permanecer verdadero hasta (u) que ψ se convierte en verdadera)
Decimos que una ω-palabra 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 2AP, w ψ.
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.
Remove ads
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.
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 .
Remove ads
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.
Remove ads
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 ), mientras que las propiedades de vitalidad indican que algo bueno sigue sucediendo ( GF o G F ) 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.
Remove ads
Extensiones
La lógica temporal lineal paramétrica extiende LTL con variables en la modalidad "hasta".[13]
Véase también
Referencias
Wikiwand - on
Seamless Wikipedia browsing. On steroids.
Remove ads