Curso completo de Lógica Temporal LTL
La lógica temporal lineal describe lo que vale ahora, siempre, eventualmente o en el siguiente instante. Es una herramienta muy natural para sistemas reactivos, protocolos y procesos en evolución.
Por qué importa
Permite expresar especificaciones como “algo nunca debe pasar”, “algo terminará pasando” o “si ocurre un evento, luego vendrá otro”.
Objetivos de aprendizaje
- Dominar G, F y X.
- Distinguir propiedades de seguridad y de vivacidad.
- Leer ejemplos de persistencia temporal.
- Entender el alcance actual del operador U en el motor.
Accesos rápidos
Panorama del curso
Esta guía reúne la cobertura completa del perfil: conceptos, operadores, comandos, ejemplos largos, límites reales del motor y un script integral descargable para seguir probando fuera de la página. Los bloques de código se pueden ejecutar inline y abrir en el editor desplegable para probar variaciones sin salir de la documentación.
Capacidades nuevas de este perfil
- explain clasifica patrones LTL estándar como safety, liveness, response, persistence, recurrence y precedence.
- El frame temporal y la intuición de irreversibilidad del futuro aparecen explícitos en la salida.
- Las trazas del tableau ayudan a mostrar por qué “eventualmente” no equivale a “siempre”.
Patrones temporales reconocidos
Response y contramodelo temporal en un mismo flujo.
logic temporal.ltl
set verbose = on
explain [](P -> <>Q)
countermodel (<>P -> []P)Cobertura exacta del perfil
LTL cubre G/F, next, until, dualidades, frame tipo S4 y seis patrones temporales nombrados por el runtime.
Operadores y aliases temporales
El parser acepta las formas textuales y luego las renderiza como `G`, `F`, `X` y `U`.
- `[](P)` / `G(P)` para siempre
- `<>(P)` / `F(P)` para eventualmente
- `next P` / `X(P)` para siguiente estado
- `P until Q` / `P U Q` para hasta que
- Dualidades `F(P) ≡ !G(!P)` y `G(P) ≡ !F(!P)`
Fórmulas base del perfil temporal
Estas líneas cubren los axiomas y contraejemplos temporales más importantes del motor.
logic temporal.ltl
set verbose = on
check valid ([]P -> P)
check valid ([]P -> <>P)
check valid ([]P -> []([]P))
check valid ([](P -> Q) -> ([]P -> [](Q)))
check valid ([]P -> next P)
check valid (<>P -> []P)
check equivalent <>(P), 
check equivalent [](P), !<>(!P)
check satisfiable (next P)
check satisfiable (P until Q)
countermodel (<>P -> []P)
countermodel (next P -> P)Los seis patrones temporales reconocidos
La clasificación temporal no debe quedar implícita; aquí están las seis familias que hoy detecta `classifyTemporalPattern()`.
logic temporal.ltl
explain [](!P)
explain <>(P)
explain [](P -> <>Q)
explain <>[](P)
explain []<>(P)
explain (!P until Q)Eso cubre Safety, Liveness, Response, Persistence, Recurrence y Precedence.
Conceptos fundamentales
1. Siempre
G(P) o [](P) indica que P vale en todos los estados futuros relevantes.
2. Eventualmente
F(P) o <>(P) indica que P ocurre en algún estado futuro.
3. Siguiente
X(P) afirma que P vale en el próximo paso.
4. Frames temporales
ST usa un frame reflexivo-transitivo para G y F, con expansión específica para X.
Operadores y formas expresivas
[](P)Siempre / G
P vale globalmente.
logic temporal.ltl
check valid [](P) -> P<>(P)Eventualmente / F
P ocurre alguna vez.
logic temporal.ltl
check valid [](P) -> <>(P)X(P)Siguiente
P vale en el siguiente instante.
logic temporal.ltl
check satisfiable X(P)Comandos que debes dominar
Ley básica de G
Si algo siempre vale, entonces vale ahora.
logic temporal.ltl
check valid [](P) -> PG implica F
Lo que siempre vale también ocurre eventualmente.
logic temporal.ltl
check valid [](P) -> <>(P)F no implica G
Lo eventual no basta para garantizar permanencia.
logic temporal.ltl
check valid <>(P) -> [](P)
countermodel <>(P) -> [](P)ST como herramienta pedagógica en esta lógica
Esta sección no solo enseña la lógica, sino también cómo usar `ST` para explicarla mejor: con aliases semánticos, funciones reutilizables, condicionales, recorridos guiados y salidas legibles para clase, taller o autoestudio.
Seguridad y vivacidad en formato de aula
Nombrar propiedades temporales vuelve mucho más clara la distinción entre “siempre” y “alguna vez”.
logic temporal.ltl
let seguridad = "Si algo siempre vale, vale ahora" : ([]P -> P)
let vivacidad = "Si algo siempre vale, eventualmente ocurre" : ([]P -> <>P)
fn revisarTemporal(F) {
explain F
return F
}
revisarTemporal(seguridad)
revisarTemporal(vivacidad)
if valid ([]P -> P) {
print "la propiedad de seguridad está activa"
}Recorrido de operadores temporales
Usa un bucle corto para recorrer las formas expresivas básicas del perfil temporal.
logic temporal.ltl
for Caso in { [](P), <>(P), X(P) } {
explain Caso
}
if valid <>(P) -> [](P) {
print "eventualmente implicaría siempre"
} else {
print "vivacidad no equivale a permanencia"
}Lecciones prácticas largas
Dualidades temporales
Reescrituras fundamentales entre siempre y eventualmente.
logic temporal.ltl
check equivalent <>(P), 
check equivalent [](P), !<>(!P)Propagación temporal
Cierre de una regla siempre válida sobre un hecho siempre válido.
logic temporal.ltl
axiom regla : []((P -> Q))
axiom hecho = [](P)
derive [](Q) from {regla, hecho}Errores frecuentes al estudiar esta lógica
- Confundir eventualmente con ahora.
- Leer X(P) como repetición de P presente.
- Confiar demasiado en until sin revisar la limitación actual del motor.
Límites del motor y advertencias
- El tableau temporal comparte límite de 200 nodos.
- El operador U tiene soporte parcial en el motor actual.
Cómo conecta con otras lógicas
- Conecta con verificación de software y protocolos.
- Se apoya en intuiciones modales pero con lectura temporal específica.