Temporal logic of actions
This article includes a list of references, related reading or external links, but its sources remain unclear because it lacks inline citations. (January 2011) (Learn how and when to remove this template message)
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 today, plus the value of x tomorrow times the value of y today, 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.
- Lamport, Leslie (2002). Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley. ISBN 0-321-14306-X. Retrieved 2007-02-02.
- Leslie Lamport (16 December 1994), Introduction to TLA (PDF), retrieved 2010-09-17
- Official website
- "TLA+ Proof System". INRIA.
- Lamport, Leslie (2014). "Thinking for Programmers".
A gentle intro to TLA+ at Build
|This formal methods-related article is a stub. You can help Wikipedia by expanding it.|