×

Reachability computation for polynomial dynamical systems. (English) Zbl 1360.93084

Summary: This paper is concerned with the problem of computing the bounded time reachable set of a polynomial discrete-time dynamical system. The problem is well-known for being difficult when nonlinear systems are considered. In this regard, we propose three reachability methods that differ in the set representation. The proposed algorithms adopt boxes, parallelotopes, and parallelotope bundles to construct flowpipes that contain the actual reachable sets. The latter is a new data structure for the symbolic representation of polytopes. Our methods exploit the Bernstein expansion of polynomials to bound the images of sets. The scalability and precision of the presented methods are analyzed on a number of dynamical systems, in comparison with other existing approaches.

MSC:

93B03 Attainable sets, reachability
93C55 Discrete-time control/observation systems
93C10 Nonlinear systems in control theory
PDF BibTeX XML Cite
Full Text: DOI Link

References:

[1] Althoff M, Le Guernic C, Krogh BH (2011) Reachable set computation for uncertain time-varying linear systems. In: Hybrid systems: computation and control, HSCC. ACM, pp 93-102 · Zbl 1362.93013
[2] Anai H, Weispfenning V (2001) Reach set computations using real quantifier elimination. In: Hybrid systems: computation and control, HSCC, pp 63-76 · Zbl 0991.93008
[3] Asarin E, Bournez O, Dang T, Maler O (2000) Approximate reachability analysis of piecewise-linear dynamical systems. In: Hybrid systems: computation and control, HSCC. Springer, pp 20-31 · Zbl 0938.93502
[4] Ashraf Q, Galor O (2011) Cultural diversity, geographical isolation, and the origin of the wealth of nations. Technical report, National Bureau of Economic Research
[5] Balluchi A, Casagrande A, Collins P, Ferrari A, Villa T, Sangiovanni-Vincentelli AL (2006) Ariadne: a framework for reachability analysis of hybrid automata. In: Mathematical theory of networks and systems, MTNS. Citeseer · Zbl 1181.03035
[6] Batt, G; Yordanov, B; Weiss, R; Belta, C, Robustness analysis and tuning of synthetic gene networks, Bioinformatics, 23, 2415-2422, (2007)
[7] Berman S, Halász Á, Kumar V (2007) Marco: a reachability algorithm for multi-affine systems with applications to biological systems. In: Hybrid systems: computation and control, HSCC. Springer, pp 76-89 · Zbl 1221.93027
[8] Bernstein, SN, Démonstration du théorème de Weierstrass fondée sur le calcul des probabilités, Commun Soc Math Kharkov, 21, 1-2, (1912) · JFM 43.0301.03
[9] Berz, M; Makino, K, Verified integration of odes and flows using differential algebraic methods on high-order Taylor models, Reliab Comput, 4, 361-369, (1998) · Zbl 0976.65061
[10] Botchkarev O, Tripakis S (2000) Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations. In: Hybrid systems: computation and control, HSCC. Springer, pp 73-88 · Zbl 1037.93510
[11] Bournez O, Maler O, Pnueli A (1999) Orthogonal polyhedra: representation and computation. In: Hybrid systems: computation and control, HSCC. Springer, pp 46-60 · Zbl 0947.68154
[12] Casagrande A, Dreossi, T (2013) pyhybrid analysis: a package for semantics analysis of hybrid systems. In: Digital system design, DSD, pp 815-818. doi:10.1109/DSD.2013.143 · Zbl 0595.92011
[13] Casagrande, A; Dreossi, T; Fabriková, J; Piazza, C, \(ϵ \)-semantics computations on biological systems, Inf Comput, 236, 35-51, (2014) · Zbl 1312.68127
[14] Chen L, Miné A, Wang J, Cousot P (2009) Interval polyhedra: an abstract domain to infer interval linear relationships. In: Static analysis symposium, SAS, pp 309-325 · Zbl 1248.68140
[15] Chen X, Ábrahám E (2011) Choice of directions for the approximation of reachable sets for hybrid systems. In: International conference on computer aided systems theory, EUROCAST. Springer, pp 535-542
[16] Chen X, Abraham E, Sankaranarayanan S (2012) Taylor model flowpipe construction for non-linear hybrid systems. In: Real-time systems symposium, RTSS. IEEE, pp 183-192 · JFM 53.0517.01
[17] Chen X, Ábrahám E, Sankaranarayanan S (2013) Flow*: an analyzer for non-linear hybrid systems. In: Computer aided verification, CAV, pp 258-263 · Zbl 1151.92018
[18] Chutinan A, Krogh BH (1998) Computing polyhedral approximations to flow pipes for dynamic systems. In: Conference on decision and control, CDC, vol 2. IEEE, pp 2089-2094 · JFM 52.0450.05
[19] Chutinan A, Krogh BH (1999) Computing approximating automata for a class of linear hybrid systems. In: Hybrid systems V. Springer, pp. 16-37 · Zbl 0928.93026
[20] Chutinan A, Krogh BH (1999) Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations. In: Hybrid systems: computation and control, HSCC. Springer, pp 76-90 · Zbl 0954.93020
[21] Coxeter HSM (1973) Regular polytopes. Courier Corporation, North Chelmsford · Zbl 0031.06502
[22] da Cunha AEC (2015) Benchmark: quadrotor attitude control. In: Applied verification for continuous and hybrid systems, ARCH
[23] Dang T (2006) Approximate reachability computation for polynomial systems. In: Hybrid systems: computation and control, HSCC. Springer, pp 138-152 · Zbl 1178.93068
[24] Dang T, Dreossi T, Piazza C (2014) Parameter synthesis using parallelotopic enclosure and applications to epidemic models. In: Hybrid systems and biology, HSB, pp 67-82
[25] Dang T, Dreossi T, Piazza C (2015) Parameter synthesis through temporal logic specifications. In: Formal methods, FM, pp 213-230
[26] Dang, T; Testylier, R, Reachability analysis for polynomial dynamical systems using the Bernstein expansion, Reliab Comput, 17, 128-152, (2012)
[27] Dang TXT (2000) Verification and synthesis of hybrid systems. PhD thesis, Institut National Polytechnique de Grenoble-INPG
[28] Davis PJ, Rabinowitz P (2007) Methods of numerical integration. Courier Corporation, North Chelmsford · Zbl 1139.65016
[29] Dreossi T (2016) Sapo. http://tommasodreossi.github.io/sapo/
[30] Dreossi T (2016) Sapo: A tool for the reachability computation and parameter synthesis of polynomial dynamical systems. HSCC (in press) · Zbl 1369.68257
[31] Dreossi T, Dang T (2014) Parameter synthesis for polynomial biological models. In: Hybrid systems: computation and control, HSCC, pp 233-242 · Zbl 1362.92023
[32] Eggers, A; Ramdani, N; Nedialkov, NS; Fränzle, M, Improving the sat modulo ODE approach to hybrid systems analysis by combining different enclosure methods, Softw Syst Model, 14, 121-148, (2012) · Zbl 1350.68231
[33] Farouki, RT, The Bernstein polynomial basis: a centennial retrospective, Comput Aided Geom Des, 29, 379-419, (2012) · Zbl 1252.65039
[34] Frehse G (2005) Phaver: algorithmic verification of hybrid systems past hytech. In: Hybrid systems: computation and control, HSCC. Springer, pp 258-273 · Zbl 1078.93533
[35] Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O (2011) Spaceex: scalable verification of hybrid systems. In: Computer aided verification, CAV. Springer, pp 379-395 · Zbl 0976.65061
[36] Galor O (2007) Discrete dynamical systems. Springer Science & Business Media, Berlin · Zbl 1107.37002
[37] Gao S (2012) Computable analysis, decision procedures, and hybrid automata: a new framework for the formal verification of cyber-physical systems. PhD thesis, PhD thesis, Carnegie Mellon University
[38] Garloff, J; Smith, AP, Investigation of a subdivision based algorithm for solving systems of polynomial equations, Nonlinear Anal Theory Methods Appl, 47, 167-178, (2001) · Zbl 1042.65526
[39] Girard A (2005) Reachability of uncertain linear systems using zonotopes. In: Hybrid systems: computation and control, HSCC. Springer, pp 291-305 · Zbl 1078.93005
[40] Girard A, Le Guernic C, Maler O (2006) Efficient computation of reachable sets of linear time-invariant systems with inputs. In: Hybrid systems: computation and control, HSCC. Springer, pp 257-271 · Zbl 1178.93024
[41] Gropp, W; Lusk, E; Doss, N; Skjellum, A, A high-performance, portable implementation of the mpi message passing interface standard, Parallel Comput, 22, 789-828, (1996) · Zbl 0875.68206
[42] Henzinger TA, Ho PH, Wong-Toi H (1997) Hytech: a model checker for hybrid systems. In: Computer aided verification, CAV. Springer, pp 460-463 · Zbl 1060.68603
[43] Hildebrand FB (1987) Introduction to numerical analysis. Courier Corporation, North Chelmsford · Zbl 0641.65001
[44] Jódar, L; Villanueva, RJ; Arenas, AJ; González, GC, Nonstandard numerical methods for a mathematical model for influenza disease, Math Comput Simul, 79, 622-633, (2008) · Zbl 1151.92018
[45] Karp RM (1972) Reducibility among combinatorial problems. Springer, Berlin · Zbl 0366.68041
[46] Kermack, WO; McKendrick, AG, A contribution to the mathematical theory of epidemics, R Soc Lond A Math Phys Eng Sci, 115, 700-721, (1927) · JFM 53.0517.01
[47] Klipp E, Herwig R, Kowald A, Wierling C, Lehrach H (2008) Systems biology in practice: concepts, implementation and application. Wiley, New York
[48] Kong S, Gao S, Chen W, Clarke E (2015) dreach: \(δ \)-reachability analysis for hybrid systems. In: Tools and algorithms for the construction and analysis of systems, TACAS. Springer, pp 200-205
[49] Kostousova, E, State estimation for dynamic systems via parallelotopes optimization and parallel computations, Optim Methods Softw, 9, 269-306, (1998) · Zbl 0919.93017
[50] Kostousovat, EK, Control synthesis via parallelotopes: optimzation and parallel compuations, Optim Methods Softw, 4, 267-310, (2001) · Zbl 0998.93014
[51] Kot, M, Discrete-time travelling waves: ecological examples, J Math Biol, 30, 413-436, (1992) · Zbl 0825.92126
[52] Kot, M; Schaffer, WM, Discrete-time growth-dispersal models, Math Biosci, 80, 109-136, (1986) · Zbl 0595.92011
[53] Krommer AR (1994) Numerical integration: on advanced computer systems, vol 848. Springer Science & Business Media, Berlin · Zbl 0825.65012
[54] Kurzhanski, AB; Varaiya, P, Ellipsoidal techniques for reachability analysis: internal approximation, Syst Control Lett, 41, 201-211, (2000) · Zbl 1031.93014
[55] Kurzhanskiy AA, Varaiya P, et al (2006) Ellipsoidal toolbox. EECS Department, University of California, Berkeley, Technical report UCB/EECS-2006-46
[56] Kvasnica M, Grieder P, Baotić M, Morari M (2004) Multi-parametric toolbox (mpt). In: Hybrid systems: computation and control. HSCC, Springer, pp 448-462 · Zbl 1135.93332
[57] Lafferriere, G; Pappas, GJ; Yovine, S, Symbolic reachability computation for families of linear vector fields, J Symb Comput, 32, 231-253, (2001) · Zbl 0983.93004
[58] Le Guernic C (2009) Reachability analysis of hybrid systems with linear continuous dynamics. PhD thesis, Université Joseph-Fourier-Grenoble I · Zbl 1242.93059
[59] Guernic, C; Girard, A, Reachability analysis of linear systems using support functions, Nonlinear Anal Hybrid Syst, 4, 250-262, (2010) · Zbl 1201.93018
[60] Lotka AJ (1925) Elements of physical biology. Williams & Wilkins Company · Zbl 1031.93014
[61] Mourrain, B; Pavone, JP, Subdivision methods for solving polynomial equations, J Symb Comput, 44, 292-306, (2009) · Zbl 1158.13010
[62] Nataraj, P; Arounassalame, M, A new subdivision algorithm for the Bernstein polynomial approach to global optimization, Int J Autom Comput, 4, 342-352, (2007)
[63] Nvidia CUDA (2008) Programming guide, Nvida · Zbl 1201.93018
[64] Platzer A (2007) Differential dynamic logic for verifying parametric hybrid systems. In: Automated reasoning with analytic tableaux and related methods, TABLEAUX, pp 216-232 · Zbl 1132.68478
[65] Platzer, A, Differential dynamic logic for hybrid systems, J Autom Reason, 41, 143-189, (2008) · Zbl 1181.03035
[66] Platzer A, Quesel J (2008) Keymaera: a hybrid theorem prover for hybrid systems (system description). In: International joint conference on automated reasoning, IJCAR, pp 171-178 · Zbl 1165.68469
[67] Pol, B, Lxxxviii. on “relaxation-oscillations”, Lond Edinb Dublin Philos Mag J Sci, 2, 978-992, (1926) · JFM 52.0450.05
[68] Prabhakar P, Viswanathan M (2011) A dynamic algorithm for approximate flow computations. In: Hybrid systems: computation and control, HSCC, HSCC ’11. ACM, New York, NY, USA, pp 133-142. doi:10.1145/1967701.1967722 · Zbl 1362.93019
[69] Rössler, OE, An equation for continuous chaos, Phys Lett A, 57, 397-398, (1976) · Zbl 1371.37062
[70] Rössler, OE, An equation for hyperchaos, Phys Lett A, 71, 155-157, (1979) · Zbl 0996.37502
[71] Sankaranarayanan S, Dang T, Ivančić F (2008) Symbolic model checking of hybrid systems using template polyhedra. In: Tools and algorithms for the construction and analysis of systems, TACAS. Springer, pp. 188-202 · Zbl 1134.68419
[72] Sankaranarayanan S, Sipma HB, Manna Z (2005) Scalable analysis of linear systems using mathematical programming. In: Verification, model checking, and abstract interpretation, VMCAI, pp 25-41 · Zbl 1111.68514
[73] Sassi MAB, Sankaranarayanan S (2015) Bernstein polynomial relaxations for polynomial optimization problems. arXiv preprint arXiv:1509.01156 · Zbl 1312.68127
[74] Sassi MAB, Testylier R, Dang T, Girard A (2012) Reachability analysis of polynomial systems using linear programming relaxations. In: Automated technology for verification and analysis, ATVA, pp 137-151 · Zbl 1375.68077
[75] Shisha, O, The Bernstein form of a polynomial, J Res Natl Bur Stand Math Math Phys B, 70, 79, (1966) · Zbl 0139.10003
[76] Stursberg O, Krogh BH (2003) Efficient representation and computation of reachable sets for hybrid systems. In: Hybrid systems: computation and control, HSCC. Springer, pp 482-497 · Zbl 1032.93037
[77] Varaiya, P; Inan, M (ed.); Kurshan, R (ed.), Reach set computation using optimal control, No. 170, 323-331, (2000), Berlin · Zbl 0957.68066
[78] Volterra V (1927) Variazioni e fluttuazioni del numero d’individui in specie animali conviventi. C Ferrari · JFM 52.0450.06
[79] Wildenberg, J; Vano, J; Sprott, J, Complex spatiotemporal dynamics in Lotka-Volterra ring systems, Ecol Complex, 3, 140-147, (2006)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.