Skip to main content
SpringerLink
Log in

Hybrid automata with finite bisimulations

  • Automata and Formal Languages II
  • Conference paper
  • First Online:
Automata, Languages and Programming (ICALP 1995)

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

Included in the following conference series:

Abstract

The analysis, verification, and control of hybrid automata with finite bisimulations can be reduced to finite-state problems. We advocate a time-abstract, phase-based methodology for checking if a given hybrid automaton has a finite bisimulation. First, we factor the automaton into two components, a boolean automaton with a discrete dynamics on the finite state space \(\mathbb{B}\) m and a euclidean automaton with a continuous dynamics on the infinite state space ℝn. Second, we investigate the phase portrait of the euclidean component. In this fashion, we obtain new decidability results for hybrid systems as well as new, uniform proofs of known decidability results.

This research was supported in part by the NSF grant CCR-9200794, by the AFOSR contract F49620-93-1-0056, and by the DARPA grant NAG2-892.

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. R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3–34, 1995.

    Google Scholar 

  2. R. Alur, C. Courcoubetis, T.A. Henzinger, P.-H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. Hybrid Systems, Springer LNCS 736, pp. 209–229, 1993.

    Google Scholar 

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

    Google Scholar 

  4. R. Alur, T.A. Henzinger, P.-H. Ho. Automatic symbolic verification of embedded systems. IEEE Real-time Systems Symp., pp. 2–11, 1993.

    Google Scholar 

  5. P. Abdulla, B. Jonsson. Verifying programs with unreliable channels. IEEE Symp. Logic in Computer Science, pp. 160–170, 1993.

    Google Scholar 

  6. A. Bouajjani, R. Echahed, R. Robbana. Verifying invariance properties of timed systems with duration variables. Formal Techniques in Real-time and Fault-tolerant Systems, Springer LNCS 863, pp. 193–210, 1994.

    Google Scholar 

  7. A. Bouajjani, J.-C. Fernandez, N. Halbwachs. Minimal model generation. Computer-aided Verification, Springer LNCS 531, pp. 197–203, 1990.

    Google Scholar 

  8. A. Bouajjani, R. Robbana. Verifying Ω-regular properties for subclasses of linear hybrid systems. Computer-aided Verification, Springer LNCS, 1995.

    Google Scholar 

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

    Google Scholar 

  10. T.A. Henzinger, P.-H. Ho. Model-checking strategies for linear hybrid systems. Workshop on Hybrid Systems and Autonomous Control (Ithaca, NY), 1994.

    Google Scholar 

  11. T.A. Henzinger, P.-H. Ho. Algorithmic analysis of nonlinear hybrid systems. Computer-aided Verification, Springer LNCS, 1995.

    Google Scholar 

  12. T.A. Henzinger, P. Kopke, A. Puri, P. Varaiya. What's decidable about hybrid automata? ACM Symp. Theory of Computing, 1995.

    Google Scholar 

  13. T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111:193–244, 1994.

    Google Scholar 

  14. N. Halbwachs, P. Raymond, and Y.-E. Proy. Verification of linear hybrid systems by means of convex approximation. Static Analysis Symp., Springer LNCS 864, 1994.

    Google Scholar 

  15. Y. Kesten, A. Pnueli, J. Sifakis, S. Yovine. Integration graphs: a class of decidable hybrid systems. Hybrid Systems, Springer LNCS 736, pp. 179–208, 1993.

    Google Scholar 

  16. P.C. Kanellakis, S.A. Smolka. CCS expressions, finite-state processes, and three problems of equivalence. Information and Computation, 86:43–68, 1990.

    Google Scholar 

  17. D. Lee, M. Yannakakis. Online minimization of transition systems. ACM Symp. Theory of Computing, pp. 264–274, 1992.

    Google Scholar 

  18. O. Maler, A. Pnueli. Reachability analysis of planar multi-linear systems. Computer-aided Verification, Springer LNCS 697, pp. 194–209, 1993.

    Google Scholar 

  19. O. Maler, A. Pnueli, J. Sifakis. On the synthesis of discrete controllers for timed systems. Theoretical Aspects of Computer Science, Springer LNCS, 1995.

    Google Scholar 

  20. J. McManis, P. Varaiya. Suspension automata: a decidable class of hybrid automata. Computer-aided Verification, Springer LNCS 818, pp. 105–117, 1994.

    Google Scholar 

  21. X. Nicollin, A. Olivero, J. Sifakis, S. Yovine. An approach to the description and analysis of hybrid systems. Hybrid Systems, Springer LNCS 736, pp. 149–178, 1993.

    Google Scholar 

  22. A. Olivero, J. Sifakis, S. Yovine. Using abstractions for the verification of linear hybrid systems. Computer-aided Verification, Springer LNCS 818, pp. 81–94, 1994.

    Google Scholar 

  23. R. Paige, R.E. Tarjan. Three partition-refinement algorithms. SIAM J. Computing, 16:973–989, 1987.

    Google Scholar 

  24. A. Puri, P. Varaiya. Decidability of hybrid systems with rectangular differential inclusions. Computer-aided Verification, Springer LNCS 818, pp. 95–104, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Cornell University, 14850, Ithaca, NY

    Thomas A. Henzinger

Authors
  1. Thomas A. Henzinger
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Zoltán Fülöp Ferenc Gécseg

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Henzinger, T.A. (1995). Hybrid automata with finite bisimulations. In: Fülöp, Z., Gécseg, F. (eds) Automata, Languages and Programming. ICALP 1995. Lecture Notes in Computer Science, vol 944. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60084-1_85

Download citation

  • DOI: https://doi.org/10.1007/3-540-60084-1_85

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60084-8

  • Online ISBN: 978-3-540-49425-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation