Inner and outer approximate quantifier elimination for general reachability problems

DOI10.1145/3641513.3650125MaRDI QIDQ6993505zbMATH OpenFDO

Authors Éric Goubault, Sylvie Putot

Publication date 25 April 2025

Full work available at URL https://doi.org/10.1145/3641513.3650125

zbMATH Keywords

inner and outer approximationsquantified problemsreachability

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Cites work

• A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games
• Bracketing the solutions of an ordinary differential equation with uncertain initial conditions
• Comparing Forward and Backward Reachability as Tools for Safety Analysis
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Fast approximations of quantifier elimination
• Hamilton–Jacobi Formulation for Reach–Avoid Differential Games
• scientific article; zbMATH DE number 3497890 (Why is no real title available?)
• scientific article; zbMATH DE number 2069519 (Why is no real title available?)
• scientific article; zbMATH DE number 1444352 (Why is no real title available?)
• scientific article; zbMATH DE number 3053259 (Why is no real title available?)
• Hybrid Systems: Computation and Control
• Inner and outer reachability for the verification of control systems
• Nonlinear control system design by quantifier elimination
• On Taylor Model Based Integration of ODEs
• On the Piano Movers problem. II: General techniques for computing topological properties of real algebraic manifolds
• Planning Algorithms
• QEPCAD B
• Quantifier elimination for real algebra -- the quadratic case and beyond
• Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets
• Reachability analysis of polynomial systems using linear programming relaxations
• Reachable set computation for uncertain time-varying linear systems
• Robustness of temporal logic specifications for continuous-time signals
• Safe over- and under-approximation of reachable sets for autonomous dynamical systems
• Under-approximating backward reachable sets by polytopes
• Verification and synthesis using real quantifier elimination

Cited in

(1)

• Inner and outer approximations of arbitrarily quantified reachability problems

This page was built for publication: Inner and outer approximate quantifier elimination for general reachability problems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6993505)