This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
TLA in Pictures
September 1995 (vol. 21 no. 9)
pp. 768-775
ASCII Text
x 
 
Leslie Lamport, "TLA in Pictures," IEEE Transactions on Software Engineering, vol. 21, no. 9, pp. 768-775, September, 1995.
 
 
BibTex
x
 
@article{ 10.1109/32.464544,
author = {Leslie Lamport},
title = {TLA in Pictures},
journal ={IEEE Transactions on Software Engineering},
volume = {21},
number = {9},
issn = {0098-5589},
year = {1995},
pages = {768-775},
doi = {http://doi.ieeecomputersociety.org/10.1109/32.464544},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Software Engineering
TI - TLA in Pictures
IS - 9
SN - 0098-5589
SP768
EP775
EPD - 768-775
A1 - Leslie Lamport,
PY - 1995
KW - Concurrency
KW - specification
KW - state-transition diagrams
KW - temporal logic.
VL - 21
JA - IEEE Transactions on Software Engineering
ER -
 
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.
Citation:
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.