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. Please help improve this article by introducing more precise citations. (January 2011) (Learn how and when to remove this message)

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 and distributed systems. It is the logic underlying the specification language TLA+.