Abstract
This paper is concerned with a method for computing reachable sets of linear continuous systems with uncertain input. Such a method is required for verification of hybrid systems and more generally embedded systems with mixed continuous-discrete dynamics. In general, the reachable sets of such systems (except for some linear systems with special eigenstructures) are hard to compute exactly and are thus often over-approximated. The approximation accuracy is important especially when the computed over-approximations do not allow proving a property. In this paper we address the problem of refining the reachable set approximation by adding redundant constraints which allow bounding the reachable sets in some critical directions. We introduce the notion of directional distance which is appropriate for measuring approximation effectiveness with respect to verifying a safety property. We also describe an implementation of the reachability algorithm which favors the constraint-based representation over the vertex-based one and avoids expensive conversions between them. This implementation allowed us to treat systems of much higher dimensions. We finally report some experimental results showing the performance of the refinement algorithm.
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
Althoff, M., Stursberg, O., Buss, M.: Reachability Analysis of Nonlinear Systems with Uncertain Parameters using Conservative Linearization. In: CDC 2008 (2008)
Asarin, E., Dang, T., Maler, O.: The d/dt tool for verification of hybrid systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 365–370. Springer, Heidelberg (2002)
Asarin, E., 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. 21–31. Springer, Heidelberg (2000)
Avis, D., Fukuda, K.: A pivoting algorithm for convex hulls and vertex enumeration of arrangements and polyhedra. Discrete and Computational Geometry 8(1), 295–313 (1992)
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)
Chutinan, A., Krogh, B.H.: Computational Techniques for Hybrid System Verification. IEEE Trans. on Automatic Control 48, 64–75 (2003)
Cameron, S.A., Culley, R.K.: Determining the Minimum Translational Distance between Two Convex Polyhedra. Proceedings of International Conference on Robotics and Automation 48, 591–596 (1986)
Dang, T.: Verification and Synthesis of Hybrid Systems. PhD Thesis, INPG (2000)
Frehse, G.: PHAVER: Algorithmic Verification of Hybrid Systems past HYTECH. International Journal on Software Tools for Technology Transfer (STTT) 10(3) (June 2008)
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)
Le Guernic, C., Girard, A.: Reachability Analysis of Hybrid Systems Using Support Functions. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 540–554. Springer, Heidelberg (2009)
Girard, A., Le Guernic, C., Maler, O.: Efficient Computation of Reachable Sets of Linear Time-invariant Systems with Inputs. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 257–271. Springer, Heidelberg (2006)
Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HYTECH: A model checker for hybrid systems. Software Tools for Technology Transfer 1(1-2), 110–122 (1997)
Kalman, R.E., Falb, P.L., Arbib, M.A.: Topics in Mathematical System Theory. McGraw-Hill Book Company, New York (1968)
Kostoukova, E.K.: State Estimation for dynamic systems via parallelotopes: Optimization and Parallel Computations. Optimization Methods and Software 9, 269–306 (1999)
Kvasnica, M., Grieder, P., Baotic, M., Morari, M.: Multi-Parametric Toolbox (MPT). In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 448–462. Springer, Heidelberg (2004)
Kurzhanski, A., 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)
Kurzhanskiy, A., Varaiya, P.: Ellipsoidal Techniques for Reachability Analysis of Discrete-time Linear Systems. IEEE Trans. Automatic Control 52, 26–38 (2007)
Larsen, K., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Software Tools for Technology Transfert 1(1-2), 134–152 (1997)
Lin, M.C., Manocha, D.: Collision and proximity queries. In: Handbook of Discrete and Computational Geometry (2003)
Pappas, G., Lafferriere, G., Yovine, S.: A new class of decidable hybrid systems. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 29–31. Springer, Heidelberg (1999)
Sankaranarayanan, S., Dang, T., Ivancic, F.: Symbolic model checking of hybrid systems using template polyhedra. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 188–202. Springer, Heidelberg (2008)
Stursberg, O., Krogh, B.H.: Efficient Representation and Computation of Reachable Sets for Hybrid Systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 482–497. Springer, Heidelberg (2003)
Varaiya, P.: Reach Set computation using Optimal Control. In: KIT Workshop, Verimag, Grenoble, pp. 377–383 (1998)
Yovine, S.: KRONOS: A verification tool for real-time systems. Software Tools for Technology Transfer 1(1-2), 123–133 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Asarin, E., Dang, T., Maler, O., Testylier, R. (2010). Using Redundant Constraints for Refinement. In: Bouajjani, A., Chin, WN. (eds) Automated Technology for Verification and Analysis. ATVA 2010. Lecture Notes in Computer Science, vol 6252. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15643-4_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-15643-4_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15642-7
Online ISBN: 978-3-642-15643-4
eBook Packages: Computer ScienceComputer Science (R0)