Temporal logic of actions

Short description: Logic used to describe behaviours of concurrent systems.

Temporal logic of actions (TLA) is a logic developed by Leslie Lamport, which combines temporal logic with a logic of actions. It is used to describe behaviours of concurrent and distributed systems. It is the logic underlying the specification language TLA+.

Details

Statements in the temporal logic of actions are of the form [math]\displaystyle{ [A]_t }[/math], where A is an action and t contains a subset of the variables appearing in A. An action is an expression containing primed and non-primed variables, such as [math]\displaystyle{ x+x'*y=y' }[/math]. The meaning of the non-primed variables is the variable's value in this state. The meaning of primed variables is the variable's value in the next state. The above expression means the value of x today, plus the value of x tomorrow times the value of y today, equals the value of y tomorrow.

The meaning of [math]\displaystyle{ [A]_t }[/math] is that either A is valid now, or the variables appearing in t do not change. This allows for stuttering steps, in which none of the program variables change their values.

See also

• Temporal logic
• PlusCal
• TLA+

References

• Lamport, Leslie (2002). Specifying Systems: The TLA⁺ Language and Tools for Hardware and Software Engineers. Addison-Wesley. ISBN 0-321-14306-X. http://research.microsoft.com/users/lamport/tla/book.html. Retrieved 2007-02-02. 
• Leslie Lamport (16 December 1994), Introduction to TLA, https://www.hpl.hp.com/techreports/Compaq-DEC/SRC-TN-1994-001.pdf, retrieved 2010-09-17 

External links

• "TLA+ Proof System". INRIA. https://tla.msr-inria.inria.fr/tlaps/content/Home.html. 
• Lamport, Leslie (2014). "Thinking for Programmers". http://channel9.msdn.com/Events/Build/2014/3-642. "A gentle intro to TLA+ at Build"