Abstract
This work is concerned with the problem of computing the set of reachable states for linear time-invariant systems with bounded inputs. Our main contribution is a novel algorithm which improves significantly the computational complexity of reachability analysis. Algorithms to compute over and under-approximations of the reachable sets are proposed as well. These algorithms are not subject to the wrapping effect and therefore our approximations are tight. We show that these approximations are useful in the context of hybrid systems verification and control synthesis. The performance of a prototype implementation of the algorithm confirms its qualities and gives hope for scaling up verification technology for continuous and hybrid systems.
This work was partially supported by the European Community projects IST-2001-33520 CC (Control and Computation) and IST-2003-507219 PROSYD (Property-based System Design) as well as by the project CalCel of région Rhône-Alpes.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The Algorithmic Analysis of Hybrid Systems. Theoretical Computer Science 138, 3–34 (1995)
Asarin, A., Bournez, O., Dang, T., Maler, O.: Approximate Reachability Analysis of Piecewise-linear Dynamical Systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 20–31. Springer, Heidelberg (2000)
Asarin, E., Bournez, O., Dang, T., Maler, O., Pnueli, A.: Effective Synthesis of Switching Controllers for Linear Systems. Proceedings of the IEEE 88, 1011–1025 (2000)
Asarin, E., Dang, T., Girard, A.: Reachability Analysis of Nonlinear Systems using Conservative Approximation. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 20–35. Springer, Heidelberg (2003)
Asarin, E., Maler, O., Pnueli, A.: Reachability Analysis of Dynamical Systems having Piecewise-Constant Derivatives. Theoretical Computer Science 138, 35–65 (1995)
Botchkarev, O., Tripakis, S.: Verification of Hybrid Systems with Linear Differential Inclusions using Ellipsoidal Approximations. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 73–88. Springer, Heidelberg (2000)
The Caml Language webpage (2005), http://caml.inria.fr/
Chutinan, A., Krogh, B.H.: Computing Polyhedral Approximations to Dynamic Flow Pipes. In: CDC 1998, IEEE, Los Alamitos (1998)
Chutinan, A., Krogh, B.H.: Verification of Polyhedral-invariant Hybrid Automata using Polygonal Flow Pipe Approximations. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 76–90. Springer, Heidelberg (1999)
Chutinan, A., Krogh, B.H.: Computational Techniques for Hybrid System Verification. IEEE Trans. on Automatic Control 48, 64–75 (2003)
Coppersmith, D., Winograd, S.: Matrix Multiplication via Arithmetic Progressions. J. Symbolic Computation 9, 251–280 (1990)
Dang, T.: Verification and Synthesis of Hybrid Systems, PhD thesis, Institut National Polytechnique de Grenoble, Laboratoire Verimag (2000)
Dang, T., Maler, O.: Reachability Analysis via Face Lifting. In: Henzinger, T.A., Sastry, S.S. (eds.) HSCC 1998. LNCS, vol. 1386, pp. 96–109. Springer, Heidelberg (1998)
PHAVer: Algorithmic Verification of Hybrid Systems Past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005)
Girard, A.: Reachability of Uncertain Linear Systems using Zonotopes. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 291–305. Springer, Heidelberg (2005)
Greenstreet, M.R.: Verifying Safety Properties of Differential Equations. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 277–287. Springer, Heidelberg (1996)
Greenstreet, M.R., Mitchell, I.: Reachability Analysis using Polygonal Projections. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 103–116. Springer, Heidelberg (1999)
Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: Hytech: A Model Checker for Hybrid Systems. Software Tools for Technology Transfer 1, 110–122 (1997)
Kühn, W.: Rigorously Computed Orbits of Dynamical Systems without the Wrapping Rffect. Computing 61, 47–68 (1998)
Kühn, W.: Towards an Optimal Control of the Wrapping Effect. In: SCAN 1998, Developments in Reliable Computing, pp. 43–51. Kluwer, Dordrecht (1999)
Kurzhanski, A., Valyi, I.: Ellipsoidal Calculus for Estimation and Control. Birkhauser (1997)
Kurzhanski, A.B., Varaiya, P.: Ellipsoidal Techniques for Reachability Analysis. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 202–214. Springer, Heidelberg (2000)
Maler, O.: Control from Computer Science. Annual Reviews in Control 26, 175–187 (2002)
Mitchell, I., Tomlin, C.: Level Set Methods for Computation in Hybrid Systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 310–323. Springer, Heidelberg (2000)
Varaiya, P.: Reach Set computation using Optimal Control. In: KIT Workshop, Verimag, Grenoble, pp. 377–383 (1998)
Zaslavsky, T.: Facing Up to Arrangements: Face-Count Formulas for Partitions of Space by Hyperplanes. In: Memoirs of the AMS, vol. 154, American Mathematical Society (1975)
Vaandrager, F.W., van Schuppen, J.H. (eds.): HSCC 1999. LNCS, vol. 1569. Springer, Heidelberg (1999)
Lynch, N.A., Krogh, B.H. (eds.): HSCC 2000. LNCS, vol. 1790. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Girard, A., Le Guernic, C., Maler, O. (2006). Efficient Computation of Reachable Sets of Linear Time-Invariant Systems with Inputs. In: Hespanha, J.P., Tiwari, A. (eds) Hybrid Systems: Computation and Control. HSCC 2006. Lecture Notes in Computer Science, vol 3927. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11730637_21
Download citation
DOI: https://doi.org/10.1007/11730637_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33170-4
Online ISBN: 978-3-540-33171-1
eBook Packages: Computer ScienceComputer Science (R0)