El artículo técnico analiza la capacidad del lenguaje de especificación TLA+ para expresar propiedades de alcanzabilidad y posibilidad, un tema que suele generar confusión debido a la naturaleza lineal de su lógica frente a la lógica de tiempo ramificado. El texto explica que, aunque TLA+ no permite expresar directamente la propiedad de que un estado es alcanzable desde cualquier preámbulo de comportamiento, existen mecanismos para validarlas. Se detalla el operador ENABLED, que verifica la posibilidad de tomar una acción inmediata, y la notación de Lamport para expresar la alcanzabilidad en múltiples pasos, aunque esta última no es verificable directamente por el verificador TLC en su versión actual.
El artículo destaca que TLC ha implementado recientemente soporte para propiedades de posibilidad básicas mediante la etiqueta _POSSIBLE P, que actúa como una prueba de unidad para el modelo. Además, se describe el algoritmo de alcanzabilidad hacia atrás, una técnica que permite verificar si un estado objetivo es accesible desde cualquier estado del sistema mediante una búsqueda en anchura inversa. Finalmente, se explica cómo las suposiciones de equidad (fairness assumptions) permiten simular razonamiento de tiempo ramificado dentro de la lógica lineal de TLA+, permitiendo definir comportamientos que evitan estados de bloqueo y garantizan la progresión del sistema hacia estados deseados, integrando así la verificación de liveness properties en el framework de TLA+.