Verifying invariance properties of timed systems with duration variables
We consider the verification problem of invariance properties for timed systems modeled by (extended) Timed Graphs with duration variables. While clocks of a Timed Graph can be seen as continuous (real valued) variables with rates 1 at each control location of the system, duration variables (also called integrators) are continuous variables having rates 0 or 1. The use of integrators allows to reason about the accumulated delays spent at some particular locations during some computation. We show that under some conditions, the verification problem of invariance properties is decidable for (closed) Timed Graphs with one integrator, the integrator can be tested and/or reset at any transition. For this, we use a new digitization technique and prove that every real computation of such systems has a valid digitization. Then, we show how to solve the verification problem in the case of a discrete time domain.
Unable to display preview. Download preview PDF.
- [ACD90]R. Alur, C. Courcoubetis, and D. Dill. Model-Checking for Real-Time Systems. In 5th Symp. on Logic in Computer Science. IEEE, 1990.Google Scholar
- [ACH+92]R. Alur, C. Courcoubetis, N. Halbwachs, D. Dill, and H. Wong-Toi. Minimization of Timed Transition Systems. In CONCUR'92. LNCS 630, Springer Verlag, 1992.Google Scholar
- [ACH93]R. Alur, C. Courcoubetis, and T. A. Henzinger. Computing Accumulated Delays in Real-time Systems. In Hybrid Systems. Springer-Verlag, 1993. LNCS 736.Google Scholar
- [ACHH93]R. Alur, C. Courcoubetis, T. Henzinger, and P-H. Ho. Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. In Hybrid Systems. Springer-Verlag, 1993. LNCS 736.Google Scholar
- [BER94]A. Bouajjani, R. Echahed, and R. Robbana. Verification of Context-Free Timed Systems using Linear Hybrid Observers. In Proc. Computer Aided Verification (CAV'94), 1994.Google Scholar
- [Cer92]K. Cerans. Decidability of Bisimulation Equivalence for Parallel Timer Processes. In Proc. Computer-Aided Verification (CAV'92). Springer-Verlag, 1992. LNCS 663.Google Scholar
- [CHR91]Z. Chaochen, C.A.R. Hoare, and A.P. Ravn. A Calculus of Durations. Information Processing Letters, 40:269–276, 1991.Google Scholar
- [HK94]T.A. Henzinger and P.W. Kopke. Undecidability Results for Hybrid Systems. Draft, June 1994.Google Scholar
- [HMP92]T. Henzinger, Z. Manna, and A. Pnueli. What Good are Digital Clocks? In 19th. Internat. Coll. on Automata, Languages and Programming. Springer-Verlag, 1992. LNCS 623.Google Scholar
- [HNSY92]T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic Model-Checking for Real-Time Systems. In 7th Symp. on Logic in Computer Science. IEEE, 1992.Google Scholar
- [KPSY93]Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Integration Graphs: A Class of Decidable Hybrid System s. In Hybrid Systems. Springer-Verlag, 1993. LNCS 736.Google Scholar
- [NOSY93]X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. An Approach to the Description and Analysis of Hybrid Systems. In Hybrid Systems. Springer-Verlag, 1993. LNCS 736.Google Scholar
- [NSY92]X. Nicollin, J. Sifakis, and S. Yovine. From ATP to Timed Graphs and Hybrid Systems. In REX workshop on Real-Time: Theory and Practice. Springer-Verlag, 1992. LNCS 600.Google Scholar