On the power of non-observable actions in timed automata

  • Béatrice Bérard
  • Paul Gastin
  • Antoine Petit
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1046)


Timed finite automata, introduced by Alur and Dill, are one of the most widely studied models for real-time systems. We focus in this paper on the power of silent transitions, i.e. ε-transitions, in such automata. We show that ε-transitions strictly increase the power of timed automata and that the class of timed languages recognized by automata with ε-transitions is much more robust than the corresponding class without ε-transitions. Our main result shows that these transitions increase the power of these automata only if they reset clocks.


Finite Automaton Repeated State Empty Word Visible Transition Observable Action 
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, Dill D., N. Halbwachs, and H. Wong-Toi. Minimization of timed transition systems. In Proceedings of CONCUR'92, LNCS 630, 1992.Google Scholar
  2. 2.
    R. Alur, C. Courcoubetis, and T.A. Henzinger. The observational power of clocks. In Proceedings of CONCUR'94, LNCS 836, pages 162–177, 1994.Google Scholar
  3. 3.
    R. Alur and D.L. Dill. Automata for modeling real-time systems. In Proceedings of ICALP'90, LNCS 443, pages 322–335, 1990.Google Scholar
  4. 4.
    R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.CrossRefGoogle Scholar
  5. 5.
    R. Alur, L. Fix, and T.A. Henzinger. A determinizable class of timed automata. In Proceedings of CAV'94, LNCS 818, pages 1–13, 1994.Google Scholar
  6. 6.
    R. Alur and T.A. Henzinger. Back to the future: towards a theory of timed regular languages. In Proceedings of FOCS'92, LNCS, pages 177–186, 1992.Google Scholar
  7. 7.
    B. Bérard. Untiming timed languages. Information Processing Letters, 55:129–135, 1995.CrossRefGoogle Scholar
  8. 8.
    B. Bérard, P. Gastin, and A. Petit. On the power of non observable actions in timed automata. Tech. Rep. 95.08, ENS de Cachan, LIFAC, 1995.Google Scholar
  9. 9.
    E. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal-logic specifications. ACM Trans. Programming Languages and Systems, 8:244–263, 1986.CrossRefGoogle Scholar
  10. 10.
    C. Courcoubetis and M. Yannakakis. Minimum and maximum delay problems in real-time systems. In Proceedings of CAV'91, LNCS 575, pages 399–409, 1991.Google Scholar
  11. 11.
    T. Henzinger, Z. Manna, and A. Pnueli. Temporal proofs methodologies for realtime systems. In Proceedings of POPL '91, pages 353–366, 1991.Google Scholar
  12. 12.
    T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information und Computation, 111(2):193–244, 1994.CrossRefGoogle Scholar
  13. 13.
    T.A. Henzinger, P.W. Kopke, and Wong Toi H., The expressive power of clocks. In Proceedings of ICALP'95, LNCS 944, pages 335–346, 1995.Google Scholar
  14. 14.
    N. Lynch and H. Attiya. Using mappings to prove timing properties. In Proceedings of PODC'90, pages 265–280, 1990.Google Scholar
  15. 15.
    X. Nicollin, J. Sifakis, and S. Yovine. From ATP to timed graphs and hybrid systems. In Proceedings of REX workshop ”Real-time: theory in practice”, LNCS 600, pages 549–572, 1991.Google Scholar
  16. 16.
    J. Ostroff. Temporal Logic of Real-time Systems. Research Studies Press, 1990.Google Scholar
  17. 17.
    C. Ramchandani. Analysis of asynchronous concurrent systems by petri nets. Technical report, Massachusetts Institute of Technology, 1974.Google Scholar
  18. 18.
    W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 133–191. Elsevier Science Publishers (North-Holland), 1990.Google Scholar
  19. 19.
    M. Vardi. Verification of concurrent-programs — the automata-theoretic framework. In Proceedings of LICS'87, pages 167–176, 1987.Google Scholar
  20. 20.
    P. Wolper, M. Vardi, and A.P. Sistla. Reasoning about infinite computation paths. In Proceedings of FOCS'83, pages 185–194, 1983.Google Scholar
  21. 21.
    H. Wong-Toi and G. Hoffmann. The control of dense real-time discrete event systems. In Proceedings of the 30th IEEE Conf. on Decision and Control, pages 1527–1528, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Béatrice Bérard
    • 1
  • Paul Gastin
    • 2
  • Antoine Petit
    • 1
  1. 1.LIFACENS de CachanCachan CedexFrance
  2. 2.LITP - IBPUniversité Paris 7Paris Cedex 05France

Personalised recommendations