An interval logic for higher-level temporal reasoning

ABSTRACT

During the last several years, we have explored temporal logic as a framework for specifying and reasoning about concurrent programs, distributed systems, and communications protocols. Previous papers[Schwartz/Melliar-Smith81, 82, Vogt82a,b] report on our efforts using temporal reasoning primitives to express very high-level abstract requirements that a program or system is to satisfy. Based on our experiences with those primitives, we have developed an interval logic more suitable for expressing higher-level temporal properties.

REFERENCES

• 1: Bochmann, G.V., "Hardware Specification with Temporal Logic: An Example", IEEE Transactions on Computers, Vol C-31, No. 3, March 1982.
• 2: Hailpern, B., "Verifying Concurrent Processes Using Temporal Logic", Technical Report 195, Computer Systems Laboratory, Stanford Univ., August 1980.
• 3: David Harel, First-Order Dynamic Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1979
• 4: International Standards Organization, "Data Processing - Open Systems Interconnection - Basic Reference Model", ISO/DIS 7498, April 1982.
• 5: Leslie Lamport, TIMESETS -- A New Method for Temporal Reasoning about Programs, Logic of Programs, Workshop, p.177-196, May 01, 1981
• 6: Moszkowski, B., "A Temporal Logic for Multi-Level Reasoning about Hardware", Technical Report STAN-CS-82-952, Computer Science Dept., Stanford Univ., Dec. 1982.
• 7: Plaisted, D., "An Intermediate-Level Language for Obtaining Decision Procedures for a Class of Temporal Logics", Computer Science Laboratory, SRI, in preparation, June 1983.
• 8: Schwartz, R., P.M. Melliar-Smith, "Temporal Logic Specification of Distributed Systems", Proceedings of the IEEE Conference on Distributed Systems, April 1981.
• 9: Schwartz, R., P.M. Melliar-Smith, "From State Machines to Temporal Logic: Specification Methods for Protocol Standards", IEEE Transactions on Communications, Dec. 1982.
• 10: Seitz, C., "Ideas about Arbiters", Lambda, pp. 10-14, First Quarter, 1980.
• 11: Robert E. Shostak , Richard L. Schwartz , P. M. Melliar-Smith, STP: A Mechanized Logic for Specification and Verification, Proceedings of the 6th Conference on Automated Deduction, p.32-49, June 07-09, 1982
• 12: Vogt, F., "Entwurf eines Ereignisorientierten Modells zur Spezifikation von Verteilten Systemen Mittels Temporaler Logik", Ph.D. Dissertation, Technische Universität Wien, Austria, Feb. 1982.
• 13: Friedrich H. Vogt, Event-Based Temporal Logic Specifications of Services and Protocols, Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification, p.63-73, May 17-20, 1982
• 14: Wolper, P., "Synthesis of Communicating Processes from Temporal Logic Specifications", Report No. STAN-CS-82-925, Dept of Computer Science, Stanford University, August 1982.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Temporal logic

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

General Terms:
Theory