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.
Statements in temporal logic of the form $[A]\_t$, 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 $x+x\text{'}$
★ y=y'. 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 $[A]\_t$ 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.
Some TLA+ editors include : Eclipse TLA+ Plugin, VisualTLA, TLA Editor, TLA# Plugin for Microsoft Visual Studio 2005

Contents

See also

External link

See also

★ Temporal logic

External link

★ TLA – The Temporal Logic of Actions