La lógica temporal de acciones ( TLA ) es una lógica desarrollada por Leslie Lamport , que combina una lógica temporal con una lógica de acciones . Se utiliza para describir comportamientos de sistemas concurrentes y distribuidos . Es la lógica subyacente al lenguaje de especificación TLA+ .
Las declaraciones en la lógica temporal de las acciones tienen la forma , donde A es una acción y t contiene un subconjunto de las variables que aparecen en A . Una acción es una expresión que contiene variables primadas y no primadas, como . El significado de las variables no primadas es el valor de la variable en este estado . El significado de las variables primadas es el valor de la variable en el siguiente estado . La expresión anterior significa que el valor de x hoy , más el valor de x mañana multiplicado por el valor de y hoy , es igual al valor de y mañana .
El significado de es que A es válida ahora o las variables que aparecen en t no cambian. Esto permite pasos entrecortados, en los que ninguna de las variables del programa cambia sus valores.
![{\displaystyle [A]_{t}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/03d6eaf7fc064571a2d2e88332f923d25a436f1c)
