Restructuring Dynamical Systems for Inductive Verification

Abstract

Inductive approaches to deductive verification has gained widespread adoption in the control and verification of safety-critical dynamical systems. The practical success of barrier certificates attests to their effectiveness and ongoing theoretical and practical refinement. However, when verification conditions are non-inductive, various strategies are employed to address this issue. One strategy is to strengthen the property until they arrive at an inductive proof. However, it is not always obvious how one must strengthen a property. Notions of strenghtening are particularly non-obvious when the properties of interest are more expressive than safety or reachability. An alternative technique is to instead consider structural changes. These structural changes may either be to consider novel notions of induction such as $k$-induction, or to encode additional information similar to dimension lifting. We posit that reformulating or restructuring of the system is fundamental to inductive approaches. This position article provides an overview of barrier certificate based verification approaches and their connection to system restructuring. We discuss the opportunities, challenges, and open problems in this emerging field, paving the way for future research in the verification of safety-critical dynamical systems. The framework of restructuring of a system holds promise for advancing deductive verification, enhancing system safety, and promoting design insights.

Keywords

• Barrier certificates
• cyber-physical systems
• formal verification
• induction
• safety