# Verification methods for the divergent runs of clock systems

## 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## Preview

Unable to display preview. Download preview PDF.

## References

- [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 - [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 - [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 - [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 - [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 - [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 - [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 - [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
- [Hen92]T.A. Henzinger. Sooner is safer than later.
*Information Processing Letters*, 43:135–141, 1992.Google Scholar - [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 - [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 - [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 - [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 - [MP92]Z. Manna and A. Pnueli.
*The Temporal Logic of Reactive and Concurrent Systems: Specification*. Springer-Verlag, 1992.Google Scholar - [MP93]Z. Manna and A. Pnueli. Models for reactivity.
*Acta Informatica*, 30:609–678, 1993.Google Scholar - [Sch94]F.B. Schneider.
*On Concurrent Programming*. To Appear, 1994.Google Scholar