Skip to main content
SpringerLink
Log in

On the power of non-observable actions in timed automata

  • Conference paper
  • First Online:
STACS 96 (STACS 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1046))

Included in the following conference series:

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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. 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. 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. R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.

    Article  Google Scholar 

  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. 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. B. Bérard. Untiming timed languages. Information Processing Letters, 55:129–135, 1995.

    Article  Google Scholar 

  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. 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.

    Article  Google Scholar 

  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. 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. T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information und Computation, 111(2):193–244, 1994.

    Article  Google Scholar 

  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. N. Lynch and H. Attiya. Using mappings to prove timing properties. In Proceedings of PODC'90, pages 265–280, 1990.

    Google Scholar 

  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. J. Ostroff. Temporal Logic of Real-time Systems. Research Studies Press, 1990.

    Google Scholar 

  17. C. Ramchandani. Analysis of asynchronous concurrent systems by petri nets. Technical report, Massachusetts Institute of Technology, 1974.

    Google Scholar 

  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. M. Vardi. Verification of concurrent-programs — the automata-theoretic framework. In Proceedings of LICS'87, pages 167–176, 1987.

    Google Scholar 

  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. 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 

Download references

Author information

Authors and Affiliations

  1. LIFAC, ENS de Cachan, 61 av. du Prés. Wilson, F-94235, Cachan Cedex, France

    Béatrice Bérard & Antoine Petit

  2. LITP - IBP, Université Paris 7, 2, place Jussieu, F-75251, Paris Cedex 05, France

    Paul Gastin

Authors
  1. Béatrice Bérard
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Paul Gastin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Antoine Petit
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Claude Puech Rüdiger Reischuk

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bérard, B., Gastin, P., Petit, A. (1996). On the power of non-observable actions in timed automata. In: Puech, C., Reischuk, R. (eds) STACS 96. STACS 1996. Lecture Notes in Computer Science, vol 1046. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60922-9_22

Download citation

  • DOI: https://doi.org/10.1007/3-540-60922-9_22

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60922-3

  • Online ISBN: 978-3-540-49723-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation