Abstract
Since their introduction by Alur and Dill, timed automata have been one of the most widely studied models for real-time systems. The syntactic extension of so-called updatable timed automata allows more powerful updates of clocks than the reset operation proposed in the original model.
We prove that any language accepted by an updatable timed automaton (from classes where emptiness is decidable) is also accepted by a “classical” timed automaton. We propose even more precise results on bisimilarity between updatable and classical timed automata.
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
R. Alur, C. Courcoubetis, and T.A. Henzinger. The observational power of clocks. In Proc. of CONCUR’94, LNCS 836, pages 162–177, 1994.
R. Alur and D. Dill. Automata for modeling real-time systems. In Proc. of ICALP’90, LNCS 443, pages 322–335, 1990.
R. Alur and D. Dill. A theory of timed automata. TCS’94, pages 183–235, 1994.
R. Alur, T.A. Henzinger, and M. Vardi. Parametric real-time reasoning. In Proc. of the 25th ACM STOC, pages 592–601, 1993.
P. Bouyer, C. Dufourd, E. Fleury, and A. Petit. Are timed automata updatable? In Proc. of CAV’2000, LNCS, 2000. To appear.
P. Bouyer, C. Dufourd, E. Fleury, and A. Petit. Expressiveness of updatable timed automata. Research report, ENS de Cachan, 2000.
B. Bérard, V. Diekert, P. Gastin, and A. Petit. Characterization of the expressive power of silent transitions in timed automata. Fundamenta Informaticae, pages 145–182, 1998.
B. Bérard and C. Dufourd. Timed automata and additive clock constraints. Research report LSV-00-4, LSV, ENS de Cachan, 2000.
B. Bérard and L. Fribourg. Automatic verification of a parametric real-time program: the ABR conformance protocol. In Proc. of CAV’99, LNCS 1633, pages 96–107, 1999.
C. Choffrut and M. Goldwurm. Timed automata with periodic clock constraints. Technical Report 99/28, LIAFA, Université Paris VII, 1999.
F. Demichelis and W. Zielonka. Controlled timed automata. In Proc. of CONCUR’98, LNCS 1466, pages 455–469, 1998.
T.A. Henzinger, P. Ho, and H. Wong-Toi. Hytech: A model checker for hybrid systems. In Software Tools for Technology Transfer, pages 110–122, 1997. (special issue on Timed and Hybrid Systems).
K.G. Larsen, P. Pettersson, and W. Yi. Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer, 1:134–152, 1997.
R. Milner. Communication and Concurrency. Prentice Hall Int., 1989.
D. M. Park. Concurrency on automata and infinite sequences. In CTCS’81, LNCS 104, pages 167–183, 1981.
T. Wilke. Specifying timed state sequences in powerful decidable logics and timed automata. In Proc. of FTRT-FTS, LNCS 863, pages 694–715, 1994.
S. Yovine. A verification tool for real-time systems. Springer International Journal of Software Tools for Technology Transfer, 1, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bouyer, P., Dufourd, C., Fleury, E., Petit, A. (2000). Expressiveness of Updatable Timed Automata. In: Nielsen, M., Rovan, B. (eds) Mathematical Foundations of Computer Science 2000. MFCS 2000. Lecture Notes in Computer Science, vol 1893. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44612-5_19
Download citation
DOI: https://doi.org/10.1007/3-540-44612-5_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67901-1
Online ISBN: 978-3-540-44612-5
eBook Packages: Springer Book Archive