Temporal logic of actions: Difference between revisions
m +zh |
|||
Line 24: | Line 24: | ||
[[de:Temporale Logik der Aktionen]] |
[[de:Temporale Logik der Aktionen]] |
||
[[zh:动作的时间逻辑]] |
Revision as of 17:47, 21 May 2010
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 , 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.
Some TLA+ editors include : Eclipse TLA+ Plugin, VisualTLA, TLA Editor, TLA# Plugin for Microsoft Visual Studio 2005