Advertisement

A Robust Interpretation of Duration Calculus

  • Martin Fränzle
  • Michael R. Hansen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3722)

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.

Keywords

Metric-time temporal logic Robust interpretation Discrete time vs dense time 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 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)CrossRefGoogle Scholar
  3. 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)CrossRefGoogle Scholar
  4. 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)CrossRefGoogle Scholar
  5. 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. 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)CrossRefGoogle Scholar
  7. 7.
    Hansen, M.R.: Model-checking discrete duration calculus. Formal Aspects of Computing 6(6A), 826–845 (1994)zbMATHCrossRefGoogle Scholar
  8. 8.
    Puri, A.: Dynamical properties of timed automata. In: Ravn, A.P., Rischel, H. (eds.) [12], pp. 210–227Google Scholar
  9. 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)CrossRefGoogle Scholar
  10. 10.
    Ratschan, S.: Quantified constraints under perturbations. Journal of Symbolic Computation 33(4), 493–505 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Ratschan, S.: Search heuristics for box decomposition methods. Journal of Global Optimization 24(1), 51–60 (2002)CrossRefMathSciNetGoogle Scholar
  12. 12.
    Ravn, A.P., Rischel, H. (eds.): FTRTFT 1998. LNCS, vol. 1486. Springer, Heidelberg (1998)Google Scholar
  13. 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)CrossRefGoogle Scholar
  14. 14.
    Tarski, A.: A decision method for elementary algebra and geometry. RAND Corporation, Santa Monica, Calif. (1948)Google Scholar
  15. 15.
    Chaochen, Z., Hansen, M.R.: Duration Calculus — A Formal Approach to Real-Time Systems. EATCS monographs on theoretical computer science. Springer, Heidelberg (2004)zbMATHGoogle Scholar
  16. 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. 17.
    Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Martin Fränzle
    • 1
  • Michael R. Hansen
    • 2
  1. 1.FK II, Dpt. InformatikCarl von Ossietzky Universität OldenburgOldenburgGermany
  2. 2.Informatics and Mathematical ModellingTechnical University of DenmarkLyngbyDenmark

Personalised recommendations