TLA+ (Lógica Temporal de Acciones) modela un sistema como un conjunto de comportamientos, cada comportamiento siendo una secuencia de estados. Usando operadores temporales, puede expresar invariantes (por ejemplo, []P significando que P se mantiene en cada estado) y propiedades de acción tales como [](x' >= x) (el nuevo valor de x siempre es al menos el antiguo valor). Las propiedades de vitalidad, que afirman que 'algo bueno siempre sucede,' se construyen a partir del operador <>; ejemplos incluyen <>[]P (eventualmente P permanece verdadero para siempre) y P ~> Q (P lleva a Q). Estas propiedades se evalúan en todos los posibles comportamientos, asegurando que se mantengan universalmente.
Una limitación fundamental es que TLA+ no puede expresar propiedades que requieren cuantificación existencial sobre comportamientos. Por ejemplo, propiedades de alcance como 'existe un comportamiento donde P es verdadero' — necesarias para demostrar que un juego es ganable — están fuera del alcance del lenguaje. Del mismo modo, TLA+ no puede expresar hiperpropiedades, que son propiedades sobre conjuntos de comportamientos; un ejemplo es verificar que un modo de ahorro de energía siempre use menos energía que el modo normal en todas las secuencias posibles de acciones, lo que requeriría comparar dos comportamientos distintos.
Aunque existen soluciones alternativas — como usar variables auxiliares para almacenar un historial de estado, emplear auto‑composición para modelar múltiples comportamientos, o aprovechar la palabra clave REACHABLE y TLCGet en el verificador de modelo TLC — presentan serios inconvenientes. Las variables auxiliares complican las refinaciones, la auto‑composición causa una explosión exponencial del espacio de estados, y estas técnicas a menudo producen modelos que parecen desordenados y ya no corresponden directamente al sistema real. Otras herramientas como CTL o PRISM pueden manejar algunas de estas propiedades pero sacrifican al ser más débiles en las verificaciones de seguridad y vitalidad donde TLA+ destaca.