Abstract
We consider timed automata whose clocks are imperfect. For a given perturbation error 0 < ε< 1, the perturbed language of a timed automaton is obtained by letting its clocks change at a rate within the interval [1 − ε,1 + ε]. We show that the perturbed language of a timed automaton with a single clock can be captured by a deterministic timed automaton. This leads to a decision procedure for the language inclusion problem for systems modeled as products of 1-clock automata with imperfect clocks. We also prove that determinization and decidability of language inclusion are not possible for multi-clock automata, even with perturbation.
This research was partially supported by the US National Science Foundation under grants ITR/SY0121431 and CCR0410662. The second author was also supported by the MIUR grant ex-60% 2003 Università degli Studi di Salerno.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Alur, R., Madhusudan, P.: Decision problems for timed automata: a survey. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 1–24. Springer, Heidelberg (2004)
Larsen, K., Pettersson, P., Yi, W.: Uppaal in a nutshell. Springer International Journal of Software Tools for Technology Transfer 1 (1997)
Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool kronos. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 208–219. Springer, Heidelberg (1996)
Wang, F.: Efficient data structures for fully symbolic verification of real-time software systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 157–171. Springer, Heidelberg (2000)
Henzinger, T., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 545–558. Springer, Heidelberg (1992)
Alur, R., Fix, L., Henzinger, T.: Event-clock automata: a determinizable class of timed automata. Theoretical Computer Science 211, 253–273 (1999); A preliminary version appears In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 253–273. Springer, Heidelberg (1994)
Alur, R., Courcoubetis, C., Henzinger, T.: The observational power of clocks. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 162–177. Springer, Heidelberg (1994)
Alur, R., Henzinger, T.: Back to the future: Towards a theory of timed regular languages. In: Proceedings of the 33rd IEEE Symposium on Foundations of Computer Science, pp. 177–186 (1992)
Henzinger, T., Raskin, J., Schobbens, P.: The regular real-time languages. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 580–593. Springer, Heidelberg (1998)
Ouaknine, J., Worrell, J.: Revisiting digitization, robustness, and decidability for timed automata. In: Proc. of the 18th IEEE Symp. on Logic in Comp. Sc. (2003)
Ouaknine, J., Worrell, J.: On the language inclusion problem for timed automata: Closing a decidability gap. In: Proceedings of the 19th IEEE Symposium on Logic in Computer Science (2004)
Gupta, V., Henzinger, T., Jagadeesan, R.: Robust timed automata. In: Maler, O. (ed.) HART 1997. LNCS, vol. 1201, pp. 48–62. Springer, Heidelberg (1997)
Henzinger, T., Raskin, J.: Robust undecidability of timed and hybrid systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 145–159. Springer, Heidelberg (2000)
Henzinger, T., Kopke, P., Puri, A., Varaiya, P.: What’s decidable about hybrid automata. Journal of Computer and System Sciences 57, 94–124 (1998)
Brzozowski, J., Seger, C.: Advances in asynchronous circuit theory, Part II: Bounded inertial delay models, MOS circuit design techniques. Bulletin of the European Assoc. for Theoretical Comp. Sc. 43, 199–263 (1991)
Rokicki, T.: Representing and modeling digital circuits. PhD thesis, Stanford University (1993)
Maler, O., Pnueli, A.: Timing analysis of asynchronous circuits using timed automata. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 189–205. Springer, Heidelberg (1995)
Tasiran, S., Brayton, R.: STARI: a case study in compositional and hierarchical timing verification. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 191–201. Springer, Heidelberg (1997)
Puri, A.: Dynamical properties of timed automata. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 210–227. Springer, Heidelberg (1998)
De Wulf, M., Doyen, L., Markey, N., Raskin, J.: Robustness and implementability of timed automata. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253. Springer, Heidelberg (2004)
Alur, R., Feder, T., Henzinger, T.: The benefits of relaxing punctuality. Journal of the ACM 43, 116–146 (1996)
Agrawal, M., Thiagarajan, P.S.: Lazy rectangular hybrid automata. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 1–15. Springer, Heidelberg (2004)
Ouaknine, J.: Personal communication (2004)
Bouyer, P.: Forward analysis of updatable timed automata. Formal Methods in System Design 24, 281–320 (2004)
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
Alur, R., La Torre, S., Madhusudan, P. (2005). Perturbed Timed Automata. In: Morari, M., Thiele, L. (eds) Hybrid Systems: Computation and Control. HSCC 2005. Lecture Notes in Computer Science, vol 3414. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31954-2_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-31954-2_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25108-8
Online ISBN: 978-3-540-31954-2
eBook Packages: Computer ScienceComputer Science (R0)