This Article 
 Bibliographic References 
 Add to: 
TLA in Pictures
September 1995 (vol. 21 no. 9)
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.

[1] G.H. Mealy,“A method for synthesizing sequential circuits,” Bell System Technical J., vol. 34, pp. 1,045-1,079, Sept. 1955.
[2] E.F. Moore,“Gedanken-experiments on sequential machines,” C.E. Shannon and J. McCarthy, eds., Automata Studies, pp. 129-153.Princeton, N.J.: Princeton Univ. Press, 1956.
[3] L. Lamport and S. Owicki, "The Temporal Logic of Actions," ACM Trans. Programming Languages and Systems, vol. 16, pp. 872-923, May 994.
[4] B. Alpern and F.B. Schneider,“Defining liveness,” Information Processing Letters, vol. 21, pp. 181-185, Oct. 1985.
[5] C. Mead and L. Conway, Introduction to VLSI Systems, Addison-Wesley, Reading, Mass., 1980.
[6] M. Abadi and L. Lamport, "Conjoining Specifications," ACM Trans. Programming Languages and Systems, Vol. 17, No. 3, May 1995, pp. 507-534.

Index Terms:
Concurrency, specification, state-transition diagrams, temporal logic.
Leslie Lamport, "TLA in Pictures," IEEE Transactions on Software Engineering, vol. 21, no. 9, pp. 768-775, Sept. 1995, doi:10.1109/32.464544
Usage of this product signifies your acceptance of the Terms of Use.