More Web Proxy on the site http://driver.im/

research-article

Inner and outer reachability for the verification of control systems

Authors:

Sylvie PutotAuthors Info & Claims

HSCC '19: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control

Pages 11 - 22

https://doi.org/10.1145/3302504.3311794

Published: 16 April 2019 Publication History

Abstract

We investigate the information and guarantees provided by different inner and outer approximated reachability analyses, for proving properties of dynamical systems. We explore the connection of these approximated sets with the maximal and minimal reachable sets of Mitchell [31], with an additional notion of robustness to disturbance. We demonstrate the practical use of a specific computation of these approximated reachable sets. We revisit in particular the reachavoid properties.

References

[1]

M. Althoff. 2013. Reachability Analysis of Nonlinear Systems Using Conservative Polynomialization and Non-convex Sets. In HSCC. ACM publishers, 173--182.

Digital Library

[2]

J.-P. Aubin. 2001. Viability Kernels and Capture Basins of Sets Under Differential Inclusions. SIAM Journal on Control and Optimization (2001).

Digital Library

[3]

S. Bansal, M. Chen, S. L. Herbert, and C. J. Tomlin. 2017. Hamilton-Jacobi reachability: A brief overview and recent advances. In CDC.

[4]

P. Cardaliaguet, M. Quincampoix, and P. Saint-Pierre. 1999. Set-Valued Numerical Analysis for Optimal Control and Differential Games. Birkhäuser.

[5]

X. Chen, E. Ábrahám, and S. Sankaranarayanan. 2012. Taylor Model Flowpipe Construction for Non-linear Hybrid Systems. In RTSS.

Digital Library

[6]

X. Chen, S. Sankaranarayanan, and E. Abraham. 2014. Under-approximate Flow-pipes for Non-linear Continuous Systems. In FMCAD.

Digital Library

[7]

J. Comba and J. Stolfi. 1993. Affine arithmetic and its applications to computer graphics. In SIBGRAPI (1993).

[8]

A. E. C. Da Cunha. 2015. Benchmark: Quadrotor Attitude Control. In ARCH'14--15, Vol. 34. EasyChair, 57--72.

[9]

T. Dang, O. Maler, and R. Testylier. 2010. Accurate hybridization of nonlinear systems. In HSCC.

Digital Library

[10]

I. Filippidis, S. Dathathri, S. C. Livingston, N. Ozay, and R. M. Murray. 2016. Control design for hybrid systems with TuLiP: The Temporal Logic Planning toolbox. In CCA. IEEE, 1030--1041.

[11]

J. F. Fisac, M. Chen, C. J. Tomlin, and S. S. Sastry. 2015. Reach-avoid problems with time-varying dynamics, targets and constraints. In HSCC.

Digital Library

[12]

J. Förster. 2015. System Identification of the Crazyflie 2.0 Nano Quadrocopter. Bachelor Thesis.

[13]

A. Girard. 2005. Reachability of uncertain linear systems using zonotopes. In HSCC'05. Springer.

Digital Library

[14]

A. Girard, C. Le Guernic, and O. Maler. 2006. Efficient Computation of Reachable Sets of Linear Time-Invariant Systems with Inputs. In HSCC.

Digital Library

[15]

A. Goldsztejn. 2006. A Branch and Prune Algorithm for the Approximation of Non-linear AE-solution Sets. In ACM SAC.

Digital Library

[16]

Alexandre Goldsztejn. 2012. Modal Intervals Revisited, Part 1: A Generalized Interval Natural Extension. Reliable Computing 16 (2012), 130--183.

[17]

Alexandre Goldsztejn. 2012. Modal Intervals Revisited, Part 2: A Generalized Interval Mean Value Extension. Reliable Computing 16 (2012), 184--209.

[18]

A. Goldsztejn, D. Daney, M. Rueher, and P. Taillibert. 2005. Modal intervals revisited: a mean-value extension to generalized intervals. In QCP'05.

[19]

E. Goubault and S. Putot. 2017. Forward Inner-Approximated Reachability of Non-Linear Continuous Systems. In HSCC. ACM.

Digital Library

[20]

E. Goubault, S. Putot, and L. Sahlman. 2018. Inner and Outer Approximating Flowpipes for Delay Differential Equations. In CAV.

[21]

R. Scitovski J. Cumin, B. Grizelj. 2009. Numerical Solving of Ballistic Flight Equations for Big Bore Air Rifle. Technical Gazette 16 (2009).

[22]

E.W. Kaucher. 1980. Interval analysis in the extended interval space IR. Comput. (Supplementum) 2 (1980).

[23]

S. Kaynama, J. Maidens, M. Oishi, I. M. Mitchell, and G. A. Dumont. 2012. Computing the Viability Kernel Using Maximal Reachable Sets. In HSCC. ACM.

Digital Library

[24]

S. Kaynama, M. Oishi, I. M. Mitchell, and G. A. Dumont. 2011. The continual reachability set and its computation using maximal reachability techniques. In IEEE CDC.

[25]

M. Korda, D. Henrion, and C. N. Jones. 2013. Inner Approximations of the Region of Attraction for Polynomial Dynamical Systems. In NOLCOS.

[26]

A. B Kurzhanski and P. Varaiya. 2000. Ellipsoidal techniques for reachability analysis: internal approximation. Systems & control letters (2000).

[27]

D. Liberzon. 2003. Switching in Systems and Control. Birkhauser.

[28]

C. Luis and J. Le Ny. 2016. Design of a Trajectory Tracking Controller for a Nanoquadcopter. https://arxiv.org/abs/1608.05786v1.

[29]

K. Margellos and J. Lygeros. 2011. Hamilton-Jacobi Formulation for Reach-Avoid Differential Games. IEEE Trans. Automat. Contr. 56, 8 (2011), 1849--1861.

[30]

T. Le Mézo, L. Jaulin, and B. Zerr. 2017. Bracketing the solutions of an ordinary differential equation with uncertain initial conditions. Appl. Math. Comput. (2017).

Digital Library

[31]

I. M. Mitchell. 2007. Comparing Forward and Backward Reachability as Tools for Safety Analysis. In HSCC.

Digital Library

[32]

Ramon E. Moore. 1966. Interval analysis.

[33]

N. S. Nedialkov, K. Jackson, and G. Corliss. 1999. Validated Solutions of Initial Value Problems for Ordinary Differential Equations. Appl. Math. Comp. (1999).

Digital Library

[34]

M. Amin Ben Sassi, R. Testylier, T. Dang, and A. Girard. 2012. Reachability Analysis of Polynomial Systems Using Linear Programming Relaxations. In ATVA.

[35]

C.J. Tomlin, J. Lygeros, and S. Shankar Sastry. 2000. A game theoretic approach to controller design for hybrid systems. Proc. IEEE 88, 7 (2000), 949--970.

[36]

T. Wongpiromsarn, U. Topcu, N. Ozay, H. Xu, and R. M. Murray. 2011. TuLiP: a software toolbox for receding horizon temporal logic planning. In HSCC. ACM.

Digital Library

[37]

B. Xue, M. Fränzle, and N. Zhan. 2018. Under-Approximating Reach Sets for Polynomial Continuous Systems. In Proceedings of HSCC '18. ACM. 51--60.

Digital Library

[38]

B. Xue, P. Nazier Mosaad, M. Fränzle, M. Chen, Y. Li, and N. Zhan. 2017. Safe Over-and Under-Approximation of Reachable Sets for Delay Differential Equations. In FORMATS (LNCS), Vol. 10419. Springer, 281--299.

[39]

Bai Xue, Zhikun She, and Arvind Easwaran. 2016. Under-Approximating Backward Reachable Sets by Polytopes. In CAV.

[40]

Z. Zhou, J. Ding, H. Huang, R. Takei, and C. Tomlin. 2018. Efficient path planning algorithms in reach-avoid problems. Automatica 89 (2018).

Cited By

Goubault EPutot S(2024)Inner and outer approximate quantifier elimination for general reachability problemsProceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3641513.3650125(1-11)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3641513.3650125
El-Kebir HPirosmanishvili AOrnik M(2024)Online Guaranteed Reachable Set Approximation for Systems With Changed Dynamics and Control AuthorityIEEE Transactions on Automatic Control10.1109/TAC.2023.327549569:2(726-740)Online publication date: Feb-2024
https://doi.org/10.1109/TAC.2023.3275495
Wetzlinger MKulmburg AAlthoff M(2024)Inner Approximations of Reachable Sets for Nonlinear Systems Using the Minkowski DifferenceIEEE Control Systems Letters10.1109/LCSYS.2024.34211948(2033-2038)Online publication date: 2024
https://doi.org/10.1109/LCSYS.2024.3421194
Show More Cited By

Recommendations

Falsification of hybrid systems using symbolic reachability and trajectory splicing
HSCC '19: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control

The falsification of a hybrid system aims at finding trajectories that violate a given safety property. This is a challenging problem, and the practical applicability of current falsification algorithms still suffers from their high time complexity. In ...
Two CEGAR-based approaches for the safety verification of PLC-controlled plants
Abstract
In this paper we address the safety analysis of chemical plants controlled by programmable logic controllers (PLCs). We consider a specification of the control program of the PLCs, extended with the specification of the dynamic plant behavior. The ...
Ivy: safety verification by interactive generalization
PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation

Despite several decades of research, the problem of formal verification of infinite-state systems has resisted effective automation. We describe a system --- Ivy --- for interactively verifying safety of infinite-state systems. Ivy's key principle is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

HSCC '19: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control

April 2019

299 pages

ISBN:9781450362825

DOI:10.1145/3302504

Program Chairs:
Necmiye Ozay
University of Michigan
,
Pavithra Prabhakar
Kansas State University

Copyright © 2019 ACM.

Publication rights licensed to ACM. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of a national government. As such, the Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.

Sponsors

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 April 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Direction Générale de lðArmement
Direction Générale de lðArmement, Thalès, Dassault Aviation, Naval Group

Conference

HSCC '19

Sponsor:

SIGBED

HSCC '19: 22nd ACM International Conference on Hybrid Systems: Computation and Control

April 16 - 18, 2019

Quebec, Montreal, Canada

Acceptance Rates

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

25
Total Citations
View Citations
285
Total Downloads

Downloads (Last 12 months)29
Downloads (Last 6 weeks)6

Reflects downloads up to 21 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Goubault EPutot S(2024)Inner and outer approximate quantifier elimination for general reachability problemsProceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3641513.3650125(1-11)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3641513.3650125
El-Kebir HPirosmanishvili AOrnik M(2024)Online Guaranteed Reachable Set Approximation for Systems With Changed Dynamics and Control AuthorityIEEE Transactions on Automatic Control10.1109/TAC.2023.327549569:2(726-740)Online publication date: Feb-2024
https://doi.org/10.1109/TAC.2023.3275495
Wetzlinger MKulmburg AAlthoff M(2024)Inner Approximations of Reachable Sets for Nonlinear Systems Using the Minkowski DifferenceIEEE Control Systems Letters10.1109/LCSYS.2024.34211948(2033-2038)Online publication date: 2024
https://doi.org/10.1109/LCSYS.2024.3421194
Bernini NBessa MDelmas RGold AGoubault EPennec RPutot SSillion F(2024)Reinforcement learning with formal performance metrics for quadcopter attitude control under non-nominal contextsEngineering Applications of Artificial Intelligence10.1016/j.engappai.2023.107090127(107090)Online publication date: Jan-2024
https://doi.org/10.1016/j.engappai.2023.107090
Ren DLiang ZWu CDing JWu TXue B(2024)Inner-Approximate Reachability Computation via Zonotopic Boundary AnalysisComputer Aided Verification10.1007/978-3-031-65633-0_14(307-328)Online publication date: 26-Jul-2024
https://doi.org/10.1007/978-3-031-65633-0_14
Raz DYang LUmberger BOzay N(2023)Determining the domain of stable human sit-to-stand motions via controlled invariant sets and backward reachability2023 European Control Conference (ECC)10.23919/ECC57647.2023.10178282(1-7)Online publication date: 13-Jun-2023
https://doi.org/10.23919/ECC57647.2023.10178282
Wetzlinger MKochdumper NBak SAlthoff M(2023)Fully Automated Verification of Linear Systems Using Inner and Outer Approximations of Reachable SetsIEEE Transactions on Automatic Control10.1109/TAC.2023.329200868:12(7771-7786)Online publication date: Dec-2023
https://doi.org/10.1109/TAC.2023.3292008
Djeumou FVinod AGoubault EPutot STopcu U(2023)On-the-Fly Control of Unknown Systems: From Side Information to Performance Guarantees Through ReachabilityIEEE Transactions on Automatic Control10.1109/TAC.2022.321726068:8(4857-4872)Online publication date: Aug-2023
https://doi.org/10.1109/TAC.2022.3217260
Bohn CReis PSchwartz MHohmann S(2023)Time and Memory-Efficient Computation of Hamilton-Jacobi Reachable Sets Based on a Level Set Method Employing Adaptive Grids2023 62nd IEEE Conference on Decision and Control (CDC)10.1109/CDC49753.2023.10383317(8235-8241)Online publication date: 13-Dec-2023
https://doi.org/10.1109/CDC49753.2023.10383317
Yang LZhang HJeannin JOzay N(2022)Efficient Backward Reachability Using the Minkowski Difference of Constrained ZonotopesIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2022.319797141:11(3969-3980)Online publication date: Nov-2022
https://doi.org/10.1109/TCAD.2022.3197971
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents