Restructuring Dynamical Systems for Inductive Verification
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 verificatio...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2023-01-01
|
| Series: | IEEE Open Journal of Control Systems |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/10179178/ |
| _version_ | 1797384365279281152 |
|---|---|
| author | Vishnu Murali Ashutosh Trivedi Majid Zamani |
| author_facet | Vishnu Murali Ashutosh Trivedi Majid Zamani |
| author_sort | Vishnu Murali |
| collection | DOAJ |
| description | 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 <italic>strengthen</italic> 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 <italic>structural</italic> changes. These structural changes may either be to consider novel notions of induction such as <inline-formula><tex-math notation="LaTeX">$k$</tex-math></inline-formula>-induction, or to encode additional information similar to dimension lifting. We posit that reformulating or <italic>restructuring</italic> 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. |
| first_indexed | 2024-03-08T21:35:26Z |
| format | Article |
| id | doaj.art-a6c242decc474946bb77185b43684aee |
| institution | Directory Open Access Journal |
| issn | 2694-085X |
| language | English |
| last_indexed | 2024-03-08T21:35:26Z |
| publishDate | 2023-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Open Journal of Control Systems |
| spelling | doaj.art-a6c242decc474946bb77185b43684aee2023-12-21T00:02:07ZengIEEEIEEE Open Journal of Control Systems2694-085X2023-01-01220020710.1109/OJCSYS.2023.329409810179178Restructuring Dynamical Systems for Inductive VerificationVishnu Murali0https://orcid.org/0000-0002-8762-5614Ashutosh Trivedi1https://orcid.org/0000-0001-9346-0126Majid Zamani2https://orcid.org/0000-0001-6608-3708University of Colorado, Boulder, CO, USAUniversity of Colorado, Boulder, CO, USAUniversity of Colorado, Boulder, CO, USAInductive 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 <italic>strengthen</italic> 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 <italic>structural</italic> changes. These structural changes may either be to consider novel notions of induction such as <inline-formula><tex-math notation="LaTeX">$k$</tex-math></inline-formula>-induction, or to encode additional information similar to dimension lifting. We posit that reformulating or <italic>restructuring</italic> 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.https://ieeexplore.ieee.org/document/10179178/Barrier certificatescyber-physical systemsformal verificationinductionsafety |
| spellingShingle | Vishnu Murali Ashutosh Trivedi Majid Zamani Restructuring Dynamical Systems for Inductive Verification IEEE Open Journal of Control Systems Barrier certificates cyber-physical systems formal verification induction safety |
| title | Restructuring Dynamical Systems for Inductive Verification |
| title_full | Restructuring Dynamical Systems for Inductive Verification |
| title_fullStr | Restructuring Dynamical Systems for Inductive Verification |
| title_full_unstemmed | Restructuring Dynamical Systems for Inductive Verification |
| title_short | Restructuring Dynamical Systems for Inductive Verification |
| title_sort | restructuring dynamical systems for inductive verification |
| topic | Barrier certificates cyber-physical systems formal verification induction safety |
| url | https://ieeexplore.ieee.org/document/10179178/ |
| work_keys_str_mv | AT vishnumurali restructuringdynamicalsystemsforinductiveverification AT ashutoshtrivedi restructuringdynamicalsystemsforinductiveverification AT majidzamani restructuringdynamicalsystemsforinductiveverification |