Expressiveness of Updatable Timed Automata

  • P. Bouyer
  • C. Dufourd
  • E. Fleury
  • A. Petit
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1893)


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.


Fractional Part Expressive Power Label Transition System Decidable Classis Local Update 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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. 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. 3.
    R. Alur and D. Dill. A theory of timed automata. TCS’94, pages 183–235, 1994.Google Scholar
  4. 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. 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. 6.
    P. Bouyer, C. Dufourd, E. Fleury, and A. Petit. Expressiveness of updatable timed automata. Research report, ENS de Cachan, 2000.Google Scholar
  7. 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. 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. 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. 10.
    C. Choffrut and M. Goldwurm. Timed automata with periodic clock constraints. Technical Report 99/28, LIAFA, Université Paris VII, 1999.Google Scholar
  11. 11.
    F. Demichelis and W. Zielonka. Controlled timed automata. In Proc. of CONCUR’98, LNCS 1466, pages 455–469, 1998.Google Scholar
  12. 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
  13. 13.
    K.G. Larsen, P. Pettersson, and W. Yi. Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer, 1:134–152, 1997.zbMATHCrossRefGoogle Scholar
  14. 14.
    R. Milner. Communication and Concurrency. Prentice Hall Int., 1989.Google Scholar
  15. 15.
    D. M. Park. Concurrency on automata and infinite sequences. In CTCS’81, LNCS 104, pages 167–183, 1981.Google Scholar
  16. 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. 17.
    S. Yovine. A verification tool for real-time systems. Springer International Journal of Software Tools for Technology Transfer, 1, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • P. Bouyer
    • 1
  • C. Dufourd
    • 1
  • E. Fleury
    • 1
  • A. Petit
    • 1
  1. 1.LSV, UMR 8643CNRS & ENS de CachanCachan cedexFrance

Personalised recommendations