From duration calculus to linear hybrid automata

Extended abstract
  • Ahmed Bouajjani
  • Yassine Lakhnech
  • Riadh Robbana
Session 7: Invited Titorial
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)


We relate two different approaches for the specification and verification of hybrid systems. The first one is logic-based and uses the framework of the Calculus of Durations (CoD), the second one is automata-based and uses algorithmic analysis techniques for hybrid automata. Fragments of CoD have been identified in [13, 19] for the description of control systems and their requirements. We mainly show that the problem of verifying that a CoD control design satisfies a CoD requirement is decidable. This is proved by reducing this verification problem to the reachability problem for a subclass of linear hybrid automata where this problem is decidable.


Hybrid System Atomic Proposition Hybrid Automaton State Formula Boolean Combination 
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.


  1. 1.
    R. Alur, C. Courcoubetis, and D. Dill. Model-Checking for Real-Time Systems. In LICS'90. IEEE, 1990.Google Scholar
  2. 2.
    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. TCS, 138, 1995.Google Scholar
  3. 3.
    R. Alur, C. Courcoubetis, T. Henzinger, and P-H. Ho. Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. In Hybrid Systems. LNCS 736, 1993.Google Scholar
  4. 4.
    R. Alur, C. Courcoubetis, and T. A. Henzinger. Computing Accumulated Delays in Real-time Systems. In CAV'93. LNCS 697, 1993.Google Scholar
  5. 5.
    R. Alur and D. Dill. A Theory of Timed Automata. TCS, 126, 1994.Google Scholar
  6. 6.
    A. Bouajjani, R. Echahed, and R. Robbana. Verifying Invariance Properties of Timed Systems with Duration Variables. In FTRTFT'94. LNCS 863, 1994.Google Scholar
  7. 7.
    A. Bouajjani, R. Echahed, and J. Sifakis. On Model Checking for Real-Time Properties with Durations. In LICS'93. IEEE, 1993.Google Scholar
  8. 8.
    A. Bouajjani and R. Robbana. Verifying ω-Regular Properties for Subclasses of Linear Hybrid Systems. In CAV'95. This Volume, 1995.Google Scholar
  9. 9.
    K. Cerans. Decidability of Bisimulation Equivalence for Parallel Timer Processes. In CAV'92. LNCS 663, 1992.Google Scholar
  10. 10.
    Z. Chaochen, C.A.R. Hoare, and A.P. Ravn. A Calculus of Durations. IPL, 40:269–276, 1991.Google Scholar
  11. 11.
    Z. Chaochen and X. Li. A Mean-Value Duration Calculus. In A Classical Mind, Essays in Honour of C.A.R. Hoare. Prentice-Hall, 1994.Google Scholar
  12. 12.
    Z. Chaouchen, M.R. Hansen, and P. Sestoft. Decidability and Undecidability Results for Duration Calculus. In STACS'93. LNCS 665, 1993.Google Scholar
  13. 13.
    J. He, C.A.R. Hoare, M. Fränzle, M. Müller-Olm, E.R. Olderog, M. Schenke, M.R. Hansen, A.P. Ravn, and H. Rishel. Provably Correct Systems. In FTRTFT'94. LNCS 863, 1994.Google Scholar
  14. 14.
    T.A. Henzinger, P.W. Kopke, A. Puri, and P. Varaiya. What's Decidable about Hybrid Automata. In STOC'95, 1995.Google Scholar
  15. 15.
    T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic Model-Checking for Real-Time Systems. In LICS'92. IEEE, 1992.Google Scholar
  16. 16.
    Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Integration Graphs: A Class of Decidable Hybrid Systems. In Hybrid Systems. LNCS 736, 1993.Google Scholar
  17. 17.
    O. Maler, Z. Manna, and A. Pnueli. From Timed to Hybrid Systems. In REX workshop on Real-Time: Theory and Practice. LNCS 600, 1992.Google Scholar
  18. 18.
    X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. An Approach to the Description and Analysis of Hybrid Systems. In Hybrid Systems. LNCS 736, 1993.Google Scholar
  19. 19.
    A. Ravn. Design of Embedded Real-time Computing Systems. Unpublished Notes, 1994.Google Scholar
  20. 20.
    A.P. Ravn, H. Rischel, and K.M. Hansen. Specifying and Verifying Requirements of Real-Time Systems. In Trans. on Soft. Eng. IEEE, 1993.Google Scholar
  21. 21.
    W. Thomas. Automata on Infinite Objects. In Handbook of Theo. Comp. Sci. Elsevier Sci. Pub., 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Ahmed Bouajjani
    • 1
  • Yassine Lakhnech
    • 2
  • Riadh Robbana
    • 1
  1. 1.Miniparc-ZirstVERIMAGMontbonnot St-MartinFrance
  2. 2.Institut für Informatik und Praktische Mathematik Christian-Albrechts-Universität zu KielKielGermany

Personalised recommendations