A really temporal logic

ABSTRACT

We introduce a temporal logic for the specification of real-time systems. Our logic, TPTL, employs a novel quantifier construct for referencing time: the freeze quantifier binds a variable to the time of the local temporal context. TPTL is both a natural language for specification and a suitable formalism for verification. We present a tableau-based decision procedure and a model-checking algorithm for TPTL. Several generalizations of TPTL are shown to be highly undecidable.

REFERENCES

• 1: Martín Abadi , Leslie Lamport, An Old-Fashioned Recipe for Real Time, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.1-27, June 03-07, 1991
• 2: ~ALUR, R., COURCOUBETtS, C., AND DILL, D. L. 1990. Model checking for real-time systems. In ~Proceedings of the 5th Annual Sympostum on Logic in Computer Science, IEEE Computer Society ~Press, New York, pp. 414-425.
• 3: Rajeev Alur , Tomás Feder , Thomas A. Henzinger, The benefits of relaxing punctuality, Proceedings of the tenth annual ACM symposium on Principles of distributed computing, p.139-152, August 19-21, 1991, Montreal, Quebec, Canada [doi>10.1145/112600.112613]
• 4: ~ALUR, R., AND HENZINGER, T. A. 1989. A really temporal logic. In Proceedings of the 30th ~Annual Symposium on Foundations of Computer Science. IEEE Computer Society Press, New ~York, pp. 164-169.
• 5: ~ALUR, R., AND HENZINGER, T. A. 1990. Real-time logics: Complexity and expressiveness. In ~Proceedings of the 5th Annual Symposium on Logic in Computer Science. IEEE Computer Society ~Press, New York, pp. 390-401.
• 6: Rajeev Alur , Thomas A. Henzinger, Logics and Models of Real Time: A Survey, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.74-106, June 03-07, 1991
• 7: Mordechai Ben-Ari , Zohar Manna , Amir Pnueli, The temporal logic of branching time, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.164-176, January 26-28, 1981, Williamsburg, Virginia [doi>10.1145/567532.567551]
• 8: Arthur Bernstein , Paul K. Harter, Jr., Proving real-time properties of programs with temporal logic, Proceedings of the eighth ACM symposium on Operating systems principles, p.1-11, December 14-16, 1981, Pacific Grove, California, United States
• 9: E. Allen Emerson , Aloysius K. Mok , A. Prasad Sistla , Jai Srinivasan, Quantitative Temporal Reasoning, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.136-145, June 18-21, 1990
• 10: Dov Gabbay , Amir Pnueli , Saharon Shelah , Jonathan Stavi, On the temporal analysis of fairness, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567462]
• 11: Joseph Y. Halpern, Presburger arithmetic with unary predicates is P¹1 complete, Journal of Symbolic Logic, v.56 n.2, p.637-642, June 1991 [doi>10.2307/2274706]
• 12: ~HAREL, E. 1988. Temporal analysis of real-time systems. Master's thesis, The Weizmann ~Institute of Science, Rehovot, Israel.
• 13: ~HAREL, E., LICHTENSTEIN, O., AND PNUELI, h. 1990. Explicit-clock temporal logic. In Proceedings ~of the 5th Annual Symposium on Logic in Computer Sctence. IEEE Computer Society Press, New ~York, pp. 402-413.
• 14: ~HAREL, D., PNUELI, h., AND STAVI, J. 1983. Propositional dynamic logic of regular programs. J. ~Comput. Syst. Sct., 26, 2, 222-243.
• 15: Tom Henzinger, Half-order modal logic: how to prove real-time properties, Proceedings of the ninth annual ACM symposium on Principles of distributed computing, p.281-296, August 22-24, 1990, Quebec City, Quebec, Canada [doi>10.1145/93385.93429]
• 16: Thomas A. Henzinger, The temporal specification and verification of real-time systems, Stanford University, Stanford, CA, 1992
• 17: Thomas A. Henzinger , Zohar Manna , Amir Pnueli, What Good Are Digital Clocks?, Proceedings of the 19th International Colloquium on Automata, Languages and Programming, p.545-558, July 13-17, 1992
• 18: John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 19: F Jahanian , A K Mok, Safety analysis of timing properties in real-time systems, IEEE Transactions on Software Engineering, v.12 n.9, p.890-904, Sept. 1986
• 20: Ron Koymans, Specifying real-time properties with metric temporal logic, Real-Time Systems, v.2 n.4, p.255-299, Nov. 1990 [doi>10.1007/BF01995674]
• 21: Orna Lichtenstein , Amir Pnueli, Checking that finite state concurrent programs satisfy their linear specification, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-107, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318622]
• 22: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 23: Zohar Manna , Pierre Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.68-93, Jan. 1984 [doi>10.1145/357233.357237]
• 24: Jonathan S. Ostroff, Temporal logic for real time systems, John Wiley & Sons, Inc., New York, NY, 1989
• 25: Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
• 26: PNUEU, A. 1977. The temporal logic of programs. In Proceedings of the 18th Annual Symposmm on Foundations of Computer Science. IEEE Computer Society Press, New York, pp. 46-57.
• 27: Amir Pnueli , Eyal Harel, Applications of temporal logic to the specification of real time systems (extended abstract), Proceedings of a Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.84-98, September 1988, Warwick, United Kingdom
• 28: ~PRATt, V. R. 1980. A near-optimal method for reasoning about action. J. Comput. Syst. Sci. 20, ~2, 231-254.
• 29: Hartley Rogers, Jr., Theory of recursive functions and effective computability, MIT Press, Cambridge, MA, 1987
• 30: A. P. Sistla , E. M. Clarke, The complexity of propositional linear temporal logics, Journal of the ACM (JACM), v.32 n.3, p.733-749, July 1985 [doi>10.1145/3828.3837]
• 31: ~SMULLYAN, R. M. 1968. First-Order Logic. Springer-Verlag, New York.
• 32: ~WANG, F., MOK, h. K., AND EMERSON, E. h. 1992. Asynchronous propositional temporal logic. ~In Proceedings of the 12th hzternatlonal Conference of Software Engmeenng.

INDEX TERMS

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

Additional Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Real-time and embedded systems

  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Complexity of proof procedures
  F.3 LOGICS AND MEANINGS OF PROGRAMS
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages
          Subjects: Decision problems

General Terms:
Theory, Verification

Keywords:
EXPSPACE-completeness, dense time, discrete time, linear-time temporal logic, model checking, real-time requirements