Temporal logic of actions
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 systems.
Details
Statements in temporal logic are of the form ![[A]_t](/2012-wikipedia_en_all_nopic_01_2012/I/be43a9bf5e1328a8d8ce7f33284b59ae.png)
, 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 
. 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 now, plus the value of x tomorrow times the value of y now, equals the value of y tomorrow.
The meaning of 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.
Editors
Some TLA+ editors include:
See also
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.
- Introduction to TLA, 16 December 1994, http://www.hpl.hp.com/techreports/Compaq-DEC/SRC-TN-1994-001.pdf, retrieved 2010-09-17