0
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Deductive Stability Proofs for Ordinary Differential Equations

      Preprint
      ,

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          Stability is required for real world controlled systems as it ensures that they can tolerate small, real world perturbations around their desired operating states. This paper shows how stability for continuous systems modeled by ordinary differential equations (ODEs) can be formally verified in differential dynamic logic (dL). The key insight is to specify ODE stability by suitably nesting the dynamic modalities of dL with first-order logic quantifiers. Elucidating the logical structure of stability properties in this way has three key benefits: i) it provides a flexible means of formally specifying various stability properties of interest, ii) it yields rigorous proofs of those stability properties from dL's axioms with dL's ODE safety and liveness proof principles, and iii) it enables formal analysis of the relationships between various stability properties which, in turn, inform proofs of those properties. These benefits are put into practice through an implementation of stability proofs for several examples in KeYmaera X, a hybrid systems theorem prover based on dL.

          Related collections

          Author and article information

          Journal
          25 October 2020
          Article
          2010.13096
          27cf3b5d-0b86-4b57-aad4-4fdf4e6b2809

          http://arxiv.org/licenses/nonexclusive-distrib/1.0/

          History
          Custom metadata
          03B70, 34A38, 34D05, 93D05
          cs.LO

          Theoretical computer science
          Theoretical computer science

          Comments

          Comment on this article