Expressiveness of Updatable Timed Automata
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.
KeywordsFractional Part Expressive Power Label Transition System Decidable Classis Local Update
Unable to display preview. Download preview PDF.
- 1.R. Alur, C. Courcoubetis, and T.A. Henzinger. The observational power of clocks. In Proc. of CONCUR’94, LNCS 836, pages 162–177, 1994.Google Scholar
- 2.R. Alur and D. Dill. Automata for modeling real-time systems. In Proc. of ICALP’90, LNCS 443, pages 322–335, 1990.Google Scholar
- 3.R. Alur and D. Dill. A theory of timed automata. TCS’94, pages 183–235, 1994.Google Scholar
- 4.R. Alur, T.A. Henzinger, and M. Vardi. Parametric real-time reasoning. In Proc. of the 25th ACM STOC, pages 592–601, 1993.Google Scholar
- 5.P. Bouyer, C. Dufourd, E. Fleury, and A. Petit. Are timed automata updatable? In Proc. of CAV’2000, LNCS, 2000. To appear.Google Scholar
- 6.P. Bouyer, C. Dufourd, E. Fleury, and A. Petit. Expressiveness of updatable timed automata. Research report, ENS de Cachan, 2000.Google Scholar
- 7.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.Google Scholar
- 8.B. Bérard and C. Dufourd. Timed automata and additive clock constraints. Research report LSV-00-4, LSV, ENS de Cachan, 2000.Google Scholar
- 9.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.Google Scholar
- 10.C. Choffrut and M. Goldwurm. Timed automata with periodic clock constraints. Technical Report 99/28, LIAFA, Université Paris VII, 1999.Google Scholar
- 11.F. Demichelis and W. Zielonka. Controlled timed automata. In Proc. of CONCUR’98, LNCS 1466, pages 455–469, 1998.Google Scholar
- 12.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).Google Scholar
- 14.R. Milner. Communication and Concurrency. Prentice Hall Int., 1989.Google Scholar
- 15.D. M. Park. Concurrency on automata and infinite sequences. In CTCS’81, LNCS 104, pages 167–183, 1981.Google Scholar
- 16.T. Wilke. Specifying timed state sequences in powerful decidable logics and timed automata. In Proc. of FTRT-FTS, LNCS 863, pages 694–715, 1994.Google Scholar
- 17.S. Yovine. A verification tool for real-time systems. Springer International Journal of Software Tools for Technology Transfer, 1, 1997.Google Scholar