Skip to main content
SpringerLink
Log in

From quantity to quality

  • Conference paper
  • First Online:
Hybrid and Real-Time Systems (HART 1997)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1201))

Included in the following conference series:

Abstract

In temporal-logic model checking, we verify the correctness of a program with respect to a desired behavior by checking whether a structure that models the program satisfies a temporal-logic formula that specifies the behavior. The model-checking problem for the branching-time temporal logic CTL can be solved in linear running time, and model-checking tools for CTL are used successfully in industrial applications. The development of programs that must meet rigid real-time constraints has brought with it a need for real-time temporal logics that enable quantitative reference to time. Early research on real-time temporal logics uses the discrete domain of the integers to model time. Present research on real-time temporal logics focuses on continuous time and uses the dense domain of the reals to model time. There, model checking becomes significantly more complicated. For example, the model-checking problem for TCTL, a continuous-time extension of the logic CTL, is PSPACE-complete.

In this paper we suggest a reduction from TCTL model checking to CTL model checking. The contribution of such a reduction is twofold. Theoretically, while it has long been known that model-checking methods for untimed temporal logics can be extended quite easily to handle discrete time, it was not clear whether and how untimed methods can handle the reset quantifier of TCTL, which resets a realvalued clock. Practically, our reduction enables anyone who has a tool for CTL model checking to use it for TCTL model checking. The TCTL model-checking algorithm that follows from our reduction is in PSPACE, matching the known bound for this problem. In addition, it enjoys the wide distribution of CTL model-checking tools and the extensive and fruitful research efforts and heuristics that have been put into these tools.

This research was supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA grant NAG2-892, and by the SRC contract 95-DC-324.036.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2–34, May 1993.

    Google Scholar 

  2. R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183–236, 1994.

    Google Scholar 

  3. 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. 1992.

    Google Scholar 

  4. R. Alur and T. Henzinger. Real-time logics: Complexity and expressiveness. Information and Computation, 104(1):35–77, May 1993.

    Google Scholar 

  5. R. Alur and T.A. Henzinger. A really temporal logic. Journal of the ACM, 41(1):181–204, 1994.

    Google Scholar 

  6. R.K. Brayton, G.D. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S.-T. Cheng, S. Edwards, S. Khatri, T. Kukimoto, A. Pardo, S. Qadeer, R.K. Ranjan, S. Sarwary, T.R. Shiple, G. Swamy, and T. Villa. VIS: a system for verification and synthesis. In Computer Aided Verification, Proc. 8th Int. Workshop, volume 1102 of Lecture Notes in Computer Science, pages 428–432. Springer-Verlag, 1996.

    Google Scholar 

  7. O. Bernholtz, M.Y. Vardi, and P. Wolper. An automatatheoretic approach to branching-time model checking. In Computer Aided Verification, Proc. 6th Int. Conference, volume 818 of Lecture Notes in Computer Science, pages 142–155, 1994.

    Google Scholar 

  8. S. Campos, E.M. Clarke, W. Marrero, M. Minea, and H. Hiraishi. Computing quantitative characteristics of finite-state real-time systems. In Proceedings of the 15th Annual Real-time Systems Symposium. IEEE Computer Society Press, 1994.

    Google Scholar 

  9. E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. Workshop on Logic of Programs, volume 131 of Lecture Notes in Computer Science, pages 52–71. Springer-Verlag, 1981.

    Google Scholar 

  10. E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, January 1986.

    Google Scholar 

  11. E.M. Clarke, O. Grumberg, and D. Long. Verification tools for finite-state concurrent systems. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Decade of Concurrency — Reflections and Perspectives (Proceedings of REX School), Lecture Notes in Computer Science, pages 124–175. Springer-Verlag, 1993.

    Google Scholar 

  12. E.A. Emerson, A.K. Mok, A.P. Sistla, and J. Srinivasan. Quantitative temporal reasoning. In Proc. 2nd Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science, pages 136–145. Springer-Verlag, 1990.

    Google Scholar 

  13. J.-C. Fernandez, H. Garavel, A. Kerbrat, L. Mounier, R. Mateescu, and M. Sighireanu. CADP: a protocol validitation and verification toolbox. In Computer Aided Verification, Proc. 8th Int. Workshop, volume 1102 of Lecture Notes in Computer Science, pages 437–440. Springer-Verlag, 1996.

    Google Scholar 

  14. T.A. Henzinger. Hybrid automata with finite bisimulations. In Z. Fülöp and F. Gécseg, editors, ICALP 95: Automata, Languages, and Programming, Lecture Notes in Computer Science 944, pages 324–335. Springer-Verlag, 1995.

    Google Scholar 

  15. T.A. Henzinger, O. Kupferman, and M.Y. Vardi. A space-efficient on-the-fly algorithm for real-time model checking. In Proc. 7th Conferance on Concurrency Theory, Pisa, August 1996. Springer-Verlag.

    Google Scholar 

  16. T.A. Henzinger, Z. Manna, and A. Pnueli. What good are digital clocks? In W. Kuich, editor, ICALP 92: Automata, Languages, and Programming, Lecture Notes in Computer Science 623, pages 545–558. Springer-Verlag, 1992.

    Google Scholar 

  17. T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111:193–244, 1994.

    Google Scholar 

  18. O. Kupferman and O. Grumberg. Buy one, get one free! Journal of Logic and Computation, 6(4), 1996.

    Google Scholar 

  19. O. Kupferman and M.Y. Vardi. On the complexity of branching modular model checking. In Proc. 6th Conferance on Concurrency Theory, pages 408–422, Philadelphia, August 1995. Springer-Verlag.

    Google Scholar 

  20. F. Laroussinie and K. G. Larsen. Compositional model checking of real time systems. In Proc. 6th Conferance on Concurrency Theory, pages 27–41, Philadelphia, August 1995. Springer-Verlag.

    Google Scholar 

  21. K.L. McMillan. Symbolic model checking. Kluwer Academic Publishers, 1993.

    Google Scholar 

  22. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, Berlin, January 1992.

    Google Scholar 

  23. A. Pnueli. The temporal logic of programs. In Proc. 18th IEEE Symposium on Foundation of Computer Science, pages 46–57, 1977.

    Google Scholar 

  24. J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th International Symp. on Programming, volume 137, pages 337–351. Springer-Verlag, Lecture Notes in Computer Science, 1981.

    Google Scholar 

  25. O.V. Sokolsky and S.A. Smolka. Local model checking for real-time systems. In Computer Aided Verification, Proc. 7th Int. Workshop, Lecture Notes in Computer Science 939, pages 211–224, Liege, July 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. EECS Department, UC Berkeley, 94720-1770, Berkeley, CA, USA

    Thomas A. Henzinger & Orna Kupferman

Authors
  1. Thomas A. Henzinger
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Orna Kupferman
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Oded Maler

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Henzinger, T.A., Kupferman, O. (1997). From quantity to quality. In: Maler, O. (eds) Hybrid and Real-Time Systems. HART 1997. Lecture Notes in Computer Science, vol 1201. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014712

Download citation

  • DOI: https://doi.org/10.1007/BFb0014712

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-62600-8

  • Online ISBN: 978-3-540-68330-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation