Skip to main content
SpringerLink
Log in

Reachability verification for hybrid automata

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

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

Included in the following conference series:

Abstract

We study the reachability problem for hybrid automata. Automatic approaches, which attempt to construct the reachable region by symbolic execution, often do not terminate. In these cases, we require the user to guess the reachable region, and we use a theorem prover (Pvs) to verify the guess. We classify hybrid automata according to the theory in which their reachable region can be defined finitely. This is the theory in which the prover needs to operate in order to verify the guess. The approach is interesting, because an appropriate guess can often be deduced by extrapolating from the first few steps of symbolic execution.

This research was supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA grant NAG2-892, and by the SRC contract 95-DC-324.036.

Supported by Lavoisier grant of the French Foreign Affairs Ministry and by SRI.

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. ACH+5. 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:3–34, 1995.

    Google Scholar 

  2. R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.

    Article  Google Scholar 

  3. R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verificationof embedded systems. IEEE Ransactions on Software Engineering, 22(3):181–201, 1996.

    Google Scholar 

  4. B. Boigelot, L. Bronne, and S. Rassart. An improved reachability analysis method for strongly linear hybrid systems. In Proc. of the 9th Conference on Computer-Aided Verification, CAV'97, LNCS 1254, pages 167–178. Springer-Verlag, 1997.

    Google Scholar 

  5. A. Burgue≈no and V. Rusu. Task-system analysis using slope-parametric hybrid automata. In Proc. of the 3rd Conference on Parallel Processing, Euro-Par'97, LNCS 1300, pages 1262–1273. Springer-Verlag, 1997.

    Google Scholar 

  6. B. Boigelot and P. Wolper. Symbolic verification with periodic sets. In Proc. of the 6th Conference on Computer-Aided Verification, CAV'94, LNCS 818, pages 55–67. Springer-Verlag, 1994.

    Google Scholar 

  7. Z. Chaochen, C.A.R. Hoare, and A.P. Ravn. A calculus of durations. Information Processing Letters, 40:269–276, 1991.

    Google Scholar 

  8. T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. Algorithmic analysis of nonlinear hybrid systems. IEEE Transactions on Automatic Control, 1998. To appear.

    Google Scholar 

  9. T.A. Henzinger, P.W. Kopke, A. Puri, and P. Varaiya. What's decidable about hybrid automata? In Proc. of the 27th Annual ACM Symposium on Theory of Computing, STOC'95, pages 373–382, 1995.

    Google Scholar 

  10. N. Halbwachs, Y.-E. Proy, and P. Raymond. Verification of linear hybrid systems by means of convex approximations. In Proc. of the 1st Static Analysis Symposium, SAS'94, LNCS 864, pages 223–237. Springer-Verlag, 1994.

    Google Scholar 

  11. M. Jaffe, N. Levenson, M. Heimdahl, and B. Melhart. Software requirements analysis for real-time process-control systems. IEEE Transactions on Software Engineering, 17(3):241–258, 1991.

    Google Scholar 

  12. Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Integration graphs: a class of decidable hybrid systems. In Proc. of the 1st Workshop on Theory of Hybrid Systems, LNCS 736, pages 179–208. Springer-Verlag, 1993.

    Google Scholar 

  13. S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. Pvs: Combining specification, proof checking, and model checking. In Proc. of the 8th Conference on Computer-Aided Verification, CAV.'96, LNCS 1102, pages 411–414. Springer-Verlag, 1996.

    Google Scholar 

  14. O. Roux and V. Rusu. Uniformity for the decidability of hybrid automata. In Proc. of the 3rd Static Analysis Symposium, SAS'96, LNCS 1145, pages 301–316. Springer-Verlag, 1996.

    Google Scholar 

  15. Jan Vitt and Josef Hooman. Assertional specification and verification using Pvs of the steam boiler control system. In Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, LNCS 1165, pages 453–472. Springer-Verlag, 1996.

    Google Scholar 

  16. G. M. Ziegler. Lectures on Polytopes, volume 152 of Graduate Texts in Mathematics. Springer-Verlag, 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. EECS Department, University of California, Berkeley, CA

    Thomas A. Henzinger

  2. SRI International, Computer Science Laboratory, Menlo Park, CA

    Vlad Rusu

Authors
  1. Thomas A. Henzinger
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vlad Rusu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Thomas A. Henzinger Shankar Sastry

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Henzinger, T.A., Rusu, V. (1998). Reachability verification for hybrid automata. In: Henzinger, T.A., Sastry, S. (eds) Hybrid Systems: Computation and Control. HSCC 1998. Lecture Notes in Computer Science, vol 1386. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-64358-3_40

Download citation

  • DOI: https://doi.org/10.1007/3-540-64358-3_40

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64358-6

  • Online ISBN: 978-3-540-69754-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation