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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
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)
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.: 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)
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)
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)
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)
Hansen, M.R.: Model-checking discrete duration calculus. Formal Aspects of Computing 6(6A), 826–845 (1994)
Puri, A.: Dynamical properties of timed automata. In: Ravn, A.P., Rischel, H. (eds.) [12], pp. 210–227
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)
Ratschan, S.: Quantified constraints under perturbations. Journal of Symbolic Computation 33(4), 493–505 (2002)
Ratschan, S.: Search heuristics for box decomposition methods. Journal of Global Optimization 24(1), 51–60 (2002)
Ravn, A.P., Rischel, H. (eds.): FTRTFT 1998. LNCS, vol. 1486. Springer, Heidelberg (1998)
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)
Tarski, A.: A decision method for elementary algebra and geometry. RAND Corporation, Santa Monica, Calif. (1948)
Chaochen, Z., Hansen, M.R.: Duration Calculus — A Formal Approach to Real-Time Systems. EATCS monographs on theoretical computer science. Springer, Heidelberg (2004)
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)
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
© 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)