An improved reachability analysis method for strongly linear hybrid systems (extended abstract)

  • Bernard Boigelot
  • Louis Bronne
  • Stéphane Rassart
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


This paper addresses the exact computation of the set of reachable states of a strongly linear hybrid system. It proposes an approach that is an extension of classical state-space exploration. This approach uses a new operation, based on a cycle analysis in the control graph of the system, for generating sets of reachable states, as well as a powerful representation system for sets of values. The method broadens the range of hybrid systems for which a finite and exact representation of the set of reachable states can be computed. In particular, the state-space exploration may be performed even if the set of variable values reachable at a given control location cannot be expressed as a finite union of convex regions. The technique is illustrated on a very simple example.


Control Location Hybrid System Reachable State Finite Union Convex Region 
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. [ACD93]
    R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2–34, May 1993.Google Scholar
  2. [ACH+95]
    R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138(1):3–34, 6 February 1995.Google Scholar
  3. [ACHH93]
    R. Alur, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems I, volume 736 of Lecture Notes in Computer Science, pages 209–229. Springer-Verlag, 1993.Google Scholar
  4. [AD94]
    R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183–235, 25 April 1994. Fundamental Study.Google Scholar
  5. [AHH96]
    R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering, 22(3):181–201, 1996.Google Scholar
  6. [BG96]
    B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite state spaces using QDDs. In Proc. Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 1–12, New-Brunswick, NJ, USA, July 1996. Springer-Verlag.Google Scholar
  7. [BLL+95]
    J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. UPPAAL — a tool suite for automatic verification of real-time systems. In Proceedings of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, New Brunswick, New Jersey, October 1995.Google Scholar
  8. [Büc62]
    J. R. Büchi. On a decision method in restricted second order arithmetic. In Logic, Methodology and Philosophy of Science, Proceedings of the 1960 International Congress, Stanford, California, 1962. Stanford Univ. Press.Google Scholar
  9. [BW94]
    B. Boigelot and P. Wolper. Symbolic verification with periodic sets. In Computer Aided Verification, Proc. 6th Int. Conference, Stanford, California, June 1994. Lecture Notes in Computer Science, Springer-Verlag.Google Scholar
  10. [DOTY96]
    C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool Kronos. In Hybrid Systems HI, Verification and Control, volume 1066 of Lecture Notes in Computer Science. Springer-Verlag, 1996.Google Scholar
  11. [DY95]
    C. Daws and S. Yovine. Two examples of verification of multirate timed automata with Kronos. In Proceedings of the 1995 IEEE Real-Time Systems Symposium, Pisa, Italy, 1995. IEEE Computer Society Press.Google Scholar
  12. [Eve79]
    S. Even. Graph Algorithms. Computer Science Press, 1979.Google Scholar
  13. [Hen96]
    T. 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
  14. [HH94]
    T.A. Henzinger and P.-H. Ho. Model-checking strategies for linear hybrid systems. Technical Report CSD-TR-94-1437, Cornell University, 1994. Presented at the Seventh International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems (Austin, TX).Google Scholar
  15. [HH95]
    T.A. Henzinger and P.-H. Ho. HyTech: The Cornell Hybrid Technology Tool. In P. Antsaklis, A. Nerode, W. Kohn, and S. Sastry, editors, Hybrid Systems II, volume 999 of Lecture Notes in Computer Science, pages 265–293. Springer-Verlag, 1995.Google Scholar
  16. [HHWT95a]
    T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: the next generation. In Proceedings of the 16th Annual Real-time Systems Symposium, pages 56–65. IEEE Computer Society Press, 1995.Google Scholar
  17. [HHWT95b]
    T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. A user guide to HyTech. In E. Brinksma, W.R. Cleaveland, K.G. Larsen, T. Margaria, and B. Steffen, editors, TACAS 95: Tools and Algorithms for the Construction and Analysis of Systems, volume 1019 of Lecture Notes in Computer Science, pages 41–71. Springer-Verlag, 1995.Google Scholar
  18. [HKPV95]
    T.A. Henzinger, P.W. Kopke, A. Puri, and P. Varaiya. What's decidable about hybrid automata? In Proceedings of the 27th Annual Symposium on Theory of Computing, pages 373–382. ACM Press, 1995.Google Scholar
  19. [HNSY94]
    T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193–244, 1994. Special issue for LICS 92.Google Scholar
  20. [KPSY92]
    Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Integration graphs: a class of decidable hybrid systems. In Proceedings of Workshop on Theory of Hybrid Systems, volume 736 of Lecture Notes in Computer Science, pages 179–208, Lyngby, Denmark, 1992. Springer-Verlag.Google Scholar
  21. [LPY95]
    K. G. Larsen, P. Pettersson, and W. Yi. Model-checking for real-time systems. In Horst Reichel, editor, Proceedings of the 10th International Conference on Fundamentals of Computation Theory, volume 965 of Lecture Notes in Computer Science, pages 62–88, Dresden, Germany, August 1995. Springer-Verlag.Google Scholar
  22. [MY96]
    O. Maler and S. Yovine. Hardware timing verification using Kronos. In Proceedings of the IEEE 7th Israeli Conference on Computer Systems and Software Engineering, ICCBSSE'96. IEEE Computer Society Press, 1996.Google Scholar
  23. [WB95]
    P. Wolper and B. Boigelot. An automata-theoretic approach to Presburger arithmetic constraints. In Proc. Static Analysis Symposium, Lecture Notes in Computer Science, Glasgow, September 1995. Springer-Verlag.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Bernard Boigelot
    • 1
  • Louis Bronne
    • 1
  • Stéphane Rassart
    • 1
  1. 1.Institut MontefioreUniversité de LiègeLiège Sart-TihnanBelgium

Personalised recommendations