The temporal logic of actions

ABSTRACT

The temporal logic of actions (TLA) is a logic for specifying and reasoning about concurrent systems. Systems and their properties are represented in the same logic, so the assertion that a system meets its specification and the assertion that one system implements another are both expressed by logical implication. TLA is very simple; its syntax and complete formal semantics are summarized in about a page. Yet, TLA is not just a logician's toy; it is extremely powerful, both in principle and in practice. This report introduces TLA and describes how it is used to specify and verify concurrent algorithms. The use of TLA to specify and reason about open systems will be described elsewhere.

REFERENCES

• 1: ABADI, M. AND LAMPORT, L. 1993. Conjoining specifications. Res. Rep. 118, Digital Equipment Corp., Systems Research Center, Palo Alto, Calif.
• 2: ABADI, M. AND LAMPORT, L. 1992. An old-fashioned recipe for real time. Research Report 91, Digital Equipment Corp., Systems Research Center, Palo Alto, Calif.~
• 3: Martín Abadi , Leslie Lamport, The existence of refinement mappings, Theoretical Computer Science, v.82 n.2, p.253-284, May 31, 1991 [doi>10.1016/0304-3975(91)90224-P]
• 4: ALPERN, B. AND SCHNEIDER, F. B. 1985. Defining liveness. Inf. Process. Lett. 21, 4 (Oct.), 181-185.
• 5: Krzysztof R. Apt, Ten Years of Hoare's Logic: A Survey—Part I, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.4, p.431-483, Oct. 1981 [doi>10.1145/357146.357150]
• 6: Krzysztof R. Apt , Ernst-Rüdiger Olderog, Verification of sequential and concurrent programs (2nd ed.), Springer-Verlag New York, Inc., Secaucus, NJ, 1997
• 7: ASHCROFT, E. A. 1975. }Proving assertions about parallel programs. J. Comput. Syst. Sci. 10, 110-135.
• 8: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 9: K. Mani Chandy, Parallel program design: a foundation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
• 10: DE BAKKER, J. W., HUIZING, C., DE ROEVER, W. P., AND ROZENBERG, G. (Eds.) 1992. Real-Time: Theory in Practice, Lecture Notes in Computer Science, vol. 600. Proceedings of a REX Real-Time Workshop, Springer-Verlag, Berlin.
• 11: Edsger W. Dijkstra, The structure of the “THE”-multiprogramming system, Communications of the ACM, v.11 n.5, p.341-346, May 1968 [doi>10.1145/363095.363143]
• 12: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 13: Urban Engberg , Peter Grønning , Leslie Lamport, Mechanical Verification of Concurrent Systems with TLA, Proceedings of the Fourth International Workshop on Computer Aided Verification, p.44-55, June 29-July 01, 1992
• 14: FLON, L. AND SUZUKI, N. 1978. Consistent and complete proof rules for the total correctness of parallel programs. In Proceedings of 19th Annual Symposium on Foundations of Computer Science. IEEE, New York, 184-192.
• 15: FLOYD, R. W. 1967. Assigning meanings to programs, in Proceedings of the Symposium on Applied Math. Vol. 19, American Mathematical Society, Providence, Rhode Island, 19-32.
• 16: S. J. Garland , J. V. Guttag, An overview of LP, the larch power, Proceedings of the 3rd international conference on Rewriting Techniques and Applications, p.137-151, January 1989
• 17: Eric C. R. Hehner, Predicative programming Part II, Communications of the ACM, v.27 n.2, p.144-151, Feb. 1984 [doi>10.1145/69610.357990]
• 18: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 19: Robert M. Keller, Formal verification of parallel programs, Communications of the ACM, v.19 n.7, p.371-384, July 1976 [doi>10.1145/360248.360251]
• 20: LAM, S. S. AND SHANKAR, A. U. 1984. Protocol verification via projections. IEEE Trans. Softw. Eng. SE-IO, 4 (July), 325-342.
• 21: Leslie Lamport, Hybrid Systems in TLA+, Hybrid Systems, p.77-102, January 1993
• 22: Leslie Lamport, Specifying Concurrent Program Modules, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.2, p.190-222, April 1983 [doi>10.1145/69624.357207]
• 23: LAMPORT, L. 1983b. What good is temporal logic. In Information Processing 83: Proceedings of the IFIP 9th World Congress, R. E. A. MASON, Ed. North-Holland, Amsterdam, 657-668.
• 24: LAMPORT, L. 1977. Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. SE-3, 2 (Mar.), 125-143.
• 25: LE~SENR~NG, A. C. 1969. Mathematical Logic and Hilbert's e-Symbol. Gordon and Breach, New York.
• 26: Richard J. Lipton, Reduction: a method of proving properties of parallel programs, Communications of the ACM, v.18 n.12, p.717-721, Dec. 1975 [doi>10.1145/361227.361234]
• 27: Nancy A. Lynch , Mark R. Tuttle, Hierarchical correctness proofs for distributed algorithms, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.137-151, August 10-12, 1987, Vancouver, British Columbia, Canada [doi>10.1145/41840.41852]
• 28: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 29: J. Misra, Specifying concurrent objects as communicating processes, Science of Computer Programming, v.14 n.2-3, p.159-184, Oct. 1990 [doi>10.1016/0167-6423(90)90019-A]
• 30: Susan Speer Owicki, Axiomatic proof techniques for parallel programs., 1975
• 31: Amir Pnueli, The Temporal Semantics of Concurrent Programs, Proceedings of the International Sympoisum on Semantics of Concurrent Computation, p.1-20, July 02-04, 1979
• 32: PNUELI, A. 1977. The temporal logic of programs. In Procee&ngs of the 18th Annual Symposium on the Foundations of Computer Science, IEEE, New York, 46-57.
• 33: SCHROEDER~ M. D., BIRRELL, A. D., BURROWS, M., MURRAY, H., NEED- HAM, R. M., RODEHEFFER, T. L., SATTERTHWAITE, E. H., AND THACKER, C. P. 1990. Autonet: A high-speed, self-configuring local area network using point-to-point links. Res. Rep. 59, Digital Equipment Corporation, Systems Research Center, Palo Alto, Calif.
• 34: SHANKAR, A. U. AND LAM, S. S. 1984. Time-dependent communication protocols. In Principles of Communication and Networking Protocols, S. S. LAM, Ed. IEEE Computer Society Press, Los Alamitos, Calif., 504- 519.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

General Terms:
Theory, Verification

Keywords:
concurrent programming, liveness properties, safety properties