Abstract
In this paper we propose a new method for reachability analysis of the class of discrete-time polynomial dynamical systems. Our work is based on the approach combining the use of template polyhedra and optimization [25, 7]. These problems are non-convex and are therefore generally difficult to solve exactly. Using the Bernstein form of polynomials, we define a set of equivalent problems which can be relaxed to linear programs. Unlike using affine lower-bound functions in [7], in this work we use piecewise affine lower-bound functions, which allows us to obtain more accurate approximations. In addition, we show that these bounds can be improved by increasing artificially the degree of the polynomials. This new method allows us to compute more accurately guaranteed over-approximations of the reachable sets of discrete-time polynomial dynamical systems. We also show different ways to choose suitable polyhedral templates. Finally, we show the merits of our approach on several examples.
Keywords
- Polynomial System
- Linear Programming Relaxation
- Bernstein Polynomial
- Reachability Analysis
- Polynomial Optimization
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 work was supported by the Agence Nationale de la Recherche (VEDECY project - ANR 2009 SEGI 015 01).
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
Asarin, E., Dang, T., Girard, A.: Hybridization methods for the analysis of nonlinear systems. Acta Informatica 43(7), 451–476 (2007)
Bernstein, S.: Collected Works, vol. 1. USSR Academy of Sciences (1952)
Bernstein, S.: Collected Works, vol. 2. USSR Academy of Sciences (1954)
Dang, T.: Approximate Reachability Computation for Polynomial Systems. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 138–152. Springer, Heidelberg (2006)
Dang, T., Le Guernic, C., Maler, O.: Computing Reachable States for Nonlinear Biological Models. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 126–141. Springer, Heidelberg (2009)
Dang, T., Maler, O., Testylier, R.: Accurate hybridization of nonlinear systems. In: HSCC 2010, pp. 11–20 (2010)
Dang, T., Salinas, D.: Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 219–232. Springer, Heidelberg (2009)
FitzHugh, R.: Impulses and physiological states in theoretical models of nerve membrane. Biophysical J. 1, 445–466 (1961)
Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: Scalable Verification of Hybrid Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011)
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)
Halasz, A., Kumar, V., Imielinski, M., Belta, C., Sokolsky, O., Pathak, S., Rubin, H.: Analysis of lactose metabolism in e.coli using reachability analysis of hybrid systems. IET Systems Biology 1(2), 130–148 (2007)
Han, Z., Krogh, B.H.: Reachability Analysis of Large-Scale Affine Systems Using Low-Dimensional Polytopes. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 287–301. Springer, Heidelberg (2006)
Horst, R., Tuy, H.: Global optimazation: Deterministic approaches, 2nd edn. Springer (1993)
Jaulin, L., Kieffer, M., Didrit, O., Walter, E.: Applied Interval Analysis. Springer (2001)
Kaynama, S., Oishi, M., Mitchell, I., Dumont, G.A.: The continual reachability set and its computation using maximal reachability techniques. In: CDC (2011)
Kloetzer, M., Belta, C.: Reachability Analysis of Multi-affine Systems. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 348–362. Springer, Heidelberg (2006)
Lasserre, J.B.: Global optimization with polynomials and the problem of moments. SIAM Journal of Optimization 11(3), 796–817 (2001)
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)
Lin, Q., Rokne, J.G.: Interval approxiamtions of higher order to the ranges of functions. Computers Math 31, 101–109 (1996)
Martin, R., Shou, H., Voiculescu, I., Bowyer, A., Wang, G.: Comparison of interval methods for plotting algebraic curves. Computer Aided Geometric Design (19), 553–587 (2002)
Mitchell, I., Tomlin, C.J.: 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)
Nedialkov, N.S., Jackson, K.R., Corliss, G.F.: Validated solutions of initial value problems for ordinary differential equations. Applied Mathematics and Computation (105), 21–68 (1999)
Platzer, A., Clarke, E.M.: The Image Computation Problem in Hybrid Systems Model Checking. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 473–486. Springer, Heidelberg (2007)
Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Transactions on Automatic Control 52(8), 1415–1429 (2007)
Sankaranarayanan, S., Dang, T., Ivančić, 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)
Sherali, H.D., Tuncbilek, C.H.: A global optimization algorithm for polynomial programming using a reformulation-linearization technique. Journal of Global Optimization 2, 101–112 (1991)
Sherali, H.D., Tuncbilek, C.H.: New reformulation-linearization/convexification relaxations for univariate and multivariate polynomial programming problems. Operation Research Letters 21, 1–9 (1997)
Tiwari, A., Khanna, G.: Nonlinear Systems: Approximating Reach Sets. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 600–614. Springer, Heidelberg (2004)
Yordanov, B., Belta, C.: Cdc. In: A Formal Verification Approach to the Design of Synthetic Gene Networks (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ben Sassi, M.A., Testylier, R., Dang, T., Girard, A. (2012). Reachability Analysis of Polynomial Systems Using Linear Programming Relaxations. In: Chakraborty, S., Mukund, M. (eds) Automated Technology for Verification and Analysis. ATVA 2012. Lecture Notes in Computer Science, vol 7561. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33386-6_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-33386-6_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33385-9
Online ISBN: 978-3-642-33386-6
eBook Packages: Computer ScienceComputer Science (R0)