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. 9, pp. 768-775, September 1995, doi:10.1109/32.464544