Abstract
Timed automata can be studied in not only a dense-time setting but also a discrete-time setting. The most common example of discrete-time semantics is the so called sampled semantics (i.e., discrete semantics with a fixed time granularity ε). In the real-time setting, the universality problem is known to be undecidable for timed automata. In this work, we study the universality question for the languages accepted by timed automata with sampled semantics. On the negative side, we show that deciding whether for all sampling periods ε a timed automaton accepts all timed words in ε-sampled semantics is as hard as in the real-time case, i.e., undecidable. On the positive side, we show that checking whether there is a sampling period such that a timed automaton accepts all untimed words in ε-sampled semantics is decidable. Our proof uses clock difference relations, developed to characterize the reachability relation for timed automata in connection with sampled semantics.
Chapter PDF
Similar content being viewed by others
References
Abdulla, P.A., et al.: Decidability and complexity results for timed automata via channel machines. In: Caires, L., et al. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1089–1101. Springer, Heidelberg (2005)
Abdulla, P.A., Krcal, P., Yi, W.: Sampled universality of timed automata. Technical Report 2007-001, IT Department, Uppsala University (Jan. 2007)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994), citeseer.nj.nec.com/alur94theory.html
Asarin, E., et al.: Data-structures for the verification of timed automata. In: Maler, O. (ed.) HART 1997. LNCS, vol. 1201, pp. 346–360. Springer, Heidelberg (1997)
Asarin, E., Maler, O., Pnueli, A.: On discretization of delays in timed automata and digital circuits. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 470–484. Springer, Heidelberg (1998)
Beyer, D.: Improvements in BDD-based reachability analysis of timed automata. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 318–343. Springer, Heidelberg (2001)
Bozga, M., Maler, O., Tripakis, S.: Efficient verification of timed automata using dense and discrete time semantics. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 125–141. Springer, Heidelberg (1999)
Comon, H., Jurski, Y.: Timed automata and the theory of real numbers. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 242–257. Springer, Heidelberg (1999)
Dima, C.: Computing reachability relations in timed automata. In: Proc. of LICS’02, IEEE Computer Society Press, Los Alamitos (2002)
Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) Automata, Languages and Programming. LNCS, vol. 623, pp. 545–558. Springer, Heidelberg (1992)
Henzinger, T.A., Raskin, J.-F.: 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)
Krčál, P., Pelánek, R.: On sampled semantics of timed systems. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 310–321. Springer, Heidelberg (2005)
Larsen, K.G., Yi, W.: Time-abstracted bisimulation: Implicit specifications and decidability. Information and Computation 134(2), 75–101 (1997)
Mayr, R.: Undecidable problems in unreliable computations. Theoretical Computer Science 297, 347–354 (2003)
Ouaknine, J., Worrell, J.: Revisiting digitization, robustness, and decidability for time d automata. In: Proc. of LICS’03, pp. 198–207. IEEE Computer Society Press, Los Alamitos (2003)
Ouaknine, J., Worrell, J.: Universality and language inclusion for open and closed timed automata. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 375–388. Springer, Heidelberg (2003)
Ouaknine, J., Worrell, J.: On the language inclusion problem for timed automata: Closing a decidability gap. In: Proc. of LICS 2004, pp. 54–63. IEEE Computer Society Press, Los Alamitos (2004)
Puri, A.: Dynamical properties of timed automata. Discrete Event Dynamic Systems 10(1-2), 87–113 (2000)
De Wulf, M., Doyen, L., Raskin, J.-F.: Almost ASAP semantics: From timed models to timed implementations. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 296–310. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Abdulla, P.A., Krcal, P., Yi, W. (2007). Sampled Universality of Timed Automata. In: Seidl, H. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2007. Lecture Notes in Computer Science, vol 4423. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71389-0_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-71389-0_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71388-3
Online ISBN: 978-3-540-71389-0
eBook Packages: Computer ScienceComputer Science (R0)