Abstract
This paper is concerned with the problem of computing the image of a set by a polynomial function. Such image computations constitute a crucial component in typical tools for set-based analysis of hybrid systems and embedded software with polynomial dynamics, which found applications in various engineering domains. One typical example is the computation of all states reachable from a given set in one step by a continuous dynamics described by a differential or difference equation. We propose a new algorithm for over-approximating such images based on the Bernstein expansion of polynomial functions. The images are stored using template polyhedra. Using a prototype implementation, the performance of the algorithm was demonstrated on two practical systems as well as a number of randomly generated examples.
Chapter PDF
Similar content being viewed by others
Keywords
- Hybrid System
- Polynomial System
- Multivariate Polynomial
- Polynomial Optimization
- Polynomial Optimization Problem
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.
References
Asarin, E., Dang, T., Girard, A.: Hybridization methods for the analysis of nonlinear systems. Acta Informatica 43(7), 451–476 (2007)
Boyd, S., Vandenberghe, S.: Convex optimization. Cambridge Uni. Press, Cambridge (2004)
Clauss, F., Yu, C.I.: Application of symbolic approach to the Bernstein expansion for program analysis and optimization. Program. Comput. Softw. 30(3), 164–172 (2004)
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., Salinas, D.: Computing set images of polynomias. Technical report, VERIMAG (June 2008)
Fotiou, I.A., Rostalski, P., Parrilo, P.A., Morari, M.: Parametric optimization and optimal control using algebraic geometriy methods. Int. Journal of Control 79(11), 1340–1358 (2006)
Garloff, J.: Application of Bernstein expansion to the solution of control problems. University of Girona, pp. 421–430 (1999)
Garloff, J., Jansson, C., Smith, A.P.: Lower bound functions for polynomials. Journal of Computational and Applied Mathematics 157, 207–225 (2003)
Garloff, J., Smith, A.P.: An improved method for the computation of affine lower bound functions for polynomials. In: Frontiers in Global Optimization. Series Nonconvex Optimization and Its Applications. Kluwer Academic Publ., Dordrecht (2004)
Garloff, J., Smith, A.P.: A comparison of methods for the computation of affine lower bound functions for polynomials. In: Jermann, C., Neumaier, A., Sam, D. (eds.) COCOS 2003. LNCS, vol. 3478, pp. 71–85. Springer, Heidelberg (2005)
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)
He, F., Yeung, L.F., Brown, M.: Discrete-time model representation for biochemical pathway systems. IAENG Int. Journal of Computer Science 34(1) (2007)
Henrion, D., Lasserre, J.B.: Gloptipoly: Global optimization over polynomials with matlab and sedumi. In: Proceedings of CDC (2002)
Jolliffe, I.T.: Principal Component Analysis. Springer, Heidelberg (2002)
Jordan, D.W., Smith, P.: Nonlinear Ordinary Differential Equations. Oxford Applied Mathematics and Computer Science. Oxford Uni. Press, Oxford (1987)
Mourrain, B., Pavone, J.P.: Subdivision methods for solving polynomial equations. Technical report, INRIA Research report, 5658 (August. 2005)
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.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477–492. Springer, Heidelberg (2004)
Sankaranarayanan, S., Sipma, H., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25–41. Springer, Heidelberg (2005)
Sankaranarayanan, S.: Mathematical analysis of programs. Technical report, Standford, PhD thesis (2005)
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)
Seidel, H.-P.: Polar forms and triangular B-spline surfaces. In: Blossoming: The New Polar-Form Approach to Spline Curves and Surfaces, SIGGRAPH 1991 (1991)
Tchoupaeva, I.: A symbolic approach to Bernstein expansion for program analysis and optimization. In: Duesterwald, E. (ed.) CC 2004. LNCS, vol. 2985, pp. 120–133. Springer, Heidelberg (2004)
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)
Vandenberghe, S., Boyd, S.: Semidefinite programming. SIAM Review 38(1), 49–95 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dang, T., Salinas, D. (2009). Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion. In: Bouajjani, A., Maler, O. (eds) Computer Aided Verification. CAV 2009. Lecture Notes in Computer Science, vol 5643. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02658-4_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-02658-4_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02657-7
Online ISBN: 978-3-642-02658-4
eBook Packages: Computer ScienceComputer Science (R0)