Temporal logic of actions

From Wikipedia, the free encyclopedia
Jump to: navigation, search


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[edit]

Statements in temporal logic are 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'*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 today, plus the value of x tomorrow times the value of y today, 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.

Editors[edit]

Some TLA+ editors include:

See also[edit]

References[edit]

External links[edit]