Temporal Logic of Actions
Encyclopedia
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
.
, 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.
include:
Leslie Lamport
Leslie Lamport is an American computer scientist. A graduate of the Bronx High School of Science, he received a B.S. in mathematics from the Massachusetts Institute of Technology in 1960, and M.A. and Ph.D. degrees in mathematics from Brandeis University, respectively in 1963 and 1972...
, which combines temporal logic
Temporal logic
In logic, the term temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. In a temporal logic we can then express statements like "I am always hungry", "I will eventually be hungry", or "I will be hungry...
with a logic of actions.
It is used to describe behaviours of concurrent systems
Concurrency (computer science)
In computer science, concurrency is a property of systems in which several computations are executing simultaneously, and potentially interacting with each other...
.
Details
Statements in temporal logic are of the form, 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+ editorsVisual editor
Visual editors or full screen editors are editing programs which display the text being edited on the screen as it is being edited, as opposed to line-oriented editors ....
include: