Abstract
We use linear hybrid automata to define linear approximations of the phase portraits of nonlinear hybrid systems. The approximating automata can be analyzed automatically using the symbolic model checker HyTech. We demonstrate the technique through the study of predator-prey systems, where we compute population bounds for both species. We also identify a class of nonlinear hybrid automata for which linear phase-portrait approximations can be generated automatically.
Keywords
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.
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 grants CCR-9200794 and CCR-9504469, by the AFOSR contract F49620-93-1-0056, and by the ARPA grant NAG2-892.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
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.
R. Alur, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. Hybrid Systems I, LNCS 736, pp. 209–229. Springer-Verlag, 1993.
R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. 14th Annual Real-time Systems Symposium, pp. 2–11. IEEE Computer Society Press, 1993.
V. I. Arnol'd. Geometric Methods in the Theory of Ordinary Differential Equations. Springer-Verlag, New York, 1983.
P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. 4th Annual Symposium on Principles of Programming Languages. ACM Press, 1977.
T.A. Henzinger. Hybrid automata with finite bisimulations. ICALP 95: Automata, Languages, and Programming, LNCS 944, pp. 324–335. Springer-Verlag, 1995.
T.A. Henzinger and P.-H. Ho. Algorithmic analysis of nonlinear hybrid systems. CAV 95: Computer-aided Verification, LNCS 939, pp. 225–238. Springer-Verlag, 1995.
T.A. Henzinger and P.-H. Ho. HyTech: The Cornell Hybrid Technology Tool. Hybrid Systems II, LNCS 999, pp. 265–293. Springer-Verlag, 1995.
T.A. Henzinger and P.-H. Ho. A note on abstract-interpretation strategies for hybrid automata. Hybrid Systems II, LNCS 999, pp. 252–264. Springer-Verlag, 1995.
T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: the next generation. 16th Annual Real-time Systems Symposium, pp. 56–65. IEEE Computer Society Press, 1995.
T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. A user guide to HyTech. TACAS 95: Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1019, pp. 41–71. Springer-Verlag, 1995. Full version available as Technical Report CSD-TR-95-1532, Cornell University (write to hytech@cs.cornell.edu, or check http://www.cs.cornell.edu/Info/People/tah/hytech.html).
T.A. Henzinger, P.W. Kopke, A. Puri, and P. Varaiya. What's decidable about hybrid automata? 27th Annual Symposium on Theory of Computing, pp. 373–382. ACM Press, 1995.
N. Halbwachs, P. Raymond, and Y.-E. Proy. Verification of linear hybrid systems by means of convex approximation. SAS 94: Static Analysis Symposium, LNCS 864, pp. 223–237. Springer-Verlag, 1994.
M.W. Hirsch and S. Smale. Differential Equations, Dynamical Systems, and Linear Algebra. Academic Press, 1974.
P.-H. Ho and H. Wong-Toi. Automated analysis of an audio control protocol. CAV95: Computer-aided Verification, LNCS 939, pp. 381–394. Springer-Verlag, 1995.
A.J. Lotka. Analytical note on certain rhythmic relations in organic systems. Proceedings of the National Academy of Sciences of the United States of America, 6:410–415, 1920.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Henzinger, T.A., Wong-Toi, H. (1996). Linear phase-portrait approximations for nonlinear hybrid systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds) Hybrid Systems III. HS 1995. Lecture Notes in Computer Science, vol 1066. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0020961
Download citation
DOI: https://doi.org/10.1007/BFb0020961
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61155-4
Online ISBN: 978-3-540-68334-6
eBook Packages: Springer Book Archive