Posteriormente, LTL a veces se llama lógica temporal proposicional, abreviada PTL.
entre una palabra y una fórmula LTL se define de la siguiente manera: Decimos que una ω-palabra satisface una fórmula LTL ψ cuando w
Los operadores lógicos adicionales se definen de la siguiente manera: Los operadores temporales adicionales R, F y G se definen de la siguiente manera: 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: El operador binario de liberación fuerte, denotado M, es el dual del hasta débil.
La semántica para los operadores temporales se presenta gráficamente de la siguiente manera.
Sea φ, ψ y ρ fórmulas LTL.
Esta forma normal es útil en la traducción de LTL a autómata Büchi .
La comprobación del modelo y el problema de satisfacción con una fórmula LTL es PSPACE-completo .
[11] La lógica temporal lineal paramétrica extiende LTL con variables en la modalidad "hasta".