Skip to main content

A Robust Interpretation of Duration Calculus

  • Conference paper
Theoretical Aspects of Computing – ICTAC 2005 (ICTAC 2005)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3722))

Included in the following conference series:

Abstract

We transfer the concept of robust interpretation from arithmetic first-order theories to metric-time temporal logics. The idea is that the interpretation of a formula is robust iff its truth value does not change under small variation of the constants in the formula. Exemplifying this on Duration Calculus (DC), our findings are that the robust interpretation of DC is equivalent to a multi-valued interpretation that uses the real numbers as semantic domain and assigns Lipschitz-continuous interpretations to all operators of DC. Furthermore, this continuity permits approximation between discrete and dense time, thus allowing exploitation of discrete-time (semi-)decision procedures on dense-time properties.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Asarin, E., Bouajjani, A.: Perturbed turing machines and hybrid systems. In: Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2001). IEEE, Los Alamitos (2001)

    Google Scholar 

  2. 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)

    Chapter  Google Scholar 

  3. Fränzle, M.: Analysis of hybrid systems: An ounce of realism can save an infinity of states. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 126–140. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  4. Fränzle, M.: What will be eventually true of polynomial hybrid automata. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 340–359. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  5. Fränzle, M., Hansen, M.R.: A Robust Interpretation of Duration Calculus (Extended abstract). In: Pettersson, P., Yi, W. (eds.) Nordic Workshop on Programming Theory, Technical report 2004-041, Department of Information Technology, Uppsala University, pp. 83–85 (2004)

    Google Scholar 

  6. Gupta, V., Henzinger, T.A., Jagadeesan, R.: Robust timed automata. In: Maler, O. (ed.) HART 1997. LNCS, vol. 1201, pp. 331–345. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  7. Hansen, M.R.: Model-checking discrete duration calculus. Formal Aspects of Computing 6(6A), 826–845 (1994)

    Article  MATH  Google Scholar 

  8. Puri, A.: Dynamical properties of timed automata. In: Ravn, A.P., Rischel, H. (eds.) [12], pp. 210–227

    Google Scholar 

  9. Ratschan, S.: Continuous first-order constraint satisfaction. In: Calmet, J., Benhamou, B., Caprotti, O., Hénocque, L., Sorge, V. (eds.) AISC 2002 and Calculemus 2002. LNCS (LNAI), vol. 2385, pp. 181–195. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  10. Ratschan, S.: Quantified constraints under perturbations. Journal of Symbolic Computation 33(4), 493–505 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  11. Ratschan, S.: Search heuristics for box decomposition methods. Journal of Global Optimization 24(1), 51–60 (2002)

    Article  MathSciNet  Google Scholar 

  12. Ravn, A.P., Rischel, H. (eds.): FTRTFT 1998. LNCS, vol. 1486. Springer, Heidelberg (1998)

    Google Scholar 

  13. Ravn, A.P., Rischel, H., Hansen, K.M.: Specifying and verifying requirements of real-time systems. IEEE Transactions on Software Engineering 19(1), 41–55 (1993)

    Article  Google Scholar 

  14. Tarski, A.: A decision method for elementary algebra and geometry. RAND Corporation, Santa Monica, Calif. (1948)

    Google Scholar 

  15. Chaochen, Z., Hansen, M.R.: Duration Calculus — A Formal Approach to Real-Time Systems. EATCS monographs on theoretical computer science. Springer, Heidelberg (2004)

    MATH  Google Scholar 

  16. Chaochen, Z., Hansen, M.R., Sestoft, P.: Decidability and undecidability results for duration calculus. In: Enjalbert, P., Wagner, K.W., Finkel, A. (eds.) STACS 1993. LNCS, vol. 665, pp. 58–68. Springer, Heidelberg (1993)

    Google Scholar 

  17. Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fränzle, M., Hansen, M.R. (2005). A Robust Interpretation of Duration Calculus. In: Van Hung, D., Wirsing, M. (eds) Theoretical Aspects of Computing – ICTAC 2005. ICTAC 2005. Lecture Notes in Computer Science, vol 3722. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11560647_17

Download citation

  • DOI: https://doi.org/10.1007/11560647_17

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-29107-7

  • Online ISBN: 978-3-540-32072-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics