La lógica temporal de acciones ( TLA ) es una lógica desarrollada por Leslie Lamport , que combina la lógica temporal con una lógica de acciones . Se utiliza para describir comportamientos de sistemas concurrentes .
Detalles
Los enunciados en la lógica temporal de las acciones tienen la forma , En 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 primarias y no primarias, como. El significado de las variables no primarias es el valor de la variable en este estado . El significado de las variables primarias 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álido 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.
Ver también
Referencias
- Lamport, Leslie (2002). Especificación de sistemas: el lenguaje y las herramientas TLA + para ingenieros de hardware y software . Addison-Wesley. ISBN 0-321-14306-X. Consultado el 2 de febrero de 2007 .
- Leslie Lamport (16 de diciembre de 1994), Introducción a TLA (PDF) , consultado el 17 de septiembre de 2010
enlaces externos
- Página web oficial
- "Sistema de prueba TLA +" . INRIA .
- Lamport, Leslie (2014). "Pensamiento para programadores" .
Una suave introducción a TLA + en Build