Restructuring Dynamical Systems for Inductive Verification
Vishnu Murali, Ashutosh Trivedi, Majid Zamani · IEEE Open Journal of Control Systems · 2023
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 tostrengthenthe 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 considerstructuralchanges. 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 orrestructuringof the system is fundamental to inductive approaches. This position paper 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.