Advertisement

Verification methods for the divergent runs of clock systems

  • Thomas A. Henzinger
  • Peter W. Kopke
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 863)

Abstract

We present a methodology for proving temporal properties of the divergent runs of reactive systems with real-valued clocks. A run diverges if time advances beyond any bound. Since the divergent runs of a system may satisfy liveness properties that are not satisfied by some convergent runs, the standard proof rules are incomplete if only divergent runs are considered.

First, we develop a sound and complete proof calculus for divergence, which is based on translating clock systems into discrete systems. Then, we show that simpler proofs can be obtained for stronger divergence assumptions, such as unknown ε-divergence, which requires that all delays have a minimum duration of some unknown constant ε. We classify all real-time systems into an infinite hierarchy, according to how well they admit the translation of eventuality properties into equivalent safety properties.

Keywords

Safety Property Action Predicate Clock System Liveness Property State Predicate 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [AAT94]
    R. Alur, H. Attiya, and G. Taubenfeld. Time-adaptive algorithms for synchronization. In Proceedings of the 26th Annual Symposium on Theory of Computing. ACM Press, 1994.Google Scholar
  2. [ACH94]
    R. Alur, C. Courcoubetis, and T.A. Henzinger. The observational power of clocks. In CONCUR 94: Theories of Concurrency, Lecture Notes in Computer Science. Springer-Verlag, 1994.Google Scholar
  3. [AD90]
    R. Alur and D.L. Dill. Automata for modeling real-time systems. In M.S. Paterson, editor, ICALP 90: Automata, Languages, and Programming, Lecture Notes in Computer Science 443, pages 322–335. Springer-Verlag, 1990.Google Scholar
  4. [AH92]
    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.Google Scholar
  5. [AH93]
    R. Alur and T.A. Henzinger. Real-time system = discrete system + clock variables. In T. Rus, editor, Proceedings of the First AMAST Workshop on Real-time Systems, 1993.Google Scholar
  6. [AH94]
    R. Alur and T.A. Henzinger. Finitary fairness. In Proceedings of the Ninth Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, 1994.Google Scholar
  7. [AL92]
    M. Abadi and L. Lamport. An old-fashioned recipe for real time. 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 1–27. Springer-Verlag, 1992.Google Scholar
  8. [GSSAL93]
    R. Gawlick, R. Segala, J. SØgaard-Andersen, and N. Lynch. Liveness in timed and untimed systems. Technical Report 587, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, Massachusetts, 1993.Google Scholar
  9. [Hen92]
    T.A. Henzinger. Sooner is safer than later. Information Processing Letters, 43:135–141, 1992.Google Scholar
  10. [HMP91]
    T.A. Henzinger, Z. Manna, and A. Pnueli. Temporal proof methodologies for real-time systems. In Proceedings of the 18th Annual Symposium on Principles of Programming Languages, pages 353–366. ACM Press, 1991.Google Scholar
  11. [HNSY92]
    T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. In Proceedings of the Seventh Annual Symposium on Logic in Computer Science, pages 394–406. IEEE Computer Society Press, 1992.Google Scholar
  12. [LV92]
    N. Lynch and F. Vaandrager. Forward and backward simulations for timing-based systems. 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 397–446. Springer-Verlag, 1992.Google Scholar
  13. [MP89]
    Z. Manna and A. Pnueli. Completing the temporal picture. In G. Ausiello, M. Dezani-Ciancaglini, and S. Ronchi Della Rocca, editors, ICALP 89: Automata, Languages, and Programming, Lecture Notes in Computer Science 372, pages 534–558. Springer-Verlag, 1989.Google Scholar
  14. [MP92]
    Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.Google Scholar
  15. [MP93]
    Z. Manna and A. Pnueli. Models for reactivity. Acta Informatica, 30:609–678, 1993.Google Scholar
  16. [Sch94]
    F.B. Schneider. On Concurrent Programming. To Appear, 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Thomas A. Henzinger
    • 1
  • Peter W. Kopke
    • 1
  1. 1.Computer Science DepartmentCornell UniversityIthaca

Personalised recommendations