research-article

Simulation-Driven Reachability Using Matrix Measures

Authors:

James Kapinski,

Sayan MitraAuthors Info & Claims

ACM Transactions on Embedded Computing Systems (TECS), Volume 17, Issue 1

Article No.: 21, Pages 1 - 28

https://doi.org/10.1145/3126685

Published: 06 December 2017 Publication History

Abstract

Simulation-driven verification can provide formal safety guarantees for otherwise intractable nonlinear and hybrid system models. A key step in simulation-driven algorithms is to compute the reach set overapproximations from a set of initial states through numerical simulations and sensitivity analysis. This article addresses this problem by providing algorithms for computing discrepancy functions as the upper bound on the sensitivity, that is, the rate at which trajectories starting from neighboring states converge or diverge. The algorithms rely on computing local bounds on matrix measures as the exponential change rate of the discrepancy function. We present two techniques to compute the matrix measures under different norms: regular Euclidean norm or Euclidean norm under coordinate transformation, such that the exponential rate of the discrepancy function, and therefore, the conservativeness of the overapproximation, is locally minimized. The proposed algorithms enable automatic reach set computations of general nonlinear systems and have been successfully used on several challenging benchmark models. All proposed algorithms for computing discrepancy functions give soundness and relative completeness of the overall simulation-driven safety-bounded verification algorithm. We present a series of experiments to illustrate the accuracy and performance of the algorithms.

References

[1]

James Anderson and Antonis Papachristodoulou. 2010. Dynamical system decomposition for efficient, sparse analysis. In CDC (2010). IEEE, 6565--6570.

[2]

David Angeli. 2002. A Lyapunov approach to incremental stability properties. IEEE Trans. Automat. Control 47, 3 (2002), 410--421.

[3]

David Angeli, Eduardo D. Sontag, and Yuan Wang. 2000. A characterization of integral input-to-state stability. IEEE Trans. Automat. Control 45, 6 (2000), 1082--1097.

[4]

Nikos Aréchiga, James Kapinski, Jyotirmoy V. Deshmukh, André Platzer, and Bruce Krogh. 2015. Numerically-aided deductive safety proof for a powertrain control system. Elect. Notes Theoret. Comput. Sci. 317 (2015), 19--25.

Digital Library

[5]

Nels E. Beckman, Aditya V. Nori, Sriram K. Rajamani, Robert J. Simmons, Sai Deep Tetali, and Aditya V. Thakur. 2010. Proofs from tests. IEEE Transactions on Software Engineering 36, 4 (2010), 495--508.

Digital Library

[6]

V. A. Boichenko and G. A. Leonov. 1998. Lyapunov’s direct method in estimates of topological entropy. J. Math. Sci. 91, 6 (1998), 3370--3379.

[7]

Stephen Boyd, Laurent El Ghaoui, Eric Feron, and Venkataramanan Balakrishnan. 1994. Linear Matrix Inequalities in System and Control Theory. Studies in Applied Mathematics (1994), Vol. 15. SIAM, Philadelphia.

[8]

M. Bozzano, A. Cimatti, A. Fernandes Pires, D. Jones, G. Kimberly, T. Petri, R. Robinson, and S. Tonetta. 2015. Formal design and safety analysis of AIR6110 wheel brake system. In CAV (2015). Springer, 518--535.

[9]

CAPD. 2002. Computer assisted proofs in dynamics. Retrieved from http://www.capd.ii.uj.edu.pl/.

[10]

Xin Chen, Erika Ábrahám, and Sriram Sankaranarayanan. 2013. Flow*: An analyzer for non-linear hybrid systems. In CAV (2013). Springer, 258--263.

[11]

Yi Deng, Akshay Rajhans, and A. Agung Julius. 2013. Strong: A trajectory-based verification toolbox for hybrid systems. In QEST (2013). Springer, 165--168.

Digital Library

[12]

Charles A. Desoer and Mathukumalli Vidyasagar. 1975. Feedback Systems: Input-Output Properties. Vol. 55. SIAM (1975).

Digital Library

[13]

Alexandre Donzé. 2015. Breach, a toolbox for verification and parameter synthesis of hybrid systems. In CAV (2015). Springer, 167--170.

Digital Library

[14]

Alexandre Donzé and Oded Maler. 2007. Systematic simulation using sensitivity analysis. In HSCC (2007). Springer, 174--189.

Digital Library

[15]

Parasara Sridhar Duggirala, Chuchu Fan, Sayan Mitra, and Mahesh Viswanathan. 2015. Meeting a powertrain verification challenge. In CAV (2015). Springer, 536--543.

[16]

Parasara Sridhar Duggirala, Sayan Mitra, and Mahesh Viswanathan. 2013. Verification of annotated models from executions. In EMSOFT (2013). IEEE Press, 26:1--26:10.

Digital Library

[17]

Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan, and Matthew Potok. 2015. C2E2: A verification tool for stateflow models. In TACAS (2015). Springer, 68--82.

Digital Library

[18]

Parasara Sridhar Duggirala, Le Wang, Sayan Mitra, Mahesh Viswanathan, and César Muñoz. 2014. Temporal precedence checking for switched models and its application to a parallel landing protocol. In Formal Methods (2014). Springer, 215--229.

Digital Library

[19]

A. El-Guindy, D. Han, and M. Althoff. 2016. Formal analysis of drum-boiler units to maximize the load-following capabilities of power plants. IEEE Trans. on Power Syst. (2016), vol. 31, 6, 4691--4702.

[20]

Chuchu Fan, James Kapinski, Xiaoqing Jin, and Sayan Mitra. 2016. Locally optimal reach set over-approximation for nonlinear systems. In EMSOFT (2016). ACM, 6:1--6:10.

Digital Library

[21]

Chuchu Fan and Sayan Mitra. 2015. Bounded verification with on-the-fly discrepancy computation. In ATVA (2015). Springer, 446--463.

[22]

Raena Farhadsefat, Ji Rohn, and Taher Lotfi. 2011. Norms of Interval Matrices. Technical Report No. V-1122 (2011). Institute of Computer Science, Academy of Sciences of the Czech Republic.

[23]

Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. 2011. SpaceEx: Scalable verification of hybrid systems. In CAV (2011), Shaz Qadeer Ganesh Gopalakrishnan (Ed.). Springer.

Digital Library

[24]

Antoine Girard, Giordano Pola, and Paulo Tabuada. 2010. Approximately bisimilar symbolic models for incrementally stable switched systems. IEEE Trans. Automat. Control 55, 1 (2010), 116--126.

[25]

Gene H. Golub and Charles F. Van Loan. 1996. Matrix Computations (3rd ed.). Johns Hopkins University Press (1996), Baltimore, MD.

Digital Library

[26]

Ashutosh Gupta, Rupak Majumdar, and Andrey Rybalchenko. 2009. From tests to proofs. In TACAS (2009). Springer, 262--276.

Digital Library

[27]

Zhenqi Huang, Chuchu Fan, Alexandru Mereacre, Sayan Mitra, and Marta Z. Kwiatkowska. 2014. Invariant verification of nonlinear hybrid automata networks of cardiac cells. In CAV (2014). Springer, 373--390.

Digital Library

[28]

Zhenqi Huang and Sayan Mitra. 2014. Proofs from simulations and modular annotations. In HSCC (2014). ACM Press.

Digital Library

[29]

Zhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur, and Rahul Mangharam. 2012. Modeling and verification of a dual chamber implantable pacemaker. In TACAS (2012). Springer, 188--203.

Digital Library

[30]

A. Agung Julius, Georgios E. Fainekos, Madhukar Anand, Insup Lee, and George J. Pappas. 2007. Robust test generation and coverage for hybrid systems. In HSCC (2007). Springer, 329--342.

Digital Library

[31]

A. Agung Julius and George J. Pappas. 2009. Trajectory based verification using local finite-time invariance. In HSCC (2009). Springer, 223--236.

Digital Library

[32]

James Kapinski, Jyotirmoy V. Deshmukh, Sriram Sankaranarayanan, and Nikos Aréchiga. 2014. Simulation-guided lyapunov analysis for hybrid dynamical systems. In HSCC (2014). ACM, 133--142.

Digital Library

[33]

Soonho Kong, Sicun Gao, Wei Chen, and Edmund Clarke. 2015. dReach: -reachability analysis for hybrid systems. In TACAS (2015). Springer, 200--205.

Digital Library

[34]

Alexander Kurzhanskii and István Vályi. 2012. Ellipsoidal Calculus for Estimation and Control. Nelson Thornes (1997).

[35]

Daniel Liberzon. 2012. Switching in Systems and Control. Springer Science 8 Business Media (2012).

[36]

J. Löfberg. 2004. YALMIP: A toolbox for modeling and optimization in MATLAB. In CACSD (2004). Retrieved from http://users.isy.liu.se/johanl/yalmip/pmwiki.php?n=Main.HomePage.

[37]

Winfried Lohmiller and Jean-Jacques E. Slotine. 1998. On contraction analysis for non-linear systems. Automatica 34, 6 (1998), 683--696.

Digital Library

[38]

John Maidens and Murat Arcak. 2015. Reachability analysis of nonlinear systems using matrix measures. IEEE Trans. Automat. Control 60, 1 (2015), 265--270.

[39]

Ned Nedialkov. 2006. VNODE-LP: Validated Solutions for Initial Value Problem for ODEs. Technical Report (2006). McMaster University.

[40]

Antonis Papachristodoulou and Stephen Prajna. 2005. Analysis of non-polynomial systems using the sum of squares decomposition. In Positive Polynomials in Control (2005). Springer, 23--43.

[41]

Eduardo D. Sontag. 2010. Contractive systems with inputs. In Perspectives in Mathematical System Theory, Control, and Signal Processing (2010). Springer, 217--228.

[42]

Romain Testylier and Thao Dang. 2013. NLTOOLBOX: A library for reachability computation of nonlinear dynamical systems. In ATVA (2013). Springer, 469--473.

[43]

Reha H. Tütüncü, Kim C. Toh, and Michael J. Todd. 2003. Solving semidefinite-quadratic-linear programs using SDPT3. Math. Program. 95, 2 (2003), 189--217.

[44]

Mahdi Zamani, Giordano Pola, Manuel Mazo, and Paulo Tabuada. 2012. Symbolic models for nonlinear control systems without stability assumptions. IEEE Trans. Automat. Control 57, 7 (2012), 1804--1809.

Cited By

Liu ZJafarpour SChen Y(2024)Safety Verification of Stochastic Systems: A Set-Erosion ApproachIEEE Control Systems Letters10.1109/LCSYS.2024.35183948(2859-2864)Online publication date: 2024
https://doi.org/10.1109/LCSYS.2024.3518394
Sibai HMitra S(2023)State Estimation of Continuous-Time Dynamical Systems With Uncertain Inputs With Bounded Variation: Entropy, Bit Rates, and Relation With Switched SystemsIEEE Transactions on Automatic Control10.1109/TAC.2023.325051068:12(7041-7056)Online publication date: Dec-2023
https://doi.org/10.1109/TAC.2023.3250510
Thompson EXu YWei P(2023)One-Shot Strategically Deconflicted Route and Operational Volume Generation for Urban Air Mobility Operations2023 IEEE 26th International Conference on Intelligent Transportation Systems (ITSC)10.1109/ITSC57777.2023.10421827(5174-5181)Online publication date: 24-Sep-2023
https://doi.org/10.1109/ITSC57777.2023.10421827
Show More Cited By

Index Terms

Simulation-Driven Reachability Using Matrix Measures
1. Computer systems organization
  1. Embedded and cyber-physical systems
    1. Embedded systems
      1. Embedded software

Recommendations

Adaptive backstepping controller design for nonlinear uncertain systems using fuzzy neural systems

In this article, we propose an adaptive backstepping control scheme using fuzzy neural networks FNNs, ABC_FNN, for a class of nonlinear non-affine systems in non-triangular form. The nonlinear non-affine system contains the uncertainty, external ...
Adaptive H∞ tracking control for a class of uncertain nonlinear systems using radial-basis-function neural networks

In this paper, we propose a novel adaptive H"~ tracking controller design for a class of nonlinear systems with uncertain system and gain function, which are unstructured (or non-repeatable) and state-dependent unknown nonlinear functions. Both the ...
Robust tracking control for uncertain MIMO nonlinear systems with input saturation using RWNNDO

In this paper, the robust tracking control scheme is proposed for a class of uncertain multi-input and multi-output (MIMO) nonlinear systems with input saturation and unknown external disturbance based on the recurrent wavelet neural network disturbance ...

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Embedded Computing Systems

ACM Transactions on Embedded Computing Systems Volume 17, Issue 1

Special Issue on Autonomous Battery-Free Sensing and Communication, Special Issue on ESWEEK 2016 and Regular Papers

January 2018

630 pages

ISSN:1539-9087

EISSN:1558-3465

DOI:10.1145/3136518

Editor:
Sandeep K. Shukla
Indian Institute of Technology, India

Issue’s Table of Contents

Copyright © 2017 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 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

ACM Journals for the Design of Smart and Connected Systems

Publication History

Published: 06 December 2017

Accepted: 01 July 2017

Revised: 01 July 2017

Received: 01 February 2017

Published in TECS Volume 17, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

National Science Foundations research

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
230
Total Downloads

Downloads (Last 12 months)39
Downloads (Last 6 weeks)7

Reflects downloads up to 27 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Liu ZJafarpour SChen Y(2024)Safety Verification of Stochastic Systems: A Set-Erosion ApproachIEEE Control Systems Letters10.1109/LCSYS.2024.35183948(2859-2864)Online publication date: 2024
https://doi.org/10.1109/LCSYS.2024.3518394
Sibai HMitra S(2023)State Estimation of Continuous-Time Dynamical Systems With Uncertain Inputs With Bounded Variation: Entropy, Bit Rates, and Relation With Switched SystemsIEEE Transactions on Automatic Control10.1109/TAC.2023.325051068:12(7041-7056)Online publication date: Dec-2023
https://doi.org/10.1109/TAC.2023.3250510
Thompson EXu YWei P(2023)One-Shot Strategically Deconflicted Route and Operational Volume Generation for Urban Air Mobility Operations2023 IEEE 26th International Conference on Intelligent Transportation Systems (ITSC)10.1109/ITSC57777.2023.10421827(5174-5181)Online publication date: 24-Sep-2023
https://doi.org/10.1109/ITSC57777.2023.10421827
Neubauer SGrosu R(2022)Robustness Analysis of Continuous-Depth Models with Lagrangian TechniquesPrinciples of Systems Design10.1007/978-3-031-22337-2_30(625-649)Online publication date: 29-Dec-2022
https://doi.org/10.1007/978-3-031-22337-2_30
Coogan S(2020)Mixed Monotonicity for Reachability and Safety in Dynamical Systems2020 59th IEEE Conference on Decision and Control (CDC)10.1109/CDC42340.2020.9304391(5074-5085)Online publication date: 14-Dec-2020
https://doi.org/10.1109/CDC42340.2020.9304391
Gruenbacher SCyranka JLechner MIslam MSmolka SGrosu R(2020)Lagrangian Reachtubes: The Next Generation2020 59th IEEE Conference on Decision and Control (CDC)10.1109/CDC42340.2020.9304042(1556-1563)Online publication date: 14-Dec-2020
https://doi.org/10.1109/CDC42340.2020.9304042
Sogokon AJackson PJohnson T(2019)Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous InvariantsJournal of Automated Reasoning10.1007/s10817-018-9497-x63:4(1005-1029)Online publication date: 1-Dec-2019
https://dl.acm.org/doi/10.1007/s10817-018-9497-x
Sibai HMitra S(2018)State Estimation of Dynamical Systems with Unknown InputsProceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)10.1145/3178126.3178150(217-226)Online publication date: 11-Apr-2018
https://dl.acm.org/doi/10.1145/3178126.3178150

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 Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents