Inner and outer approximate quantifier elimination for general reachability problems
Article No.: 8, Pages 1 - 11
Abstract
We propose an approach to compute inner and outer-approximations of the sets of values satisfying constraints expressed as arbitrarily quantified formulas. Such formulas arise for instance when specifying important problems in control such as robustness, motion planning or controllers comparison. We propose an interval-based method which allows for tractable but tight approximations. We demonstrate its applicability through a series of examples and benchmarks using a prototype implementation.
References
[1]
Chaouki Abdallah, Peter Dorato, and Wei Yang. 1970. Applications Of Quantifier Elimination Theory To Control System Design. Proceedings of the 4th IEEE Mediterranean Symposium on Control and Automation (02 1970).
[2]
M. Althoff. 2013. Reachability Analysis of Nonlinear Systems Using Conservative Polynomialization and Non-convex Sets. In HSCC. ACM publishers, 173–182.
[3]
M. Althoff, C. Le Guernic, and B. H. Krogh. 2011. Reachable set computation for uncertain time-varying linear systems. In International Conference on Hybrid Systems: Computation and Control. 93––102.
[4]
M. Althoff, O. Stursberg, and M. Buss. 2008. Reachability analysis of nonlinear systems with uncertain parameters using conservative linearization. In Proceedings of CDC. 4042–4048.
[5]
S. Bansal, M. Chen, S. L. Herbert, and C. J. Tomlin. 2017. Hamilton-Jacobi reachability: A brief overview and recent advances. In CDC.
[6]
Christopher W. Brown. 2003. QEPCAD B: A Program for Computing with Semi-Algebraic Sets Using CADs. SIGSAM Bull. 37, 4 (dec 2003), 97–108. https://doi.org/10.1145/968708.968710
[7]
X. Chen, E. Ábrahám, and S. Sankaranarayanan. 2012. Taylor Model Flowpipe Construction for Non-linear Hybrid Systems. In RTSS.
[8]
Xin Chen, Sriram Sankaranarayanan, and Erika Ábrahám. 2014. Under-approximate Flowpipes for Non-linear Continuous Systems. In Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design (Lausanne, Switzerland) (FMCAD ’14). FMCAD Inc, Austin, Texas, 59–66.
[9]
X. Chen, S. Sankaranarayanan, and E. Abraham. 2014. Under-approximate Flowpipes for Non-linear Continuous Systems. In FMCAD.
[10]
George E. Collins. 1975. Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In Automata Theory and Formal Languages, H. Brakhage (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 134–183.
[11]
Andreas Dolzmann and Thomas Sturm. 1997. REDLOG: Computer Algebra Meets Computer Logic. SIGSAM Bull. 31, 2 (jun 1997), 2–9. https://doi.org/10.1145/261320.261324
[12]
Alexandre Donzé. 2013. On Signal Temporal Logic. In RV(LNCS, Vol. 8174). Springer.
[13]
Georgios E. Fainekos and George J. Pappas. 2009. Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410, 42 (2009).
[14]
Sicun Gao, Soonho Kong, and Edmund Clarke. 2013. dReal: An SMT Solver for Nonlinear Theories of the Reals (Tool Paper). In CADE (Conference on Automated Deduction).
[15]
Isabel Garcia-Contreras, V. K. Hari Govind, Sharon Shoham, and Arie Gurfinkel. 2023. Fast Approximations of Quantifier Elimination. In Computer Aided Verification, Constantin Enea and Akash Lal (Eds.). Springer Nature Switzerland, Cham, 64–86.
[16]
Yeting Ge and Leonardo de Moura. 2009. Complete instantiation for quantified formulas in satisfiability modulo theories. In Computer Aided Verification. 306–320.
[17]
A. Girard, C. Le Guernic, and O. Maler. 2006. Efficient Computation of Reachable Sets of Linear Time-Invariant Systems with Inputs. In HSCC.
[18]
Joseph D. Gleason, Abraham P. Vinod, and Meeko M. K. Oishi. 2017. Underapproximation of reach-avoid sets for discrete-time stochastic systems via Lagrangian methods. In 2017 IEEE 56th Annual Conference on Decision and Control (CDC) (Melbourne, Australia). IEEE Press, 4283–4290. https://doi.org/10.1109/CDC.2017.8264291
[19]
Alexandre Goldsztejn. 2012. Modal Intervals Revisited, Part 1: A Generalized Interval Natural Extension. Reliable Computing 16 (2012), 130–183.
[20]
Alexandre Goldsztejn. 2012. Modal Intervals Revisited, Part 2: A Generalized Interval Mean Value Extension. Reliable Computing 16 (2012), 184–209.
[21]
A. Goldsztejn, D. Daney, M. Rueher, and P. Taillibert. 2005. Modal intervals revisited: a mean-value extension to generalized intervals. In QCP’05.
[22]
A. Goldsztejn and L. Jaulin. 2010. Inner Approximation of the Range of Vector-Valued Functions. Reliable Computing 14 (2010).
[23]
Eric Goubault and Sylvie Putot. 2019. Inner and outer reachability for the verification of control systems. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada, April 16-18, 2019, Necmiye Ozay and Pavithra Prabhakar (Eds.). ACM, 11–22.
[24]
Eric Goubault and Sylvie Putot. 2020. Robust Under-Approximations and Application to Reachability of Non-Linear Control Systems With Disturbances. IEEE Control. Syst. Lett. 4, 4 (2020), 928–933. https://doi.org/10.1109/LCSYS.2020.2997261
[25]
Eric Goubault and Sylvie Putot. 2021. Tractable higher-order under-approximating AE extensions for non-linear systems. In 7th IFAC Conference on Analysis and Design of Hybrid Systems, ADHS 2021, Brussels, Belgium, July 7-9, 2021. 235–240. https://doi.org/10.1016/j.ifacol.2021.08.504
[26]
Eric Goubault and Sylvie Putot. 2023. Guaranteed approximations of arbitrarily quantified reachability problems. arXiv:2309.07662 (2023).
[27]
C. Le Guernic and A. Girard. 2009. Reachability Analysis of Hybrid Systems Using Support Functions. In CAV.
[28]
Wolfram Research, Inc.[n. d.]. Mathematica, Version 13.1. https://www.wolfram.com/mathematica Champaign, IL, 2022.
[29]
Mats Jirstrand. 1997. Nonlinear Control System Design by Quantifier Elimination. J. Symb. Comput. 24 (1997), 137–152.
[30]
Niklas Kochdumper and Matthias Althoff. 2020. Computing Non-Convex Inner-Approximations of Reachable Sets for Nonlinear Continuous Systems. In 2020 59th IEEE Conference on Decision and Control (CDC). 2130–2137. https://doi.org/10.1109/CDC42340.2020.9304022
[31]
A. B. Kurzhanski and P. Varaiya. 2000. Ellipsoidal Techniques for Reachability Analysis. In HSCC.
[32]
Steven M. Lavalle. 2006. Planning Algorithms. Cambridge University Press.
[33]
M. Li, P.N. Mosaad, M. Fränzle, Z. She, and B. Xue. 2018. Safe over- and under- approximation of reachable sets for autonomous dynamical systems. In FORMATS. 252––270.
[34]
K. Makino and M. Berz. 2003. Taylor models and other validated functional inclusion methods. Int. J. Pure Appl. Math (2003).
[35]
Kostas Margellos and John Lygeros. 2011. Hamilton-Jacobi Formulation for Reach-Avoid Differential Games.IEEE Trans. Automat. Contr. 56, 8 (2011), 1849–1861.
[36]
Thomas Le Mézo, Luc Jaulin, and Benoît Zerr. 2018. Bracketing the solutions of an ordinary differential equation with uncertain initial conditions. Appl. Math. Comput. 318 (2018).
[37]
I. Mitchell, A. Bayen, and C. Tomlin. 2005. A time-dependent Hamilton–Jacobi formulation of reachable sets for continuous dynamic games. IEEE Trans. Automat. Control 50, 7 (2005), 947––957.
[38]
Ian M. Mitchell. 2007. Comparing Forward and Backward Reachability as Tools for Safety Analysis. In Hybrid Systems: Computation and Control, Alberto Bemporad, Antonio Bicchi, and Giorgio Buttazzo (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 428–443.
[39]
M. Neher, K. R. Jackson, and N. S. Nedialkov. 2007. On Taylor model based integration of ODEs. SIAM J. Numer. Anal 45 (2007).
[40]
Luan Viet Nguyen, James Kapinski, Xiaoqing Jin, Jyotirmoy V. Deshmukh, and Taylor T. Johnson. 2017. Hyperproperties of Real-Valued Signals. In MEMOCODE ’17.
[41]
M. A. Ben Sassi, R. Testylier, T. Dang, and A. Girard. 2012. Reachability Analysis of Polynomial Systems Using Linear Programming Relaxations(LNCS, Vol. 7561).
[42]
Jacob T Schwartz and Micha Sharir. 1983. On the “piano movers” problem. II. General techniques for computing topological properties of real algebraic manifolds. Advances in Applied Mathematics 4, 3 (1983), 298–351. https://doi.org/10.1016/0196-8858(83)90014-3
[43]
K. Siaulys and J. M. Maciejowski. 2016. Verification of model predictive control laws using weispfenning’s quantifier elimination by virtual substitution algorithm. In 2016 IEEE 55th Conference on Decision and Control (CDC). 1452–1457. https://doi.org/10.1109/CDC.2016.7798471
[44]
Thomas Sturm and Ashish Tiwari. 2011. Verification and synthesis using real quantifier elimination. In Proc. ISSAC 2011. ACM Press, San Jose, United States, 329. https://doi.org/10.1145/1993886.1993935
[45]
A. Tarski. 1948. A decision method for elementary algebra and geometry. Technical Report. Rand Corporation.
[46]
Volker Weispfenning. 1993. Quantifier Elimination for Real Algebra - the Quadratic Case and Beyond. AAECC 8 (1993), 85–101.
[47]
Mark Wetzlinger and Matthias Althoff. 2023. Backward Reachability Analysis of Perturbed Continuous-Time Linear Systems Using Set Propagation. CoRR abs/2310.19083 (2023). https://doi.org/10.48550/ARXIV.2310.19083 arXiv:2310.19083
[48]
B. Xue, Z. She, and A. Easwaran. 2016. Under-Approximating Backward Reachable Sets by Polytopes. In CAV.
Index Terms
- Inner and outer approximate quantifier elimination for general reachability problems
Recommendations
Outer-loop vectorization: revisited for short SIMD architectures
PACT '08: Proceedings of the 17th international conference on Parallel architectures and compilation techniquesVectorization has been an important method of using data-level parallelism to accelerate scientific workloads on vector machines such as Cray for the past three decades. In the last decade it has also proven useful for accelerating multi-media and ...
Inner and outer approximations of existentially quantified equality constraints
CP'06: Proceedings of the 12th international conference on Principles and Practice of Constraint ProgrammingWe propose a branch and prune algorithm that is able to compute inner and outer approximations of the solution set of an existentially quantified constraint where existential parameters are shared between several equations. While other techniques that ...
An Inner-Outer Approximation Approach to Chance Constrained Optimization
Nonlinear chance constrained optimization (CCOPT) problems are known to be difficult to solve. This work proposes a smooth approximation approach consisting of an inner and an outer analytic approximation of chance constraints. In this way, CCOPT is ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2024 ACM.
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 the author(s) 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: 14 May 2024
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed limited
Funding Sources
- ANR
- AID-CIEDS
Conference
HSCC '24
Sponsor:
Acceptance Rates
Overall Acceptance Rate 153 of 373 submissions, 41%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 110Total Downloads
- Downloads (Last 12 months)110
- Downloads (Last 6 weeks)6
Reflects downloads up to 05 Mar 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign inFull Access
View options
View or Download as a PDF file.
PDFeReader
View online with eReader.
eReaderHTML Format
View this article in HTML Format.
HTML Format