Skip to main content
SpringerLink
Log in
Book cover

International Conference on Concurrency Theory

CONCUR 2000: CONCUR 2000 — Concurrency Theory pp 138–152Cite as

The Impressive Power of Stopwatches

  • Conference paper
  • First Online:

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

Abstract

In this paper we define and study the class of stopwatch automata which are timed automata augmented with stopwatches and unobservable behaviour. In particular, we investigate the expressive power of this class of automata, and show as a main result that any finite or infinite timed language accepted by a linear hybrid automaton is also acceptable by a stopwatch automaton. The consequences of this result are two-fold: firstly, it shows that the seemingly minor upgrade from timed automata to stopwatch automata immediately yields the full expressive power of linear hybrid automata. Secondly, reachability analysis of linear hybrid automata may effectively be reduced to reachability analysis of stopwatch automata. This, in turn, may be carried out using an easy (over-approximating) extension of the efficient reachability analysis for timed automata to stopwatch automata. We report on preliminary experiments on analyzing translations of linear hybrid automata using a stopwatch-extension of the real-time verification tool UPPAAL.

This work is partially supported by the European Community Esprit-LTR Project 26270 VHS (Verification of Hybrid systems) and by the FIREworks Esprit WG 23531; it was carried out while the first author was visiting BRICS@Aalborg during the fall 1999.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. ABK+97._E. Asarin, M. Bozga, A. Kerbrat, O. Maler, A. Pnueli, and A. Rasse. Data-Structures for the Verification of Timed Automata. In Proc. of HART’97, LNCS 1201, 1997.

    Google Scholar 

  2. Rajeev Alur, Costas Courcoubetis, and Thomas A. Henzinger. The observational power of clocks. In Bengt Jonsson and Joachim Parrow, editors, CONCUR’ 94: Concurrency Theory, 5th International Conference, volume 836 of Lecture Notes in Computer Science, pages 162–177, Uppsala, Sweden, 22–25August 1994. Springer-Verlag.

    Chapter  Google Scholar 

  3. ACH+95._R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science B, 137, January 1995.

    Google Scholar 

  4. Rajeev Alur and David Dill. A theory of timed automata. Theoretical Computer Science B, 126:183–235, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  5. Rajeev Alur, Thomas A. Henziger, and Hei-Hsin Ho. Automatic symbolic verification of embedded systems. IEEE Transactions On Software Engineering, 22(3):181–201, March 1996.

    Google Scholar 

  6. A. Puri and P. Varaiya. Decidability of hybrid systems with rectangular differential inclusions. In David L. Dill, editor, Proceedings of the sixth International Conference on Computer-Aided Verification CAV, volume 818 of Lecture Notes in Computer Science, pages 95–104, Standford, California, USA, June 1994. Springer-Verlag.

    Google Scholar 

  7. A. Bouajjani and R. Robbana. Verifying omeg-regular properties for a subclass of linear hybrid systems. In P. Wolper, editor, Proceedings of the 7th International Conference On Computer Aided Verification, volume 939 of Lecture Notes in Computer Science, pages 437–450, Liege, Belgium, July 1995. Springer Verlag.

    Google Scholar 

  8. Patricia Bouyer, Christine Dufourd, Eric Fleury, and Antoine Petit. Decidable updatable timed automata are bisimilar to timed automata. Research report, LSV, ENS Cachan, 2000. Forthcoming.

    Google Scholar 

  9. B. Bérard, V. Diekert, P. Gastin, and A. Petit. Characterization of the expressive power of silent transitions in timed automata. Fundamenta Informaticœ, 36:145–182, 1998.

    MATH  Google Scholar 

  10. B. Bérard and L. Fribourg. Automated verification of a parametric real-time program: the ABR conformance protocol. In Proc. 11th Int. Conf. Computer Aided Verification (CAV’99), Trento, Italy, July 1999, volume 1633 of Lecture Notes in Computer Science, pages 96–107. Springer, 1999.

    Google Scholar 

  11. Béatrice Berard, Paul Gastin, and Antoine Petit. On the power of non-observable actions in timed automata. In 13th Annual Symposium on Theoretical Aspects of Computer Science, volume 1046 of lncs, pages 257–268, Grenoble, France, 22–24 February 1996. Springer.

    Google Scholar 

  12. BLP+99._Gerd Behrmann, Kim G. Larsen, Justin Pearson, Carsten Weise, and Wang Yi. Efficient timed reachability analysis using clock difference diagrams. In 11th Computer-Aided Verification, Trento, Italy, July 1999.

    Google Scholar 

  13. K. Cerans. Algorithmic problems in analysis in analysis of real-time specifications. PhD thesis, University of Latvia, 1992.

    Google Scholar 

  14. Volker Diekert, Paul Gastin, and Antoine Petit. Removing ε-transitions in timed automata. In R. Reischuk, editor, Proceedings of the 14th Annual Symposium on Theoretical Aspects of Computer Science 1997, number 1200 in Lecture Notes in Computer Science, pages 583–594, Berlin-Heidelberg-New York, 1997. Springer.

    Google Scholar 

  15. Thomas A. Henzinger. The theory of hybrid automata. In Proceedings, 11 th Annual IEEE Symposium on Logic in Computer Science, pages 278–292, New Brunswick, New Jersey, 27–30 July 1996. IEEE Computer Society Press.

    Google Scholar 

  16. Thomas A. Henzinger and Peter W. Kopke. State equivalences for rectangular hybrid automata. In Ugo Montanari and Vladimiro Sassone, editors, CONCUR’ 96: Concurrency Theory, 7th International Conference, volume 1119 of Lecture Notes in Computer Science, pages 530–545, Pisa, Italy, 26–29 August 1996. Springer-Verlag.

    Google Scholar 

  17. Thomas A. Henzinger and Peter W. Kopke. Discrete-time control for rectangular hybrid automata. In Pierpaolo Degano, Robert Gorrieri, and Alberto Marchetti-Spaccamela, editors, Automata, Languages and Programming, 24th International Colloquium, volume 1256 of Lecture Notes in Computer Science, pages 582–593, Bologna, Italy, 7–11 July 1997. Springer-Verlag.

    Google Scholar 

  18. Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. What’s decidable about hybrid automata? Journal of Computer and System Sciences, 57(1):94–124, August 1998.

    Google Scholar 

  19. Thomas A. Henzinger, Peter W. Kopke, and Howard Wong-Toi. The expressive power of clocks. In Zoltán Fülöp and Ferenc Gécseg, editors, Automata, Languages and Programming, 22nd International Colloquium, volume 944 of Lecture Notes in Computer Science, pages 417–428, Szeged, Hungary, 10–14 July 1995. Springer-Verlag.

    Google Scholar 

  20. J. McManis and P. Varaiya. Suspension automata: A decidable class of hybrid automata. In David L. Dill, editor, Proceedings of the sixth International Conference on Computer-Aided Verification CAV, volume 818 of Lecture Notes in Computer Science, pages 105–117, Standford, California, USA, June 1994. Springer-Verlag.

    Google Scholar 

  21. K. J. Kristoffersen, K. G. Larsen, P. Pettersson, and C. Weise. Verification of an experimental batch plant. VHS internal document.

    Google Scholar 

  22. Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Integration graphs: A class of decidable hybrid systems. In R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, editors, Hybrid Systems, volume 736 of Lecture Notes in Computer Science, pages 179–208. Springer-Verlag, 1993.

    Google Scholar 

  23. K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. Efficient verification of real-time systems: Compact data structure and state-space reduction. In Proc. of the 18th IEEE Real-Time Systems Symposium, RTSS’97. IEEE Computer Society Press, December 1997.

    Google Scholar 

  24. K. G. Larsen, P. Pettersson, and W. Yi. UPPAAL in a Nutshell. Journal of Software Tools for Technology Transfer, 1(1/2):134–152, October 1997.

    Google Scholar 

  25. S. Yovine. Kronos: A Verification Tool for real-Time Systems. Journal of Software Tools for Technology Transfer, 1(1/2):123–133, October 1997.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IRCCyN/CNRS UMR 6597, France

    Franck Cassez

  2. Dep. of Computer Science, Aalborg University, Denmark

    Kim Larsen

Authors
  1. Franck Cassez
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kim Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, Pennsylvania State University, 220 Pond Laboratory, University Park, PA, 16802-6106, USA

    Catuscia Palamidessi

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cassez, F., Larsen, K. (2000). The Impressive Power of Stopwatches. In: Palamidessi, C. (eds) CONCUR 2000 — Concurrency Theory. CONCUR 2000. Lecture Notes in Computer Science, vol 1877. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44618-4_12

Download citation

  • DOI: https://doi.org/10.1007/3-540-44618-4_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67897-7

  • Online ISBN: 978-3-540-44618-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation