The Community for Technology Leaders
Green Image
Issue No. 09 - September (1995 vol. 21)
ISSN: 0098-5589
pp: 768-775
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
383 ms
(Ver 3.1 (10032016))