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.

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 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.

gollark: Also, it might be neat to make a maze or something. You could even incorporate nether portals and stuff for more twistiness.
gollark: The standard is 9x9.
gollark: Yes. Destroy it. Remove it from the skybox.
gollark: I wonder if we actually could find some way to turn off the sun/moon after it's lased.
gollark: Are you going to help with my moon-shot program, then?

See also

References
  • 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
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.