Un sistema formal para expresar proposiciones sobre el orden temporal y las propiedades de estados a lo largo de puntos o intervalos temporales, utilizando operadores temporales como 'G' (globalmente), 'F' (finalmente), 'X' (siguiente) y 'U' (hasta).

Principio

Ampliar lenguajes proposicionales o de predicados con modalidades temporales interpretadas sobre un modelo del tiempo (lineal o ramificado) de modo que las fórmulas describan cómo las verdades persisten, ocurren eventualmente o se relacionan a través de la sucesión temporal.

Demostración

Al especificar un programa concurrente, la fórmula temporal G(request -> F grant) afirma que en cada línea de ejecución, cuando ocurre una petición, finalmente viene seguida de una concesión; los model checkers utilizan tales fórmulas para verificar trazas del sistema frente a la especificación.

Aplicación incorrecta

Usar una fórmula temporal de tiempo lineal para afirmar propiedades de comportamientos ramificados (por ejemplo, asumir que Fφ en una línea implica Fφ en todos los futuros) o confundir modalidades temporales con restricciones temporales métricas sin relojes ni duraciones.

Consecuencia

El uso adecuado de la lógica temporal produce especificaciones precisas de propiedades de vivacidad, seguridad y equidad en el tiempo y facilita la verificación automática al traducir el comportamiento en modelos temporales verificables.

Inversión

El reverso es la lógica atemporal donde las proposiciones se evalúan sin estructura temporal y no pueden expresar orden ni eventualidad; las relaciones temporales se reducen a valores de verdad ordinarios en un único estado estático.

Límite

La lógica temporal, en su definición estándar, no codifica de forma intrínseca tiempo métrico real (a menos que se extienda a lógicas temporales en tiempo real) ni modela probabilidades; presupone una estructura temporal escogida (discreta/continua, lineal/ramificada) que limita la expresividad.

Tensión semántica

Existe tensión entre las interpretaciones lineal y ramificada: LTL evalúa fórmulas sobre líneas temporales únicas, mientras que las lógicas ramificadas (CTL, CTL*) permiten la cuantificación sobre caminos; la elección afecta las propiedades que pueden expresarse y verificarse.

Síntesis

La lógica temporal proporciona un lenguaje y semántica para expresar cómo las propiedades evolucionan o se mantienen en el tiempo añadiendo operadores temporales a las lógicas estándar, lo que permite razonar formalmente sobre secuencias y patrones de estados en sistemas y procesos.