Comments on temporal logics for real-time system specification

ABSTRACT

The article “Temporal Logics for Real-Time System Specification” surveys some of the relevant literature dealing with the use of temporal logics for the specification of real-time systems. Unfortunately, it introduces some imprecisions that might create some confusion in the reader. While a certain degree of informality is certainly useful when addressing a broad audience, imprecisions can negatively impact the legibility of the exposition. We clarify some of its remarks on a few topics, in an effort to contribute to the usefulness of the survey for the reader.

REFERENCES

• 1: Rajeev Alur , Thomas A. Henzinger, Real-time logics: complexity and expressiveness, Information and Computation, v.104 n.1, p.35-77, May 1993 [doi>10.1006/inco.1993.1025]
• 2: Peter B. Andrews, An introduction to mathematical logic and type theory: to truth through proof, Academic Press Professional, Inc., San Diego, CA, 1986
• 3: P. Bellini , R. Mattolini , P. Nesi, Temporal logics for real-time system specification, ACM Computing Surveys (CSUR), v.32 n.1, p.12-42, March 2000 [doi>10.1145/349194.349197]
• 4: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 5: Miguel Felder , Angelo Morzenti, Validating real-time systems by history-checking TRIO specifications, ACM Transactions on Software Engineering and Methodology (TOSEM), v.3 n.4, p.308-339, Oct. 1994 [doi>10.1145/201024.201034]
• 6: Michael J. Fischer, Lambda-calculus schemata, Lisp and Symbolic Computation, v.6 n.3-4, p.259-288, Nov. 1993 [doi>10.1007/BF01019461]
• 7: Michael Fisher , Richard Owens, An Introduction to Executable Modal and Temporal Logics, Proceedings of the Workshop on Executable Modal and Temporal Logics, p.1-20, August 28, 1993
• 8: Furia, C. A., Pradella, M., and Rossi, M. 2008. Comments on ‘Temporal logics for real-time system specification.’ Tech. rep. 2008.7. DEI, Politecnico di Milano, Milan, Italy.
• 9: Dov M. Gabbay, The Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems, Temporal Logic in Specification, p.409-448, April 08-10, 1987
• 10: Dov M. Gabbay , Ian Hodkinson , Mark Reynolds, Temporal logic (vol. 1): mathematical foundations and computational aspects, Oxford University Press, Inc., New York, NY, 1994
• 11: 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]
• 12: Yoram Hirshfeld , Alexander Rabinovich, Future temporal logic needs infinitely many modalities, Information and Computation, v.187 n.2, p.196-208, 15 December 2003 [doi>10.1016/S0890-5401(03)00163-9]
• 13: Kamp, J. A. W. 1968. Tense logic and the theory of linear order. Ph.D. dissertation. University of California at Los Angeles, Los Angeles, CA.
• 14: 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]
• 15: Ron Koymans, (Real) Time: A Philosophical Perspective, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.353-370, June 03-07, 1991
• 16: Riccardo Mattolini , Paolo Nesi, An Interval Logic for Real-Time System Specification, IEEE Transactions on Software Engineering, v.27 n.3, p.208-227, March 2001 [doi>10.1109/32.910858]
• 17: Ben Moszkowski, Executing temporal logic programs, Cambridge University Press, New York, NY, 1986
• 18: Prabhakar, P. and D'Souza, D. 2006. On the expressiveness of MTL with past operators. In Proceedings of FORMATS'06. Lecture Notes in Computer Science, vol. 4202. Springer, Berlin, Germany, 322--336.
• 19: Wolper, P. 1983. Temporal logic can be more expressive. Inform. Contr. 56, 1, 72--99.

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:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages

General Terms:
Languages

Keywords:
Temporal logic