skip to main content
10.1145/3178126.3178133acmconferencesArticle/Chapter ViewAbstractPublication PagescpsweekConference Proceedingsconference-collections
research-article

Under-Approximating Reach Sets for Polynomial Continuous Systems

Published: 11 April 2018 Publication History

Abstract

In this paper we suggest a method based on convex programming for computing semi-algebraic under-approximations of reach sets for polynomial continuous systems with initial sets being the zero sub-level set of a polynomial function. It is well-known that the reachable set can be formulated as the zero sub-level set of a value function to a Hamilton-Jacobi partial differential equation (HJE), and our approach in this paper consequently focuses on searching for approximate analytical polynomial solutions to associated HJEs, of which the zero sub-level sets converge to the exact reachable set from inside in measure, without discretizing the state space. Such approximate solutions can be computed via a classical hierarchy of convex programs consisting of linear matrix inequalities, which are constructed by sum-of-squares decomposition techniques. In contrast to traditional numerical methods approximately solving HJEs, such as level-set methods, our method reduces HJE solving to convex optimization, avoiding the complexity associated to gridding the state space. Compared to existing approaches computing under-approximations, the approach described in this paper is structurally simpler as the under-approximations are the outcome of a single semi-definite program. Furthermore, an over-approximation of the reach set, shedding light on the quality of the constructed under-approximation, can be constructed via solving the same semi-definite program. Several illustrative examples and comparisons with existing methods demonstrate the merits of our approach.

References

[1]
M. Althoff, O. Stursberg, and M. Buss. Reachability analysis of nonlinear systems with uncertain parameters using conservative linearization. In CDC'08, pages 4042--4048. IEEE, 2008.
[2]
E. Asarin, O. Bournez, T. Dang, and O. Maler. Approximate reachability analysis of piecewise-linear dynamical systems. In HSCC'00, pages 20--31. Springer, 2000.
[3]
X. Chen, E. Ábrahám, and S. Sankaranarayanan. Taylor model flowpipe construction for non-linear hybrid systems. In RTSS'12, pages 183--192. IEEE, 2012.
[4]
X. Chen, S. Sankaranarayanan, and E. Ábrahám. Under-approximate flowpipes for non-linear continuous systems. In FMCAD'14, pages 59--66. FMCAD Inc, 2014.
[5]
T. Dang, O. Maler, and R. Testylier. Accurate hybridization of nonlinear systems. In HSCC'10, pages 11--20. ACM, 2010.
[6]
A. N. Daryin and A. B. Kurzhanski. Estimation of reachability sets for large-scale uncertain systems: from theory to computation. In CDC'12, pages 7401--7406. IEEE, 2012.
[7]
A. Eggers, N. Ramdani, N. S. Nedialkov, and M. Fränzle. Improving the SAT modulo ODE approach to hybrid systems analysis by combining different enclosure methods. Software & Systems Modeling, 14(1):121--148, 2015.
[8]
G. Frehse, S. Bogomolov, M. Greitschus, T. Strump, and A. Podelski. Eliminating spurious transitions in reachability with support functions. In HSCC'15, pages 149--158. ACM, 2015.
[9]
D. H. Fremlin. Kirszbraun's theorem. Preprint, 2011.
[10]
T. Gan, M. Chen, Y. Li, B. Xia, and N. Zhan. Reachability Analysis for Solvable Dynamical Systems. To appear in IEEE Trans. Autom. Control., 2017.
[11]
A. Girard, C. Le Guernic, and O. Maler. Efficient computation of reachable sets of linear time-invariant systems with inputs. In HSCC'06, pages 257--271. Springer, 2006.
[12]
E. Goubault, O. Mullier, S. Putot, and M. Kieffer. Inner approximated reachability analysis. In HSCC'14, pages 163--172. ACM, 2014.
[13]
E. Goubault and S. Putot. Forward Inner-Approximated Reachability of Non-Linear Continuous Systems. In HSCC'17, pages 1--10. ACM, 2017.
[14]
D. Handelman. Representing polynomials by positive linear functions on compact convex polyhedra. Pacific Journal of Mathematics, 132(1):35--62, 1988.
[15]
D. Henrion and M. Korda. Convex computation of the region of attraction of polynomial control systems. IEEE Trans. Autom. Control., 59(2):297--312, 2014.
[16]
M. Kojima. Exploiting Structured Sparsity in Large Scale Semi-definite Programming Problems. In ICMS'10, pages 4--9. Springer, 2010.
[17]
M. Korda, D. Henrion, and C. N. Jones. Inner approximations of the region of attraction for polynomial dynamical systems. IFAC Proceedings Volumes, 46(23):534--539, 2013.
[18]
A. B. Kurzhanski and P. Varaiya. Ellipsoidal techniques for reachability analysis: internal approximation. Systems & Control Letters, 41(3):201--211, 2000.
[19]
A. B. Kurzhanski and P. Varaiya. Ellipsoidal Techniques for Reachability Analysis. In HSCC'00, pages 202--214. Springer, 2000.
[20]
J. B. Lasserre. Semidefinite programming vs. LP relaxations for polynomial programming. Mathematics of Operations Research, 27(2):347--360, 2002.
[21]
J. B. Lasserre. Tractable approximations of sets defined with quantifiers. Mathematical Programming, 151(2):507--527, 2015.
[22]
J. Lofberg. Yalmip: A toolbox for modeling and optimization in MATLAB. In CACSD'04, pages 284--289. IEEE, 2004.
[23]
J. Lygeros. On reachability and minimum cost optimal control. Automatica, 40(6):917--927, 2004.
[24]
V. Magron, D. Henrion, and J.-B. Lasserre. Semidefinite approximations of projections and polynomial images of semialgebraic sets. SIAM Journal on Optimization, 25(4):2143--2164, 2015.
[25]
O. Maler. Algorithmic verification of continuous and hybrid systems. arXiv preprint arXiv:1403.0952, 2014.
[26]
I. M. Mitchell, A. M. Bayen, and C. J. Tomlin. A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games. IEEE Trans. Autom. Control., 50(7):947--957, 2005.
[27]
A. Mosek. The MOSEK optimization toolbox for MATLAB manual. Version 7.1 (Revision 28), page 17, 2015.
[28]
S. Prajna. Barrier certificates for nonlinear model validation. Automatica, 42(1):117--126, 2006.
[29]
M. Putinar. Positive polynomials on compact semi-algebraic sets. Indiana University Mathematics Journal, 42(3):969--984, 1993.
[30]
N. Ramdani, N. Meslem, and Y. Candau. A hybrid bounding method for computing an over-approximation for the reachable set of uncertain nonlinear systems. IEEE Trans. Autom. Control., 54(10):2352--2364, 2009.
[31]
S. Ratschan and Z. She. Safety verification of hybrid systems by constraint propagation based abstraction refinement. In HSCC'05, volume 5, pages 573--589. Springer, 2005.
[32]
P. Roux, Y.-L. Voronin, and S. Sankaranarayanan. Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants. In SAS'16, pages 424--446. Springer, 2016.
[33]
S. Sankaranarayanan, X. Chen, et al. Lyapunov Function Synthesis using Handelman Representations. IFAC Proceedings Volumes, 46(23):576--581, 2013.
[34]
S. Schupp, E. Ábrahám, X. Chen, I. B. Makhlouf, G. Frehse, S. Sankaranarayanan, and S. Kowalewski. Current challenges in the verification of hybrid systems. In CyPhy'15, pages 8--24. Springer, 2015.
[35]
L. Vandenberghe and S. Boyd. Semidefinite programming. SIAM Review, 38(1):49--95, 1996.
[36]
T.-C. Wang, S. Lall, and M. West. Polynomial level-set method for polynomial system reachable set estimation. IEEE Trans. Autom. Control., 58(10):2508--2521, 2013.
[37]
B. Xue, A. Easwaran, N.-J. Cho, and M. Fränzle. Reach-avoid verification for nonlinear systems based on boundary analysis. IEEE Trans. Autom. Control., 62(7):3518--3523, 2017.
[38]
B. Xue, P. N. Mosaad, M. Fränzle, M. Chen, Y. Li, and N. Zhan. Safe Over-and Under-Approximation of Reachable Sets for Delay Differential Equations. In FORMATS'17, pages 281--299. Springer, 2017.
[39]
B. Xue, Z. She, and A. Easwaran. Under-approximating backward reachable sets by polytopes. In CAV'16, pages 457--476. Springer, 2016.
[40]
B. Xue, Z. She, and A. Easwaran. Under-Approximating Backward Reachable Sets by Semialgebraic Sets. IEEE Trans. Autom. Control., 62:5185--5197, 2017.

Cited By

View all
  • (2024)PolyARBerNN: A Neural Network Guided Solver and Optimizer for Bounded Polynomial InequalitiesACM Transactions on Embedded Computing Systems10.1145/363297023:2(1-26)Online publication date: 24-Jan-2024
  • (2024)Practical Approximate Quantifier Elimination for Non-linear Real ArithmeticFormal Methods10.1007/978-3-031-71162-6_6(111-130)Online publication date: 11-Sep-2024
  • (2022)Formal Safety Net Control Using Backward Reachability AnalysisIEEE Transactions on Automatic Control10.1109/TAC.2021.312418867:11(5698-5713)Online publication date: Nov-2022
  • Show More Cited By
  1. Under-Approximating Reach Sets for Polynomial Continuous Systems

    Recommendations

    Comments

    Information & Contributors

    Information

    Published In

    cover image ACM Conferences
    HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)
    April 2018
    296 pages
    ISBN:9781450356428
    DOI:10.1145/3178126
    Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

    Sponsors

    Publisher

    Association for Computing Machinery

    New York, NY, United States

    Publication History

    Published: 11 April 2018

    Permissions

    Request permissions for this article.

    Check for updates

    Qualifiers

    • Research-article
    • Research
    • Refereed limited

    Conference

    HSCC '18
    Sponsor:

    Acceptance Rates

    Overall Acceptance Rate 153 of 373 submissions, 41%

    Contributors

    Other Metrics

    Bibliometrics & Citations

    Bibliometrics

    Article Metrics

    • Downloads (Last 12 months)17
    • Downloads (Last 6 weeks)0
    Reflects downloads up to 27 Jan 2025

    Other Metrics

    Citations

    Cited By

    View all
    • (2024)PolyARBerNN: A Neural Network Guided Solver and Optimizer for Bounded Polynomial InequalitiesACM Transactions on Embedded Computing Systems10.1145/363297023:2(1-26)Online publication date: 24-Jan-2024
    • (2024)Practical Approximate Quantifier Elimination for Non-linear Real ArithmeticFormal Methods10.1007/978-3-031-71162-6_6(111-130)Online publication date: 11-Sep-2024
    • (2022)Formal Safety Net Control Using Backward Reachability AnalysisIEEE Transactions on Automatic Control10.1109/TAC.2021.312418867:11(5698-5713)Online publication date: Nov-2022
    • (2022)Linearization, Model Reduction and Reachability in Nonlinear odesReachability Problems10.1007/978-3-031-19135-0_4(49-66)Online publication date: 12-Oct-2022
    • (2021)Reachable Tube Computation of Uncertain LTI Systems using Support Functions2021 European Control Conference (ECC)10.23919/ECC54610.2021.9654890(2670-2675)Online publication date: 29-Jun-2021
    • (2021)Over- and Under-Approximations of Reachable Sets With Series Representations of Evolution FunctionsIEEE Transactions on Automatic Control10.1109/TAC.2020.299401966:3(1414-1421)Online publication date: Mar-2021
    • (2021)$$\mathbf{OURS} $$: Over- and Under-Approximating Reachable Sets for Analytic Time-Invariant Differential EquationsDependable Software Engineering. Theories, Tools, and Applications10.1007/978-3-030-91265-9_14(261-278)Online publication date: 18-Nov-2021
    • (2020)Computing Non-Convex Inner-Approximations of Reachable Sets for Nonlinear Continuous Systems2020 59th IEEE Conference on Decision and Control (CDC)10.1109/CDC42340.2020.9304022(2130-2137)Online publication date: 14-Dec-2020
    • (2019)Robust invariant sets generation for state-constrained perturbed polynomial systemsProceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control10.1145/3302504.3311810(128-137)Online publication date: 16-Apr-2019
    • (2019)Inner and outer reachability for the verification of control systemsProceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control10.1145/3302504.3311794(11-22)Online publication date: 16-Apr-2019
    • Show More Cited By

    View Options

    Login options

    View options

    PDF

    View or Download as a PDF file.

    PDF

    eReader

    View online with eReader.

    eReader

    Figures

    Tables

    Media

    Share

    Share

    Share this Publication link

    Share on social media