Abstract
In this paper, we study the verification of dense time properties by discrete time analysis. Interval Duration Logic, (IDL), is a highly expressive dense time logic for specifying properties of real-time systems. Validity checking of IDL formulae is in general undecidable. A corresponding discrete-time logic QDDC has decidable validity.
In this paper, we consider a reduction of IDL validity question to QDDC validity using notions of digitization. A new notion of Strong Closure under Inverse Digitization, SCID, is proposed. For all SCID formulae, the dense and the discrete-time validity coincide. Moreover, SCID has good algebraic properties which can be used to conveniently prove that many IDL formulae are SCID. We also give some approximation techniques to strengthen/weaken formulae to SCID form. For SCID formulae, the validity of dense-time IDL formulae can be checked using the validity checker for discrete-time logic QDDC.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Alur, R., Dill, D.L.: Automata for modeling Real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443. Springer, Heidelberg (1990)
Beyer, D.: Rabiit: Verification of Real-Time Systems. In: Workshop on Real-time Tools (RT-TOOLS 2001), Aalborg, Denmark (2001)
Franzle, M.: Decidability of Duration Calculi on Restricted Model Classes. ProCoS Technical Report Kiel MF/1. Christian-Albrechts Universitat Kiel, Germany (1996)
Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 545–558. Springer, Heidelberg (1992)
Hung, D.V., Giang, P.H.: Sampling Semantics of Duration Calculus. In: Jonsson, B., Parrow, J. (eds.) FTRTFT 1996. LNCS, vol. 1135, pp. 188–207. Springer, Heidelberg (1996)
Pandya, P.K., Hung, D.V.: A Duration Calculus of Weakly Monotonic Time. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, p. 55. Springer, Heidelberg (1998)
Pandya, P.K.: Specifying and Deciding Quantified Discrete-time Duration Calculus Formulae using DCVALID: An Automata Theoretic Approach. In: Workshop on Real-time Tools (RTTOOLS 2001), Aalborg, Denmark (2001)
Pandya, P.K.: Interval Duration Logic: Expressiveness and Decidability. In: Workshop on Theory and Practice of Timed Systems (TPTS 2002), Electronic Notes in Theoretical Computer Science, ENTCS 65.6. Elsevier Science B.V (2002)
Ravn, A.P.: Design of Real-time Embedded Computing Systems. Department of Computer Science, Technical University of Denmark (1994)
Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A Calculus of Durations. Information Processing Letters 40(5), 269–276 (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chakravorty, G., Pandya, P.K. (2003). Digitizing Interval Duration Logic. In: Hunt, W.A., Somenzi, F. (eds) Computer Aided Verification. CAV 2003. Lecture Notes in Computer Science, vol 2725. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45069-6_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-45069-6_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40524-5
Online ISBN: 978-3-540-45069-6
eBook Packages: Springer Book Archive