Abstract
We summarize and reorganize some of the last decade's research on real-time extensions of temporal logic. Our main focus is on tableau constructions for model checking linear temporal formulas with timing constraints. In particular, we find that a great deal of real-time verification can be performed in polynomial space, but also that considerable care must be exercised in order to keep the real-time verification problem in polynomial space, or even decidable.
This research was supported in part by the Office of Naval Research Young Investigator award N00014-95-1-0520, by the National Science Foundation CAREER award CCR-9501708, by the National Science Foundation grant CCR-9504469, by the Defense Advanced Research Projects Agency grant NAG2-1214, by the Army Research Office MURI grant DAAH-04-96-1-0341, and by the Semiconductor Research Corporation contract 97-DC-324.041.
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, C. Courcoubetis, and D.L. Dill. Model checking in dense real time. Information and Computation, 104(1):2–34, 1993.
R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.
R. Alur, L. Fix, and T.A. Henzinger. A determinizable class of timed automata. In D.L. Dill, editor, CAV 94: Computer-aided Verification, Lecture Notes in Computer Science 818, pages 1–13. Springer-Verlag, 1994.
R. Alur, T. Feder, and T.A. Henzinger. The benefits of relaxing punctuality. Journal of the ACM, 43(1):116–146, 1996.
R. Alur and T.A. Henzinger. Back to the future: towards a theory of timed regular languages. In Proceedings of the 33rd Annual Symposium on Foundations of Computer Science, pages 177–186. IEEE Computer Society Press, 1992.
R. Alur and T.A. Henzinger. Logics and models of real time: a survey. In J.W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice, Lecture Notes in Computer Science 600, pages 74–106. Springer-Verlag, 1992.
R. Alur and T.A. Henzinger. Real-time logics: complexity and expressiveness. Information and Computation, 104(1):35–77, 1993.
R. Alur and T.A. Henzinger. A really temporal logic. Journal of the ACM, 41(1):181–204, 1994.
H. Barringer, R. Kuiper, and A. Pnueli. A really abstract concurrent model and its temporal logic. In Proceedings of the 13th Annual Symposium on Principles of Programming Languages, pages 173–183. ACM Press, 1986.
J.R. Büchi. On a decision method in restricted second-order arithmetic. In E. Nagel, P. Suppes, and A. Tarski, editors, Proceedings of the First International Congress on Logic, Methodology, and Philosophy of Science 1960, pages 1–11. Stanford University Press, 1962.
E.M. Clarke and R.P. Kurshan. Computer-aided verification. IEEE Spectrum, 33(6):61–67, 1996.
E.A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 995–1072. Elsevier Science Publishers, 1990.
E.A. Emerson. Real time and the Μ-calculus. In J.W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice, Lecture Notes in Computer Science 600, pages 176–194. Springer-Verlag, 1992.
E.A. Emerson, A.K. Mok, A.P. Sistla, and J. Srinivasan. Quantitative temporal reasoning. In R.P. Kurshan and E.M. Clarke, editors, CAV 90: Computer-aided Verification, Lecture Notes in Computer Science 531, pages 136–145. Springer-Verlag, 1990.
D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In Proceedings of the Seventh Annual Symposium on Principles of Programming Languages, pages 163–173. ACM Press, 1980.
T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193–244, 1994.
T.A. Henzinger, J.-F. Raskin, and P.-Y. Schobbens. The regular real-time languages. In ICALP 97: Automata, Languages, and Programming, Lecture Notes in Computer Science. Springer-Verlag, 1998.
R. Koymans. Specifying real-time properties with metric temporal logic. Real-time Systems, 2(4):255–299, 1990.
O. Lichtenstein and A. Pnueli. Checking that finite-state concurrent programs satisfy their linear specification. In Proceedings of the 12th Annual Symposium on Principles of Programming Languages, pages 97–107. ACM Press, 1985.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
J.-F. Raskin. Personal communication, 1998.
J.-F. Raskin and P.-Y. Schobbens. State-clock logic: a decidable real-time logic. In O. Maler, editor, HART 97: Hybrid and Real-time Systems, Lecture Notes in Computer Science 1201, pages 33–47. Springer-Verlag, 1997.
S. Safra. On the complexity of Ω-automata. In Proceedings of the 29th Annual Symposium on Foundations of Computer Science, pages 319–327. IEEE Computer Society Press, 1988.
W.J. Savitch. Relationship between nondeterministic and deterministic tape classes. Journal of Computer and System Sciences, 4:177–194, 1970.
A.P. Sistla and E.M. Clarke. The complexity of propositional linear temporal logics. Journal of the ACM, 32(3):733–749, 1985.
A.P. Sistla. Theoretical Issues in the Design and Verification of Distributed Systems. PhD thesis, Harvard University, 1983.
W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 133–191. Elsevier Science Publishers, 1990.
M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1–37, 1994.
T. Wilke. Specifying timed state sequences in powerful decidable logics and timed automata. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, FTRTFT 94: Formal Techniques in Real-time and Fault-tolerant Systems, Lecture Notes in Computer Science 863, pages 694–715. Springer-Verlag, 1994.
P. Wolper. Synthesis of Communicating Processes from Temporal-Logic Specifications. PhD thesis, Stanford University, 1982.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Henzinger, T.A. (1998). It's about time: Real-time logics reviewed. In: Sangiorgi, D., de Simone, R. (eds) CONCUR'98 Concurrency Theory. CONCUR 1998. Lecture Notes in Computer Science, vol 1466. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055640
Download citation
DOI: https://doi.org/10.1007/BFb0055640
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64896-3
Online ISBN: 978-3-540-68455-8
eBook Packages: Springer Book Archive