Abstract
Duration Calculus (DC) is a real-time logic with measurement of duration of propositions in observation intervals. It is a highly expressive logic with continuous time behaviours (also called signals) as its models. Validity checking of DC is undecidable. We propose a method for validity checking of Duration Calculus by reduction to a sampled time version of this logic called Well Sampled Interval Duration Logic (WSIDL). This reduction relies on representing a continuous time behaviour by a well-sampled behaviour with 1-oversampling. We provide weak and strong reductions (abstractions) of logic DC to logic WSIDL which respectively preserve the validity and the counter models. By combining these reductions with previous work on deciding IDL, we have implemented a tool for validity checking of Duration Calculus. This provides a partial but practical method for validity checking of Duration Calculus. We present some preliminary experimental results to measure the success of this approach.
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, pp. 332–335. Springer, Heidelberg (1990)
Bouajjani, A., Lakhnech, Y., Robbana, R.: From Duration Calculus to Linear Hybrid Automata. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 196–210. Springer, Heidelberg (1995)
Chakravorty, G., Pandya, P.K.: Digitizing Interval Duration Logic. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 167–179. Springer, Heidelberg (2003)
Fränzle, M.: Model-Checking Dense-Time Duration Calculus. In: Hansen, M.R. (ed.) Duration Calculus: A Logical Approach to Real-Time Systems Workshop proceedings of ESSLLI X (1998)
Fränzle, M.: Take it NP-easy: Bounded Model Construction for Duration Calculus. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 245–264. Springer, Heidelberg (2002)
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)
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)
Hirshfeld, Y., Rabinovich, A.: Logics for Real-time: Decidability and Complexity. Fundamenta Informaticae 62(1), 1–28 (2004)
Krishna, S.N., Pandya, P.K.: Modal Strength reduction in QDDC. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 444–456. Springer, Heidelberg (2005)
Ouaknine, J., Worrell, J.: Revisiting Digitization, Robustness and Decidability for Timed Automata. In: Proc. 18th IEEE Symposium on LICS, pp. 198–207 (2003)
Ouaknine, J., Worrell, J.: On Decidability of Metric Temporal Logic. In: Proc. 20th IEEE Symposium on LICS, pp. 188–197 (2005)
Pandya, P.K.: Specifying and Deciding Quantified Discrete-time Duration Calculus Formulae using DCVALID: An Automata Theoretic Approach. In: Proc. RTTOOLS’(2001)
Pandya, P.K.: Model checking CTL*[DC]. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 559–573. Springer, Heidelberg (2001)
Pandya, P.K.: Interval duration logic: expressiveness and decidability. ENTCS (Proc. TPTS) 65(6), 1–19 (2002)
Sharma, B., Pandya, P.K., Chakraborty, S.: Bounded Validity Checking of Interval Duration Logic. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 301–316. Springer, Heidelberg (2005)
Zhou, C., Hoare, C.A.R., Ravn, A.P.: A Calculus of Durations. Info. Proc. Letters 40(5) (1991)
Zhou, C., Zhang, J., Yang, L., Li, X.: Linear duration invariants. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 86–109. Springer, Heidelberg (1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Pandya, P.K., Krishna, S.N., Loya, K. (2007). On Sampling Abstraction of Continuous Time Logic with Durations. In: Grumberg, O., Huth, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2007. Lecture Notes in Computer Science, vol 4424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71209-1_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-71209-1_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71208-4
Online ISBN: 978-3-540-71209-1
eBook Packages: Computer ScienceComputer Science (R0)