key: cord-0060435-02of35ab authors: Tan, Yong Kiam; Platzer, André title: Deductive Stability Proofs for Ordinary Differential Equations date: 2021-02-26 journal: Tools and Algorithms for the Construction and Analysis of Systems DOI: 10.1007/978-3-030-72013-1_10 sha: 11b37382be60b029b876d273050642c9b16ec198 doc_id: 60435 cord_uid: 02of35ab Stability is required for real world controlled systems as it ensures that those systems 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. The study of stability has its roots in efforts to understand mechanical systems, particularly those arising in celestial mechanics [15, 19, 30] . Today, it is an important part of numerous applications in dynamical systems [34] and control theory [14, 18] . This paper studies proofs of stability for continuous dynamical systems described by ordinary differential equations (ODEs), such as those used to model feedback control systems [14, 18] . For such systems, ODE stability is a key correctness requirement [2] that deserves fully rigorous proofs alongside other key properties such as safety and liveness of those ODEs [28, 36] . Despite this, formal stability verification has received less attention compared to proofs of safety and liveness, e.g., through reachability or deductive techniques [8] . Stability for a continuous system (or ODEs) requires that i) its system state always stays close to some desired operating state(s) when initially slightly perturbed from those operating state(s), and ii) those perturbations are eventually dissipated so the system returns to a desired operating state. These properties are especially crucial for engineered systems because they must be robust to real world perturbations deviating from idealized system models. Simple pendulums provide canonical examples of stability phenomena: they are always observed to settle in the rest position of Fig. 1 (bottom) after some time regardless of how they are initially released. In contrast, the inverted pendulum in Fig. 1 (top) is theoretically also at a resting position but can only be observed transiently in practice because the slightest real world perturbation will cause the pendulum to fall due to gravity. Stability explains these observations-the resting position is (asymptotically) stable while the inverted position is unstable and requires active control to ensure its stability. Proofs of safety and liveness properties are still required for the inverted pendulum under control, e.g., its controller must never generate unsafe amounts of torque and the pendulum must eventually reach the inverted position. The triumvirate of safety, liveness, and stability is required for holistic correctness of the inverted pendulum controller. The classical way of distinguishing the aforementioned stability situations is by designing a Lyapunov function [19] , i.e., an energy-like auxiliary measure satisfying certain arithmetical conditions [14, 18, 31] which implies that the auxiliary energy decreases along system trajectories towards local minima at the stable resting state(s), see Fig. 2 . Prior approaches [1, 12, 17, 21, 33] have emphasized the need to formally verify those arithmetical conditions in order to guarantee that a conjectured Lyapunov function correctly implies stability for a given system. This paper shows how deductive proofs of ODE stability can be carried out in differential dynamic logic (dL) [25, 26, 27] , a logic for deductive verification of hybrid systems. 1 The key insight is that stability properties can be specified by suitably nesting the dynamic modalities of dL with quantifiers of first-order logic. The resulting specifications are amenable to rigorous proof by combining dL's ODE safety [28] and liveness [36] proof principles with real arithmetic and first-order quantifier reasoning. This makes it possible to syntactically derive stability for a given system from the small set of dL axioms which, in turn, enables trustworthy stability proofs in the KeYmaera X theorem prover for hybrid systems [11, 26] . Notably, this approach directly verifies stability specifications, which goes beyond verifying arithmetic that imply those specifications [1, 12, 17, 21, 33] . This is crucial for advanced stability notions because those variations generally require subtle twists to the required arithmetical conditions on their Lyapunov functions [14] ; proofs of stability specifications alleviate the onus on system designers to correctly pick and check the appropriate conditions for their applications. Section 3 shows how various stability properties for ODE equilibria can be formally specified and proved in dL with Lyapunov function techniques. Section 4 generalizes those stability specifications, yielding unambiguous formal specifications of advanced stability properties from the literature [14, 18] , along with their derived proof rules. These specifications also provide rigorous insights into the logical relationship between various stability notions, which are used to inform their respective proofs. Section 5 illustrates the practicality of this paper's dL approach through several stability case studies formalized in KeYmaera X. All omitted definitions and proofs are available in the supplement [35] . This section briefly recalls the syntax and semantics of dL, focusing on its continuous fragment which has a complete axiomatization for ODE invariants [28] . Full presentations of dL, including its discrete fragment, are elsewhere [26, 27] . Syntax and Semantics. The grammar of dL terms is as follows, where x ∈ V is a variable and c ∈ Q is a rational constant. These terms are polynomials over V (extensions with Noetherian functions [28] such as exp, sin, cos are possible): The grammar of dL formulas is as follows, where ∼ ∈ {=, =, ≥, >, ≤, <} is a comparison operator and α is a hybrid program: This grammar features atomic comparisons (p ∼ q), propositional connectives (¬, ∧, ∨), first-order quantifiers over the reals (∀ , ∃ ), and the box ([α]φ) and diamond ( α φ) modality formulas which express that all or some runs of hybrid program α satisfy φ, respectively. The modalities [·], · can be freely nested with first-order and modal connectives, which is crucial for the specification of stability properties in Sections 3 and 4. Formulas not containing the modalities are formulas of first-order real arithmetic and are written as P, Q, R. This paper focuses on the continuous fragment of hybrid programs α ≡ is an n-dimensional system of ordinary differential equations (ODEs), x 1 =f 1 (x), . . . , x n =f n (x), over variables x = (x 1 , . . . , x n ), the LHS x i is the time derivative of x i and the RHS f i (x) is a polynomial over variables x. The evolution domain constraint Q specifies the set of states in which the ODE is allowed to evolve continuously. When Q is the formula true, the ODE is also written as x = f (x). For n-dimensional vectors x, y, the dot product is x·y def = n i=1 x i y i and x 2 def = n i=1 x 2 i denotes the squared Euclidean norm. Variables z ∈ V \ {x} not occurring on the LHS of ODE x = f (x) are parameters that remain constant along ODE solutions. The following parametric ODE model of a simple pendulum is used as a running example. Example 1 (Pendulum model). The ODE α p ≡ θ = ω, ω = − g L sin(θ) − bω models a pendulum (illustrated below) suspended from a pivot by a rod of length L, where θ is the angle of displacement, ω is the angular velocity of the pendulum, and g > 0 is the gravitational constant. Parameter a = g L is a positive scaling constant and parameter b ≥ 0 is the coefficient of friction for angular velocity. The symbolic parameters a, b make analysis of α p apply to a range of concrete values, e.g., pendulums that are suspended by a long rod (with large L) are modeled by small positive values of a, while frictionless pendulums have b = 0. L g ω θ A simplification of α p is used because stability analyses often concern the behavior of the pendulum near its resting (or inverted) state where θ = 0. For such nearby states with θ ≈ 0, the small angle approximation sin(θ) ≈ θ yields a linear ODE: 2 An inverted pendulum is modeled by a similar ODE (illustrated on the right) under a change of coordinates. Such a pendulum requires an external torque input u(θ, ω) to maintain its stability; u(θ, ω) is determined and proved correct in Section 5. States ν : V → R assign real values to each variable in V; the set of all states is S. The semantics of dL formula φ is the set of states [[φ]] ⊆ S in which φ is true [26, 27] , where the semantics of first-order logical connectives are defined as usual, e.g., ]. For ODEs, the semantics of the modal operators is as follows. 3 Let ν ∈ S and ϕ : [0, T ) → S for some 0 < T ≤ ∞, be the unique, right-maximal solution [6] to ODE x = f (x) with initial value ϕ(0) = ν: For a formula P the ε-neighborhood of P with respect to x is defined as ≡ ∃y x − y 2 < ε 2 ∧ P (y) , where the existentially quantified variables y are fresh in P . The neighborhood formula U ε (P ) characterizes the set of states within distance ε from P , with respect to the dynamically evolving variables x. This is useful for syntactically expressing small ε perturbations in the stability definitions of Sections 3 and 4. For formulas P of first-order real arithmetic, the ε-neighborhood, U ε (P ), can be equivalently expressed in quantifier-free form by quantifier elimination [4] . For example, U ε (x = 0) is equivalent to the formula x 2 < ε 2 . Formulas P and ∂P are the syntactically definable topological closure and boundary of the set characterized by P , respectively [4] . Proof Calculus. All derivations and proof rules are presented in a classical sequent calculus. The semantics of sequent Γ φ is equivalent to the formula ( ψ∈Γ ψ) → φ. A sequent is valid iff its corresponding formula is valid. Completed branches in a sequent proof are marked with * . Assumptions ψ ∈ Γ that have only ODE parameters as free variables remain true along ODE evolutions and are soundly kept across ODE deduction steps [26, 27] . First-order real arithmetic is decidable [4] so we assume such a decision procedure and label proof steps with R when they follow from real arithmetic. Axioms and proof rules are derivable iff they can be deduced from sound dL axioms and proof rules [26, 27] . The dL proof calculus is complete for ODE invariants [28] , i.e., any true ODE invariant expressible in first-order real arithmetic can be proved in the calculus. The calculus also supports refinement reasoning [36] for proving ODE liveness properties , whose semantic value is equal to the time derivative of the value of p along solutions ϕ of the ODE [26, 28] . They are provably definable in dL using syntactic differentials [26] . This section presents Lyapunov's classical notion of asymptotic stability [19] and its formal specification in dL. This formalization enables the derivation of dL stability proof rules with Lyapunov functions [14, 18, 19, 31] . Several related stability concepts are formalized in dL, along with their relationships and rules. , so a system that starts at x 0 stays at x 0 along its continuous evolution. Such points are often interesting in real-world systems, e.g., the equilibrium point θ = 0, ω = 0 for α l from (1) is the resting state of a pendulum. For a controlled system, equilibrium points often correspond to desired steady system states where no further continuous control input (modeled as part of f (x)) is required [18] . For brevity, assume the origin 0 ∈ R n is an equilibrium point of interest. Any other equilibrium point(s) of interest x 0 ∈ R n can be translated to the origin with the change of coordinates x → x − x 0 for the ODE (see supplement [35] ). . Solutions from points in the δ ball around the origin, like the green initial point x, remain within the ε ball around the origin 0 ∈ R n (black dot) and asymptotically approach the origin. The latter two plots illustrate how asymptotic stability for an ODE can be broken down into a pair of (quantified) ODE safety and liveness properties. The following definition of asymptotic stability is standard [14, 18, 31] . 4 Definition 2 (Asymptotic stability [14, 18, 31] ). The origin 0 ∈ R n of ODE These definitions can be understood using the resting state of the pendulum from Fig. 1 (bottom) which is asymptotically stable. When the pendulum is given a light push from its bottom resting state (formally, x < δ), it gently oscillates near that resting state (formally, x(t) < ε). In the presence of friction, these oscillations eventually dissipate so the pendulum asymptotically returns to its resting state (formally, lim t→T x(t) = 0). This behavior is local, i.e., for any given ε > 0, there exists a sufficiently small δ > 0 perturbation of the initial state that results in gentle oscillations with x(t) < ε, see Fig. 3 (left). A strong push, e.g., with δ > ε, could instead cause the pendulum to spin around on its pivot. However, if the origin is stable, attractivity can be defined in a simpler way. This is proved in dL, after characterizing stability and attractivity syntactically. The formal specification of asymptotic stability in dL combines i) the dynamic modalities of dL, which are used to quantify over the dynamics of the ODE, and ii) the first-order logic quantifiers, which are used to express combinations of (topologically) local and asymptotic properties of those dynamics. Lemma 4 (Asymptotic stability in dL). The origin of ODE x = f (x) is, respectively, i) stable, ii) attractive, and iii) asymptotically stable iff the dL formulas i) Stab(x = f (x)), ii) Attr(x = f (x)), and iii) AStab(x = f (x)) respectively are valid. Variables ε, δ are fresh, i.e., not in x, f (x). terizes the set of states that asymptotically approach P along ODE solutions. expresses that solutions starting from the δ-neighborhood of the origin always (for all times) stay safely in the ε-neighborhood, as visualized in Fig. 3 (middle). Formula Attr(x = f (x)) uses the subformula Asym(x = f (x), x = 0) which characterizes the limit in Def. 2. Recall lim t→T x(t) = 0 iff for all ε > 0 there exists a time τ with 0 ≤ τ < T such that for all times t with τ ≤ t < T , the solution satisfies x(t) < ε, i.e., the limit requires for all distances ε > 0, the ODE solution will eventually always be within distance ε of the origin, as visualized in Fig. 3 (right) . This limit is characterized using nested · [·] modalities, together with first-order quantification according to Def. 2. More generally, formula Asym(x = f (x), P ) characterizes the set of initial states where the right-maximal ODE solution asymptotically approaches P ; this set is known as the region of attraction of P [18] . Thus, attractivity requires that the region of attraction of the origin contains an open neighborhood U δ (x = 0) of the origin. From Lemma 4, proving validity of the formula AStab(x = f (x)) yields a rigorous proof of asymptotic stability for x = f (x). However, if the origin is stable, then attractivity can be provably simplified with the following corollary. Corollary 5 (Stable attractivity). The following axiom is derivable in dL. Corollary 5 simplifies the syntactic characterization of the region of attraction for stable equilibria from a nested · [·] formula to a · formula, which is then directly amenable to ODE liveness reasoning [36] . This corollary is used to simplify proofs of asymptotic stability, as explained next. Lyapunov functions are the standard tool for showing stability of general, nonlinear ODEs [14, 18, 31] and finding suitable Lyapunov functions is an important problem in its own right [1, 9, 12, 17, 21, 23, 24, 33, 37] . This section shows how a candidate Lyapunov function, once found, can be used to rigorously prove stability. The following proof rules derive Lyapunov stability arguments [14, 18, 31] syntactically in dL. Lemma 6 (Lyapunov functions). The following Lyapunov function proof rules are derivable in dL. Rules Lyap ≥ , Lyap > use the Lyapunov function v as an auxiliary, energylike function near the origin which is positive and has non-positive (resp. negative Lyap > ) derivative . v. This guarantees that v is non-increasing (resp. decreasing) along ODE solutions near the origin, see Fig. 2 . The right premise of both rules use ∃γ>0 ∀x 0< x 2 ≤γ 2 → · · · to require that the Lyapunov function conditions are true in a γ-neighborhood of the origin. The subtle difference in sign condition for . v between rules Lyap ≥ , Lyap > is illustrated for the pendulum. Example 7 (Pendulum asymptotic stability). For ODE α l from (1), a suitable Lyapunov function for proving its stability [18] is . Stability 5 is formally proved in dL for any parameter values a > 0, b ≥ 0 using rule Lyap ≥ because both of its resulting arithmetical premises are provable by R. The full dL derivation, also used in KeYmaera X (Section 5), is shown in the proof of Lemma 6 [35] . When b > 0, i.e., friction is non-negligible, an identical derivation with Lyap > instead of Lyap ≥ proves asymptotic stability because − b 2 (aθ 2 + ω 2 ) is negative except at the origin. Indeed, displacements to the pendulum's resting state can only be dissipated in the presence of friction, not when b = 0. Asymptotic stability is a strong guarantee about the local behavior of ODE solutions near equilibrium points of interest. In certain applications, stronger stability guarantees may be needed for those equilibria [18] . This section examines two standard stability variations, shows how they can be proved in dL, and formally analyzes their logical relationship with asymptotic stability. Exponential stability As the name suggests, the first stability variation, exponential stability, guarantees an exponential rate of convergence towards the equilibrium point from an initial displacement. This is useful, e.g., for bounding the time spent by a perturbed system far away from its desired operating state. Definition 8 (Exponential stability [14, 18, 31] ). The origin 0 ∈ R n of ODE x = f (x) is exponentially stable if there are positive constants α, β, δ > 0 such that for all initial states x = x(0) with x < δ, the right-maximal ODE solution x(t) : [0, T ) → R n satisfies x(t) ≤ α x(0) exp (−βt) for all times 0 ≤ t < T . 5 For the trigonometric pendulum ODE αp from Example 1, the Lyapunov function v = a(1 − cos(θ)) + (bθ+ω) 2 +ω 2 4 with Lie derivative 2 (aθ sin(θ) + ω 2 ) proves its stability [18] but requires arithmetic reasoning over trigonometric functions. Exponential stability bounds the norm of solutions to ODE x = f (x) near the origin by a decaying exponential. It is specified in dL as follows. Lemma 9 (Exponential stability in dL). The origin of ODE x = f (x) is exponentially stable iff the following dL formula is valid. Variables α, β, δ, y are fresh, i.e., not in x, f (x). EStab The discrete assignment y := α 2 x 2 sets the value of variable y to that of α 2 x 2 and ; denotes sequential composition of hybrid programs [26, 27] . Formula EStab(x = f (x)) uses a fresh variable y with ODE y = −2βy and initialized to α 2 x 2 so that y differentially axiomatizes [28] the (squared) decaying exponential function α 2 x(0) 2 exp (−2βt) along ODE solutions. Such an implicit (polynomial) characterization of exponential decay allows syntactic proof steps to use decidable real arithmetic reasoning. Lemma 10 (Lyapunov function for exponential stability). The following Lyapunov function proof rule for exponential stability is derivable in dL, where k 1 , k 2 , k 3 ∈ Q are positive constants. Rule Lyap E enables proofs of exponential stability in dL. In fact, the proof of Lemma 10 (see supplement [35] ) yields concrete, quantitative bounds, where EStab(x = f (x)) is explicitly witnessed with scaling constant α = k2 k1 and decay rate β = k 3 . These can be used to calculate time bounds when the system state will return sufficiently close to the origin. Similarly, the disturbance δ in EStab(x = f (x)) is quantitatively witnessed by k1 k2 γ for any γ witnessing validity of the premise of rule Lyap E . This yields a provable estimate of the region around the origin where exponential stability holds; this latter estimate is explored next. Attr(x = f (x)) and EStab(x = f (x)) both feature a subformula of the form ∃δ > 0 ∀x (U δ (x = 0) → · · · ) which expresses that attractivity (or exponential stability) is locally true in some δ neighborhood of the origin. In many applications, it is useful to find and rigorously prove that a given set is attractive or exponentially stable with respect to the origin [18, Chapter 8.2]. The second stability variation yields provable subsets of the region of attraction, including the special case where it is the entire state space. This is formalized using the following variants of Attr(x = f (x)) and EStab(x = f (x)) within a region given by a formula P . The formula Attr P (x = f (x), P ) is valid iff the set characterized by P is a subset of the origin's region of attraction [18] . For example, Attr(x = f (x)) is ∃δ > 0 Attr P (x = f (x), U δ (x = 0)). This generalization is useful for formalizing stronger notions of stability in dL, such as the following global stability notions [14, 18] . For brevity, dL specifications of the stability properties (in bold) are given below with mathematical definitions deferred to the supplement [35] . Lemma 11 (Global stability in dL). The origin of ODE x = f (x) is globally asymptotically stable iff the dL formula Stab(x = f (x)) ∧ Attr P (x = f (x), true) is valid. The origin is globally exponentially stable iff the dL formula EStab P (x = f (x), true) is valid. Global stability ensures that all perturbations to the system state are eventually dissipated. Their proof rules are similar to Lyap > and Lyap E respectively. Lemma 12 (Lyapunov function for global stability). The following Lyapunov function proof rules for global asymptotic and exponential stability are derivable in dL. In rule Lyap G E , k 1 , k 2 , k 3 ∈ Q are positive constants. Lyap ≤ v ≤ θ 2 + ω 2 and . v ≤ − 1 2 v. Thus, rule Lyap G E proves global exponential stability of α l with k 1 = 1 2 , k 2 = 1, and k 3 = 1 4 . An important caveat is that Example 7 used a local small angle approximation, so this global phenomenon does not hold for a real world pendulum (nor for α p ). Logical relationships With the proliferation of stability variations just introduced, it is useful to take stock of their logical relationships. An important example of such a relationship is shown in the following corollary. Corollary 14 (Exponential stability implies asymptotic stability). The following axioms are derivable in dL. Derived axioms EStabStab, EStabAttr show that exponential stability implies asymptotic stability. In proofs, EStabAttr allows the region of attraction to be estimated using the region where solutions are exponentially bounded. This section provides stability definitions and proof rules that generalize stability for an equilibrium point from Section 3 to the stability of sets. These definitions are useful when the desired stable system state(s) is not modeled by a single equilibrium point, but may instead, e.g., lie on a periodic trajectory [18] , a hyperplane, or a continuum of equilibrium points within the state space [14] . The generalized definition is used to formalize two stability notions from the literature [14, 18] , and to justify their Lyapunov function proof rules. The following general stability formula defines stability in dL with respect to an ODE x = f (x) and formulas P, R. The quantified variables ε, δ are assumed to be fresh by bound renaming, i.e., do not appear in x, f (x), P or R. This formula generalizes stability of the origin Stab(x = f (x)) by adding two logical tuning knobs that can be intuitively understood as follows. The precondition P characterizes the initial states from which the system state is expected to be disturbed by some disturbance δ. The postcondition R characterizes the set of desired operating states that the system must remain close (within the ε neighborhood of R) after being disturbed from its initial states. The general attractivity formula similarly generalizes Attr P (x = f (x), P ) with a postcondition R towards which the ODE solutions from initial states satisfying precondition P are asymptotically attracted. Lemma 15 (General Lyapunov functions). The following Lyapunov function proof rule for general stability with two stacked premises is derivable in dL. Rule GLyap proves general stability for precondition P and postcondition R. It generalizes the Lyapunov function reasoning underlying rule Lyap ≥ to support arbitrary pre-and postconditions. The conjunct ∀x (∂(U γ (R)) → v ≥ k) requires v≥k on the boundary of U γ (R) while the middle conjunct requires v I 2 > I 3 > 0 are the principal moments of inertia along the respective axes. When such a rigid object is spun or rotated on each of its axes, a well-known physical curiosity [3] is that the rotation is stable in the first and third axes, whilst additional (unstable) twisting motion is observed for the intermediate axis. Mathematically, a perfect rotation, e.g., around x 1 , corresponds to a (large) initial value for x 1 with no rotation in the other axes, i.e., x 2 = 0, x 3 = 0. Accordingly the real world observation of stability for rotations about the first principal axis is explained by stability with respect to small perturbations in x 2 , x 3 , as formally specified by formula (3) below. Note that the set characterized by formula x 2 = 0∧x 3 = 0 is the entire x 1 axis, not just a single point. Similarly, rotations are stable around the third principal axis iff formula (4) is valid. Stab P R (α r , The validity of formulas (3) and (4) are proved in Example 20. The formal specification of set stability yields three provable logical consequences which are important stepping stones for the set stability proof rules. Corollary 18 (Set stability properties). The following axioms are derivable in dL. In axiom SClosure, formula P characterizes the topological closure of formula P . In axiom SClosed, formula P characterizes a closed set. Stab Axiom SetSAttr generalizes SAttr and provides a syntactic simplification of the region of attraction for formula P when P is stable. Axiom SClosure says that stability of P is equivalent to stability of its closure P , because for any perturbation δ > 0, the neighborhoods U δ (P ) and U δ (P ) are provably equivalent in real arithmetic. Axiom SClosed says that for closed formulas P , invariance of P is a necessary condition for stability of P . Without loss of generality, it suffices to develop proof rules for stability of formulas characterizing closed (using SClosure) and invariant (using SClosed) sets. Indeed, standard definitions of set stability [14, 18] usually assume that the set of concern is closed and invariant. Lemma 19 (Set stability Lyapunov functions). The following Lyapunov function proof rules for set stability are derivable in dL. In derived rules SLyap ≥ and SLyap > , formula P characterizes a compact (i.e., closed and bounded) set. In derived rule SLyap * ≥ , the two premises are stacked. All three proof rules have the necessary premise P [x = f (x)]P which says that formula P is an invariant of the ODE x = f (x). Rules SLyap ≥ , SLyap > are slight generalizations of Lyapunov function proof rules for set stability [14] and they respectively generalize rules Lyap ≥ , Lyap > to prove stability for an invariant P . Importantly, both rules assume that P characterizes a compact, i.e., closed and bounded set, which simplifies the arithmetical conditions on v in their premises. The rule without the boundedness requirement on P suggested in the remark after [18, Definition 8.1] , is unsound, see supplement [35] . For asymptotic stability (in rule SLyap > ), boundedness also guarantees that perturbed ODE solutions always exist for sufficient duration, which is a fundamental step in the ODE liveness proofs [36] . Rule SLyap * ≥ is derived from rule GLyap using invariance of P by the first premise; it provides a means of formally proving the set stability properties (3) and (4) , whose Lie derivative is . v = 0, and rule SLyap * ≥ with formula P ≡ x 2 = 0 ∧ x 3 = 0. The proof for (4) is symmetric. For the top premise of rule SLyap * ≥ , formula P is a provable invariant [28] of the ODE α r . The bottom premise, although arithmetically complicated, can be simplified by choosing γ = ε and deciding the resulting formula by R. Recall that the x 1 axis is not a compact set so neither of the standard proof rules for set stability SLyap ≥ , SLyap > would be sound for this proof. Epsilon-Stability Motivated by numerical robustness of proofs of stability, Gao et al. [12] define ε-stability for ODEs. The following dL characterization shows how ε-stability can be understood as an instance of general stability. Unlike set stability, ε-stability is an instance of general stability where the pre-and postconditions differ. In ε-stability, systems are perturbed from the precondition x = 0 (the origin), but the postcondition enlarges the set of desired states to a ε > 0 neighborhood of the origin, which is considered indistinguishable from the origin itself [12] . An immediate consequence of Lemma 21 is that rule GLyap can be used to prove ε-stability, as shown in the next section. This section puts the dL stability specifications and derivations from the preceding sections into practice through proofs for several case studies in the KeYmaera X theorem prover [11] . 6 Examples 7, 13, 17, 20 have also been formalized. The insights from these proofs are discussed after an overview of the case studies. Inverted Pendulum. The stability of the resting state of the pendulum is investigated in Examples 7 and 13. For the inverted pendulum α i from (2), the controlled torque u(θ, ω) must be designed and rigorously proved to ensure feedback stabilization [18] of the inverted position. A standard PD (Proportional-Derivative) controller can be used for stabilization, where the control input has the form u(θ, ω) = k 1 θ + k 2 ω for tuning parameters k 1 , k 2 . Asymptotic stability of the inverted position is achieved for any control parameter choice where k 1 > a and k 2 > −b. The sequent a > 0, b ≥ 0, k 1 > a, k 2 > −b AStab(α i ) is proved in KeYmaera X using the Lyapunov function (k1−a)θ 2 2 + (((b+k2)θ+ω) 2 +ω 2 ) 4 . 6 See https://github.com/LS-Lab/KeYmaeraX-projects/blob/master/stability Frictional Tennis Racket Theorem. The stability of a 3D rigid body is investigated for α r in Examples 17 and 20. The following ODEs model additional frictional forces that oppose the rotational motion in each axis of the rigid body, where α 1 , α 2 , α 3 > 0 are positive coefficients of friction: In the presence of friction, rotations of the rigid body are globally asymptotically stable in the first and third principal axes, as proved in KeYmaera X. ) Both asymptotic stability properties are proved using SLyap * ≥ and the liveness property [36] that the kinetic energy I 1 x 2 1 + I 2 x 2 2 + I 3 x 2 3 of the system tends to zero over time. The latter property implies that solutions of α f exist globally and that the values of x 1 , x 2 , x 3 asymptotically tend to zero, which proves global asymptotic stability with the aid of SetSAttr. Even though a proof rule for (global) asymptotic stability of general nonlinear ODEs and unbounded sets is not available (Section 4), this example shows that formalized stability properties can still be proved on a case-by-case basis using dL's ODE reasoning principles. Moore-Greitzer Jet Engine [12] . The origin of the ODE modeling a simpli- [12] . The sequent ε = 10 −10 Stab P R (α m , x 2 1 + x 2 2 = 0, x 2 1 + x 2 2 < ε 2 ) is proved in KeYmaera X. The key proof ingredients are an ε-Lyapunov function [12] and manual arithmetic steps, e.g., instantiating existential quantifiers appearing in the specification of ε-stability with appropriate values [12] . Other Examples [1] . Stability for several ODEs with Lyapunov functions generated by an inductive synthesis technique [1, were successfully verified in KeYmaera X. The proof for the largest, 6-dim. nonlinear ODE [1, Example 5] required substantial manual arithmetic reasoning in KeYmaera X. 7 The arithmetical conditions in [1, Equation 1 ] are identical to the premises of rule Lyap ≥ except it unsoundly omits the condition v(0) = 0, see supplement [35] . The generated Lyapunov functions remain correct because the inductive synthesis technique [1] implicitly guarantees this omitted condition. Summary. These case studies demonstrate the feasibility of carrying out proofs of various (advanced) stability properties within KeYmaera X using this paper's stability specifications. The proofs share similar high-level proof structure, which suggests that proof automation could significantly reduce proof effort [10] . Such automation should also support user input of key insights for difficult reasoning steps, e.g., real arithmetic reasoning with nested, alternating quantifiers. 7 The Lyapunov function in [1, Example 5] does not work for its associated ODE. It works if the ODE is corrected withẋ1 = −x 3 1 + 4x 3 2 − 6x3x4, as in the literature [23] . Stability is a fundamental property of interest across many different fields of mathematics [6, 15, 19, 30, 31, 34] and engineering [14, 18, 20] . This related work discussion focuses on formal approaches to stability of ODEs. Logical specification of stability. Rouche, Habets, and Laloy [31] provide a pioneering example of using logical notation to specify and classify stability properties of ODEs. Alternative logical frameworks have also been used to specify stability and related properties: stability is expressed in HyperSTL [22] as a hyperproperty relating the trace of an ODE against two constant traces; -stability is studied in the context of δ-complete reasoning over the reals [12] ; region stability for hybrid systems [29] is discussed using CTL*; the syntactic specification of Asym(x = f (x), P ) resembles the limit definition using filters [16] . This paper uses dL as a sweet spot logical framework, general enough to specify various stability properties of interest, e.g., asymptotic or exponential stability, and the stability of sets, while also enabling syntactic proofs of those properties. Formal verification of stability. There is a vast literature on finding Lyapunov functions for stability, e.g., through numerical [24, 23, 37] and algebraic methods [9, 21] . Formal approaches are often based on finding Lyapunov function candidates and certifying the correctness of those generated candidates [1, 12, 17, 33] . This paper's approach enables highly trustworthy certification of those candidates in dL and KeYmaera X, with stability proof rules that are soundly derived from dL's parsimonious axiomatization [25, 26, 27] , as implemented in KeYmaera X [11, 26] . Sections 4 and 5 further show that this paper's approach supports verification of advanced stability properties [12, 14, 18] within the same dL framework. New stability proof rules like GLyap can also be soundly and syntactically justified in dL without the need for (low-level) semantic reasoning about the underlying ODE mathematics. As an example of the latter, semantic approach, LaSalle's invariance principle is formalized in Coq [7] and used to verify the correctness of an inverted pendulum controller [32] . This paper shows how ODE stability can be formalized in dL using the key idea that stability properties are ∀ /∃ -quantified dynamical formulas. These specifications, their proof rules, and their logical relationships are all syntactically derived from dL's sound proof calculus. This further enables trustworthy KeYmaera X proofs that rigorously verify every step in an ODE stability argument, from arithmetical premises down to dynamical reasoning for ODEs. Directions for future work include i) formalization of stability with respect to perturbations of the system dynamics, and ii) generalizations of stability to hybrid systems. Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. Automated and sound synthesis of Lyapunov functions with SMT solvers Principles of Cyber-Physical Systems The twisting tennis racket Real Algebraic Geometry Handbook of Networked and Embedded Control Systems Ordinary Differential Equations with Applications A formal proof in Coq of LaSalle's invariance principle Verification of hybrid systems Construction of Lyapunov functions using Gröbner bases Bellerophon: Tactical theorem proving for hybrid systems KeYmaera X: an axiomatic tactical theorem prover for hybrid systems Numerically-robust inductive proof rules for continuous dynamical systems Hybrid Dynamical Systems: Modeling, Stability, and Robustness Nonlinear Dynamical Systems and Control: A Lyapunov-Based Approach The dynamical systems approach to differential equations Type classes and filters for mathematical analysis in Isabelle/HOL Simulation-guided Lyapunov analysis for hybrid dynamical systems Nonlinear systems Probléme général de la stabilité du mouvement Switching in Systems and Control. Systems & Control: Foundations & Applications, Birkhäuser Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems Hyperproperties of real-valued signals On the construction of Lyapunov functions using the sum of squares decomposition Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization The complete proof theory of hybrid systems A complete uniform substitution calculus for differential dynamic logic Logical Foundations of Cyber-Physical Systems Differential equation invariance axiomatization Model checking of hybrid systems: From reachability towards stability Les méthodes nouvelles de la mécanique céleste Stability Theory by Liapunov's Direct Method A formal proof in Coq of a control function for the inverted pendulum Lyapunov function synthesis using Handelman representations Nonlinear Dynamics and Chaos: With Applications to Physics Deductive stability proofs for ordinary differential equations An axiomatic approach to existence and liveness for differential equations Local stability analysis using simulations and sum-of-squares programming Acknowledgments. We thank Brandon Bohrer, Stefan Mitsch, and the anonymous reviewers for their helpful feedback on KeYmaera X and this paper.Deductive Stability Proofs for Ordinary Differential Equations