Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems

© The Author(s) 2019. We formulate numerically-robust inductive proof rules for unbounded stability and safety properties of continuous dynamical systems. These induction rules robustify standard notions of Lyapunov functions and barrier certificates so that they can tolerate small numerical errors....

Full description

Bibliographic Details
Format: Article
Language:English
Published: Springer International Publishing 2021
Online Access:https://hdl.handle.net/1721.1/137349
_version_ 1811084263163953152
collection MIT
description © The Author(s) 2019. We formulate numerically-robust inductive proof rules for unbounded stability and safety properties of continuous dynamical systems. These induction rules robustify standard notions of Lyapunov functions and barrier certificates so that they can tolerate small numerical errors. In this way, numerically-driven decision procedures can establish a sound and relative-complete proof system for unbounded properties of very general nonlinear systems. We demonstrate the effectiveness of the proposed rules for rigorously verifying unbounded properties of various nonlinear systems, including a challenging powertrain control model.
first_indexed 2024-09-23T12:47:51Z
format Article
id mit-1721.1/137349
institution Massachusetts Institute of Technology
language English
last_indexed 2024-09-23T12:47:51Z
publishDate 2021
publisher Springer International Publishing
record_format dspace
spelling mit-1721.1/1373492022-04-01T17:27:47Z Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems © The Author(s) 2019. We formulate numerically-robust inductive proof rules for unbounded stability and safety properties of continuous dynamical systems. These induction rules robustify standard notions of Lyapunov functions and barrier certificates so that they can tolerate small numerical errors. In this way, numerically-driven decision procedures can establish a sound and relative-complete proof system for unbounded properties of very general nonlinear systems. We demonstrate the effectiveness of the proposed rules for rigorously verifying unbounded properties of various nonlinear systems, including a challenging powertrain control model. 2021-11-04T15:39:43Z 2021-11-04T15:39:43Z 2019-07 2021-03-26T15:11:33Z Article http://purl.org/eprint/type/JournalArticle https://hdl.handle.net/1721.1/137349 2019. "Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems." Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 11562. en 10.1007/978-3-030-25543-5_9 Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Creative Commons Attribution 4.0 International license https://creativecommons.org/licenses/by/4.0/ application/pdf Springer International Publishing Springer
spellingShingle Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
title Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
title_full Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
title_fullStr Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
title_full_unstemmed Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
title_short Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
title_sort numerically robust inductive proof rules for continuous dynamical systems
url https://hdl.handle.net/1721.1/137349