Issue No. 09 - September (1995 vol. 21)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.464544
Predicate-action diagrams, which are similar to standard state-transition diagrams, are precisely defined as formulas of TLA (the Temporal Logic of Actions). We explain how these diagrams can be used to describe aspects of a specification—and those descriptions then proved correct—even when the complete specification cannot be written as a diagram. We also use the diagrams to illustrate proofs.
Concurrency, specification, state-transition diagrams, temporal logic.
Leslie Lamport, "TLA in Pictures", IEEE Transactions on Software Engineering, vol. 21, no. , pp. 768-775, September 1995, doi:10.1109/32.464544