Abstract
We describe new techniques to construct, and subsequently refine, over-approximations of the reachability sets for linear dynamical systems. Our approach extracts information from real eigenvectors and more generally, from certain vectors in the primary decomposition, to generate suitable invariants of the system and can be used in conjunction with other reachability computation methods. We also describe experimental results from using this technique inside the qualitative abstraction tool [18], where it helps to generate refined abstractions of hybrid systems with linear continuous dynamics. We illustrate this on a collision-avoidance example from automobile cruise control problem, which was handled completely automatically by our tool.
Research supported in part by DARPA under the MoBIES program administered by AFRL under contract F33615-00-C-1700 and NASA Langley Research Center contract NAS1-00108 to Rannoch Corporation.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
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):3–34, 1995.
R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.
Rajeev Alur, Tom Henzinger, Gerardo Lafferriere, and George J. Pappas. Discrete abstractions of hybrid systems. Proceedings of the IEEE, 88(2):971–984, July 2000.
H. Anai and V. Weispfenning. Reach set computations using real quantifier elimination. In M. D. Di Benedetto and A. L. Sangiovanni-Vincentelli, editors, HSCC, volume 2034 of Lecture Notes in Computer Science, pages 63–76. Springer, 2001.
A. Chutinan and B. H. Krogh. Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations. In Vaandrager and van Schuppen [19], pages 76–90.
T. Dang and O. Maler. Reachability analysis via face lifting. In T. A. Henzinger and S. Sastry, editors, HSCC, volume 1386 of LNCS, pages 96–109. Springer, 1998.
D. Godbole and J. Lygeros. Longitudinal control of the lead car of a platoon. IEEE Transactions on Vehicular Technology, 43(4):1125–35, 1994.
T. A. Henzinger, P. W. Kopke, A. Puri, and P. Varaiya. What’s decidable about hybrid automata? Journal of Computer and System Sciences, 57:94–124, 1998. A preliminary version appeared in the Proc. of the 27th Annual ACM Symposium on Theory of Computing (STOC 1995), pp. 373-382.
K. Hoffman and R. Kunze. Linear Algebra. Prentice-Hall, second edition, 1971.
M. Jirstrand. Algebraic methods for modeling and design in control. Licentiate thesis LIU-TEK-LIC-1996:05 Linköping Studies in Science and Technology. Thesis No 540, Department of Electrical Engineering, Li, 1996.
A. B. Kurzhanski and P. Varaiya. Ellipsoidal techniques for reachability analysis. In Lynch and Krogh [14], pages 202–214.
G. Lafferriere, G. J. Pappas, and S. Yovine. A new class of decidable hybrid systems. In Vaandrager and van Schuppen [19], pages 137–151.
G. Lafferriere, G. J. Pappas, and S. Yovine. Symbolic reachability computations for families of linear vector fields. J. Symbolic Computation, 32(3):231–253, 2001.
N. A. Lynch and B. H. Krogh, editors. Hybrid Systems: Computation and Control, Third International Workshop, HSCC 2000, Proceedings, volume 1790 of LNCS. Springer, 2000.
I. Mitchell and C. Tomlin. Level set methods for computation in hybrid systems. In Lynch and Krogh [14].
A. Puri and P. Varaiya. Decidability of hybrid systems with rectangular differential inclusions. In D. L. Dill, editor, Computer Aided Verification, CAV, volume 818 of LNCS, pages 95–104. Springer Verlag, 1994.
A. Puri and P. Varaiya. Driving safely in smart cars. In Proceedings of the 1995 American Control Conference, 1995
A. Tiwari and G. Khanna. Series of abstractions for hybrid automata. In C. Tomlin and M. R. Greenstreet, editors, HSCC, volume 2289 of Lecture Notes in Computer Science, pages 465–478. Springer, 2002.
F. W. Vaandrager and J. H. van Schuppen, editors. Hybrid Systems: Computation and Control, Second International Workshop, HSCC’99, Proceedings, volume 1569 of Lecture Notes in Computer Science. Springer, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tiwari, A. (2003). Approximate Reachability for Linear Systems. In: Maler, O., Pnueli, A. (eds) Hybrid Systems: Computation and Control. HSCC 2003. Lecture Notes in Computer Science, vol 2623. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36580-X_37
Download citation
DOI: https://doi.org/10.1007/3-540-36580-X_37
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00913-9
Online ISBN: 978-3-540-36580-8
eBook Packages: Springer Book Archive