Skip to main content
SpringerLink
Log in

Reachability Analysis of Hybrid Systems via Predicate Abstraction

  • Conference paper
  • First Online:
Hybrid Systems: Computation and Control (HSCC 2002)

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

Included in the following conference series:

Abstract

Predicate abstraction has emerged to be a powerful technique for extracting finite-state models from infinite-state discrete programs. Th is paper presents algorithms and tools for reachability analysis of hybrid systems by combining the notion of predicate abstraction with recent techniques for approximating the set of reachable states of linear systems using polyhedra.Giv en a hybrid system and a set of userde fined boolean predicates, we consider the finite discrete quotient whose states correspond to all possible truth assignments to the input predicates. T he tool performs an on-the-fly exploration of the abstract system. We demonstrate the feasibility of the proposed technique by analyzing a parametric timing-based mutual exclusion protocol and safety of a simple controller for vehicle coordination.

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

Access this chapter

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3–34, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  2. R. Alur, T. Dang, J. Esposito, R. Fierro, Y. Hur, F. Ivančić, V. Kumar, I. Lee, P. Mishra, G. Pappas, and O. Sokolsky. Hierarchical hybrid modeling of embedded systems.In Embedded Software, First Intern. Workshop, LNCS 2211. 2001.

    Google Scholar 

  3. R. Alur, T. Henzinger, G. Lafferriere, and G. Pappas. Discrete abstractions of hybrid systems. Proceedings of the IEEE, 2000.

    Google Scholar 

  4. A. Annichini, E. Asarin, and A. Bouajjani. Symbolic techniques for parametric reasoning about counter and clock systems.In Comp. Aided Verification, 2000.

    Google Scholar 

  5. E. Asarin, O. Bournez, T. Dang, and O. Maler. Approximate reachability analysis of piecewise-linear dynamical systems.In Hybrid Systems: Computation and Control, Third International Workshop, LNCS 1790, pages 21–31. 2000.

    Google Scholar 

  6. T. Ball and S. Rajamani. Bebop: A symbolic model checker for boolean programs. In SPIN 2000 Workshop on Model Checking of Software, LNCS 1885. 2000.

    Google Scholar 

  7. A. Chutinan and B.K. Krogh. Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations.In Hybrid Systems: Computation and Control, Second International Workshop, LNCS 1569, pages 76–90. 1999.

    Google Scholar 

  8. E.M. Clarke and R.P. Kurshan. Computer-aided verification. IEEE Spectrum, 33(6):61–67, 1996.

    Article  Google Scholar 

  9. J. C. Corbett, M. B. Dwyer, J. Hatcli., S. Laubach, C.S. Pasareanu, Robby, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In Proceedings of 22nd Intern. Conf. on Software Engineering. 2000.

    Google Scholar 

  10. S. Das, D. Dill, and S. Park. Experience with predicate abstraction. In Computer Aided Verification, 11th International Conference, LNCS 1633, 1999.

    Google Scholar 

  11. C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool kronos.In Hybrid Systems III: Verification and Control, LNCS 1066, 1996.

    Google Scholar 

  12. D. Godbole and J. Lygeros. Longitudinal control of a lead card of a platoon. IEEE Transactions on Vehicular Technology, 43(4):1125–1135, 1994.

    Article  MathSciNet  Google Scholar 

  13. S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In Proc. 9th Conference on Computer Aided Verification, volume 1254, 1997.

    Google Scholar 

  14. M. Greenstreet and I. Mitchell. Reachability analysis using polygonal projections. In Hybrid Systems: Computation and Control, Second Intern. Workshop, LNCS 1569. 1999.

    Google Scholar 

  15. N. Halbwachs, Y. Proy, and P. Raymond. Verification of linear hybrid systems by means of convex approximations.I n Intern. Symposium on Static Analysis, LNCS 864. 1994.

    Google Scholar 

  16. T.A. Henzinger, P. Ho, and H. Wong-Toi. HyTech: the next generation.In Proceedings of the 16th IEEE Real-Time Systems Symposium, pages 56–65, 1995.

    Google Scholar 

  17. G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279–295, 1997.

    Article  MathSciNet  Google Scholar 

  18. G.J. Holzmann and M.H. Smith. Automating software feature verification. Bell Labs Technical Journal, 5(2):72–87, 2000.

    Article  Google Scholar 

  19. A. Kurzhanski and P. Varaiya. Ellipsoidal techniques for reachability analysis. In Hybrid Systems:Computation and Control, Third Intern. Workshop, LNCS 1790. 2000.

    Google Scholar 

  20. K. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell. Springer International Journal of Software Tools for Technology Transfer, 1, 1997.

    Google Scholar 

  21. I. Mitchell and C. Tomlin. Level set methods for computation in hybrid systems.I n Hybrid Systems:Computation and Control, Third Intern. Workshop, volume LNCS 1790. 2000.

    Book  Google Scholar 

  22. A. Puri and P. Varaiya. Driving safely in smart cars. Technical Report UBC-ITSPRR-95–24, California PATH, University of California in Berkeley, July 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer and Information Science, University of Pennsylvania, USA

    Rajeev Alur, Thao Dang & Franjo Ivančić

Authors
  1. Rajeev Alur
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thao Dang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Franjo Ivančić
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Aeronautics and Astronautics, Stanford University, 250 Durand Building MC4035, 94305-4035, Stanford, CA, USA

    Claire J. Tomlin

  2. Department of Computer Science, University of British Columbia, 201-2366 Main Mall, V6T1Z4, Vancouver BC, Canada

    Mark R. Greenstreet

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Alur, R., Dang, T., Ivančić, F. (2002). Reachability Analysis of Hybrid Systems via Predicate Abstraction. In: Tomlin, C.J., Greenstreet, M.R. (eds) Hybrid Systems: Computation and Control. HSCC 2002. Lecture Notes in Computer Science, vol 2289. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45873-5_6

Download citation

  • DOI: https://doi.org/10.1007/3-540-45873-5_6

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-45873-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation