How Deduction Systems Can Help You To Verify Stability Properties

TL;DR

This paper tackles the gap between human-oriented proofs of stability and machine-checked proofs in control theory by presenting a machine-checked Lyapunov-stability proof for an inverted pendulum within differential dynamic logic ($ extsf{d} extsf{L}$) using KeYmaera X. It demonstrates how a non-trigonometric running variant facilitates automated reasoning and explicitly captures side conditions via a well-formedness constraint, enabling navigation and reuse of the proof. The authors extract the structural pattern of the mechanization, connect problem-family parameter constraints to the deductive proof, and enhance the proof with side-conditions to improve tractability and trust in correctness. They discuss practical implications for adoptability in control engineering, including tooling improvements such as proof-tree visualization and multi-branch navigation, to bridge semantic reasoning and syntactic formalization in stability verification.

Abstract

Mathematical proofs are a cornerstone of control theory, and it is important to get them right. Deduction systems can help with this by mechanically checking the proofs. However, the structure and level of detail at which a proof is represented in a deduction system differ significantly from a proof read and written by mathematicians and engineers, hampering understanding and adoption of these systems. This paper aims at helping to bridge the gap between machine-checked proofs and proofs in engineering and mathematics by presenting a machine-checked proof for stability using Lyapunov's theorem in a human-readable way. The structure of the proof is analyzed in detail, and potential benefits of such a proof are discussed, such as generalizability, reusability and increased trust in correctness.

Figures (6)

• Figure 1: The trigonometric pendulum variant according to \ref{['def:ip-dynamics-nonlin']}: the vector field of $\dot{\mathbf x}$ (upper left), a simulation (upper right), $V$ (lower left), and its total derivative $\dot V$ (lower right)
• Figure 2: Part 1: Decomposing asymptotic stability into stability ($s$) and attractivity ($a$) in $\mathsf{d}\mathcal{L}$-sequent style extracted from DBLP:conf/tacas/TanP21
• Figure 3: Part 2: Proving reachability ($r$) of the equilibrium point $\mathbf x_e$ and any of its environments
• Figure 4: Part 3: Proving stability of the equilibrium point $\mathbf x_e$ based on its reachability
• Figure 5: The non-trigonometric variant according to \ref{['def:ip-dynamics-lin']}