The temporal logic of actions
The work
| Authors | Leslie Lamport |
|---|---|
| Editors | |
| Type | article |
| Year | 1994 |
| Citekey | lamport1994temporal |
Where it appeared
| Published in | ACM Transactions on Programming Languages and Systems |
|---|---|
| Publisher | Association for Computing Machinery |
| Volume | 16 |
| Issue | 3 |
| Pages | 872--923 |
Identifiers
| DOI | 10.1145/177492.177726 |
|---|---|
| OpenAlex | W79592965 |
Access
| Landing page | https://doi.org/10.1145/177492.177726 |
|---|
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
The temporal logic of actions (TLA) is a logic for specifying and reasoning about concurrent systems. Systems and their properties are represented in the same logic, so the assertion that a system meets its specification and the assertion that one system implements another are both expressed by logical implication. TLA is very simple; its syntax and complete formal semantics are summarized in about a page. Yet, TLA is not just a logician's toy; it is extremely powerful, both in principle and in practice. This report introduces TLA and describes how it is used to specify and verify concurrent algorithms. The use of TLA to specify and reason about open systems will be described elsewhere.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-23 22:13 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@article{lamport1994temporal,
title = {The temporal logic of actions},
author = {Leslie Lamport},
year = {1994},
journal = {ACM Transactions on Programming Languages and Systems},
publisher = {Association for Computing Machinery},
volume = {16},
number = {3},
pages = {872--923},
doi = {10.1145/177492.177726},
}
This record lives at https://refs.drheap.org/lamport1994temporal/ and will keep doing so.