Abstract
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.
Similar content being viewed by others
Notes
A set of nonempty subsets of X whose union contains the given set X is called a cover of X.
References
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
Anai H, Weispfenning V (2001) Reach set computations using real quantifier elimination. In: Hybrid systems: computation and control, HSCC, pp 63–76
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
Ashraf Q, Galor O (2011) Cultural diversity, geographical isolation, and the origin of the wealth of nations. Technical report, National Bureau of Economic Research
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
Batt G, Yordanov B, Weiss R, Belta C (2007) Robustness analysis and tuning of synthetic gene networks. Bioinformatics 23(18):2415–2422
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
Bernstein SN (1912) Démonstration du théorème de weierstrass fondée sur le calcul des probabilités. Commun Soc Math Kharkov 21(4/5):1–2
Berz M, Makino K (1998) Verified integration of odes and flows using differential algebraic methods on high-order taylor models. Reliab Comput 4(4):361–369
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
Bournez O, Maler O, Pnueli A (1999) Orthogonal polyhedra: representation and computation. In: Hybrid systems: computation and control, HSCC. Springer, pp 46–60
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
Casagrande A, Dreossi T, Fabriková J, Piazza C (2014) \(\epsilon \)-semantics computations on biological systems. Inf Comput 236:35–51. doi:10.1016/j.ic.2014.01.011
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
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
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
Chen X, Ábrahám E, Sankaranarayanan S (2013) Flow*: an analyzer for non-linear hybrid systems. In: Computer aided verification, CAV, pp 258–263
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
Chutinan A, Krogh BH (1999) Computing approximating automata for a class of linear hybrid systems. In: Hybrid systems V. Springer, pp. 16–37
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
Coxeter HSM (1973) Regular polytopes. Courier Corporation, North Chelmsford
da Cunha AEC (2015) Benchmark: quadrotor attitude control. In: Applied verification for continuous and hybrid systems, ARCH
Dang T (2006) Approximate reachability computation for polynomial systems. In: Hybrid systems: computation and control, HSCC. Springer, pp 138–152
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
Dang T, Dreossi T, Piazza C (2015) Parameter synthesis through temporal logic specifications. In: Formal methods, FM, pp 213–230
Dang T, Testylier R (2012) Reachability analysis for polynomial dynamical systems using the Bernstein expansion. Reliab Comput 17(2):128–152
Dang TXT (2000) Verification and synthesis of hybrid systems. PhD thesis, Institut National Polytechnique de Grenoble-INPG
Davis PJ, Rabinowitz P (2007) Methods of numerical integration. Courier Corporation, North Chelmsford
Dreossi T (2016) Sapo. http://tommasodreossi.github.io/sapo/
Dreossi T (2016) Sapo: A tool for the reachability computation and parameter synthesis of polynomial dynamical systems. HSCC (in press)
Dreossi T, Dang T (2014) Parameter synthesis for polynomial biological models. In: Hybrid systems: computation and control, HSCC, pp 233–242
Eggers A, Ramdani N, Nedialkov NS, Fränzle M (2012) Improving the sat modulo ode approach to hybrid systems analysis by combining different enclosure methods. Softw Syst Model 14(1):121–148
Farouki RT (2012) The Bernstein polynomial basis: a centennial retrospective. Comput Aided Geom Des 29(6):379–419
Frehse G (2005) Phaver: algorithmic verification of hybrid systems past hytech. In: Hybrid systems: computation and control, HSCC. Springer, pp 258–273
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
Galor O (2007) Discrete dynamical systems. Springer Science & Business Media, Berlin
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
Garloff J, Smith AP (2001) Investigation of a subdivision based algorithm for solving systems of polynomial equations. Nonlinear Anal Theory Methods Appl 47(1):167–178
Girard A (2005) Reachability of uncertain linear systems using zonotopes. In: Hybrid systems: computation and control, HSCC. Springer, pp 291–305
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
Gropp W, Lusk E, Doss N, Skjellum A (1996) A high-performance, portable implementation of the mpi message passing interface standard. Parallel Comput 22(6):789–828
Henzinger TA, Ho PH, Wong-Toi H (1997) Hytech: a model checker for hybrid systems. In: Computer aided verification, CAV. Springer, pp 460–463
Hildebrand FB (1987) Introduction to numerical analysis. Courier Corporation, North Chelmsford
Jódar L, Villanueva RJ, Arenas AJ, González GC (2008) Nonstandard numerical methods for a mathematical model for influenza disease. Math Comput Simul 79(3):622–633
Karp RM (1972) Reducibility among combinatorial problems. Springer, Berlin
Kermack WO, McKendrick AG (1927) A contribution to the mathematical theory of epidemics. R Soc Lond A Math Phys Eng Sci 115:700–721
Klipp E, Herwig R, Kowald A, Wierling C, Lehrach H (2008) Systems biology in practice: concepts, implementation and application. Wiley, New York
Kong S, Gao S, Chen W, Clarke E (2015) dreach: \(\delta \)-reachability analysis for hybrid systems. In: Tools and algorithms for the construction and analysis of systems, TACAS. Springer, pp 200–205
Kostousova E (1998) State estimation for dynamic systems via parallelotopes optimization and parallel computations. Optim Methods Softw 9(4):269–306
Kostousovat EK (2001) Control synthesis via parallelotopes: optimzation and parallel compuations. Optim Methods Softw 4(14):267–310
Kot M (1992) Discrete-time travelling waves: ecological examples. J Math Biol 30(4):413–436
Kot M, Schaffer WM (1986) Discrete-time growth-dispersal models. Math Biosci 80(1):109–136
Krommer AR (1994) Numerical integration: on advanced computer systems, vol 848. Springer Science & Business Media, Berlin
Kurzhanski AB, Varaiya P (2000) Ellipsoidal techniques for reachability analysis: internal approximation. Syst Control Lett 41(3):201–211
Kurzhanskiy AA, Varaiya P, et al (2006) Ellipsoidal toolbox. EECS Department, University of California, Berkeley, Technical report UCB/EECS-2006-46
Kvasnica M, Grieder P, Baotić M, Morari M (2004) Multi-parametric toolbox (mpt). In: Hybrid systems: computation and control. HSCC, Springer, pp 448–462
Lafferriere G, Pappas GJ, Yovine S (2001) Symbolic reachability computation for families of linear vector fields. J Symb Comput 32(3):231–253
Le Guernic C (2009) Reachability analysis of hybrid systems with linear continuous dynamics. PhD thesis, Université Joseph-Fourier-Grenoble I
Le Guernic C, Girard A (2010) Reachability analysis of linear systems using support functions. Nonlinear Anal Hybrid Syst 4(2):250–262
Lotka AJ (1925) Elements of physical biology. Williams & Wilkins Company
Mourrain B, Pavone JP (2009) Subdivision methods for solving polynomial equations. J Symb Comput 44(3):292–306. doi:10.1016/j.jsc.2008.04.016
Nataraj P, Arounassalame M (2007) A new subdivision algorithm for the Bernstein polynomial approach to global optimization. Int J Autom Comput 4(4):342–352
Nvidia CUDA (2008) Programming guide, Nvida
Platzer A (2007) Differential dynamic logic for verifying parametric hybrid systems. In: Automated reasoning with analytic tableaux and related methods, TABLEAUX, pp 216–232
Platzer A (2008) Differential dynamic logic for hybrid systems. J Autom Reason 41(2):143–189. doi:10.1007/s10817-008-9103-8
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
Van der Pol B (1926) Lxxxviii. On “relaxation-oscillations”. Lond Edinb Dublin Philos Mag J Sci 2(11):978–992
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
Rössler OE (1976) An equation for continuous chaos. Phys Lett A 57(5):397–398
Rössler OE (1979) An equation for hyperchaos. Phys Lett A 71(2):155–157
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
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
Sassi MAB, Sankaranarayanan S (2015) Bernstein polynomial relaxations for polynomial optimization problems. arXiv preprint arXiv:1509.01156
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
Shisha O (1966) The Bernstein form of a polynomial. J Res Natl Bur Stand Math Math Phys B 70:79
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
Varaiya P (2000) Reach set computation using optimal control. In: Inan M, Kurshan R (eds) Verification of digital and hybrid systems, NATO ASI series, vol 170. Springer, Berlin, pp 323–331
Volterra V (1927) Variazioni e fluttuazioni del numero d’individui in specie animali conviventi. C Ferrari
Wildenberg J, Vano J, Sprott J (2006) Complex spatiotemporal dynamics in lotka-volterra ring systems. Ecol Complex 3(2):140–147
Author information
Authors and Affiliations
Corresponding author
Additional information
This work is partially supported by Toyota under the CHESS center, DARPA BRASS project, ANR MALTHY project (ANR-12-INSE-003), and INdAM GNCS.
Appendix: Experiment details
Appendix: Experiment details
1.1 Van der Pol
1.2 Rössler attractor
1.3 SIR epidemi model
1.4 Generalized Lotka–Volterra model
1.5 Phosphorelay systems
1.6 Quadcopter drone
for \(i,j=0,1,\dots ,16\) and
for \(i=0,1,\dots ,16\) and \(j=0,1\).
Rights and permissions
About this article
Cite this article
Dreossi, T., Dang, T. & Piazza, C. Reachability computation for polynomial dynamical systems. Form Methods Syst Des 50, 1–38 (2017). https://doi.org/10.1007/s10703-016-0266-3
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-016-0266-3