Verification of Approximate Initial-State Opacity for Control Systems via Neural Augmented Barrier Certificates
In this paper, we propose an augmented barrier certificate-based method for formally verifying the approximate initial-state opacity property of discrete time control systems. The opacity verification problem is formulated as the safety verification of an augmented system and is then addressed by se...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2022-07-01
|
| Series: | Mathematics |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2227-7390/10/14/2388 |
| _version_ | 1797417221466619904 |
|---|---|
| author | Shengpu Wang Mi Ding Wang Lin Yubo Jia |
| author_facet | Shengpu Wang Mi Ding Wang Lin Yubo Jia |
| author_sort | Shengpu Wang |
| collection | DOAJ |
| description | In this paper, we propose an augmented barrier certificate-based method for formally verifying the approximate initial-state opacity property of discrete time control systems. The opacity verification problem is formulated as the safety verification of an augmented system and is then addressed by searching for augmented barrier certificates. A set of well-defined verification conditions is a prerequisite for successfully identifying augmented barrier certificates of a specific type. We first suggest a new type of augmented barrier certificate which produces a weaker sufficient condition for approximate initial-state opacity. Furthermore, we develop an algorithmic framework where a <i>learner</i> and a <i>verifier</i> interact to synthesize augmented barrier certificates in the form of neural networks. The <i>learner</i> trains neural certificates via the deep learning method, and the <i>verifier</i> solves several mixed integer linear programs to either ensure the validity of the candidate certificates or yield counterexamples, which are passed back to further guide the <i>learner.</i> The experimental results demonstrate that our approach is more scalable and effective than the existing sum of squares programming method. |
| first_indexed | 2024-03-09T06:15:40Z |
| format | Article |
| id | doaj.art-734e0f2c634c405182bc8ba0e1db5706 |
| institution | Directory Open Access Journal |
| issn | 2227-7390 |
| language | English |
| last_indexed | 2024-03-09T06:15:40Z |
| publishDate | 2022-07-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Mathematics |
| spelling | doaj.art-734e0f2c634c405182bc8ba0e1db57062023-12-03T11:53:21ZengMDPI AGMathematics2227-73902022-07-011014238810.3390/math10142388Verification of Approximate Initial-State Opacity for Control Systems via Neural Augmented Barrier CertificatesShengpu Wang0Mi Ding1Wang Lin2Yubo Jia3School of Information Science and Technology, Zhejiang Sci-Tech University, Hangzhou 310018, ChinaSchool of Information Science and Technology, Zhejiang Sci-Tech University, Hangzhou 310018, ChinaSchool of Information Science and Technology, Zhejiang Sci-Tech University, Hangzhou 310018, ChinaSchool of Information Science and Technology, Zhejiang Sci-Tech University, Hangzhou 310018, ChinaIn this paper, we propose an augmented barrier certificate-based method for formally verifying the approximate initial-state opacity property of discrete time control systems. The opacity verification problem is formulated as the safety verification of an augmented system and is then addressed by searching for augmented barrier certificates. A set of well-defined verification conditions is a prerequisite for successfully identifying augmented barrier certificates of a specific type. We first suggest a new type of augmented barrier certificate which produces a weaker sufficient condition for approximate initial-state opacity. Furthermore, we develop an algorithmic framework where a <i>learner</i> and a <i>verifier</i> interact to synthesize augmented barrier certificates in the form of neural networks. The <i>learner</i> trains neural certificates via the deep learning method, and the <i>verifier</i> solves several mixed integer linear programs to either ensure the validity of the candidate certificates or yield counterexamples, which are passed back to further guide the <i>learner.</i> The experimental results demonstrate that our approach is more scalable and effective than the existing sum of squares programming method.https://www.mdpi.com/2227-7390/10/14/2388approximate initial-state opacitybarrier certificatediscrete-time control systemdeep learningmixed integer linear programming |
| spellingShingle | Shengpu Wang Mi Ding Wang Lin Yubo Jia Verification of Approximate Initial-State Opacity for Control Systems via Neural Augmented Barrier Certificates Mathematics approximate initial-state opacity barrier certificate discrete-time control system deep learning mixed integer linear programming |
| title | Verification of Approximate Initial-State Opacity for Control Systems via Neural Augmented Barrier Certificates |
| title_full | Verification of Approximate Initial-State Opacity for Control Systems via Neural Augmented Barrier Certificates |
| title_fullStr | Verification of Approximate Initial-State Opacity for Control Systems via Neural Augmented Barrier Certificates |
| title_full_unstemmed | Verification of Approximate Initial-State Opacity for Control Systems via Neural Augmented Barrier Certificates |
| title_short | Verification of Approximate Initial-State Opacity for Control Systems via Neural Augmented Barrier Certificates |
| title_sort | verification of approximate initial state opacity for control systems via neural augmented barrier certificates |
| topic | approximate initial-state opacity barrier certificate discrete-time control system deep learning mixed integer linear programming |
| url | https://www.mdpi.com/2227-7390/10/14/2388 |
| work_keys_str_mv | AT shengpuwang verificationofapproximateinitialstateopacityforcontrolsystemsvianeuralaugmentedbarriercertificates AT miding verificationofapproximateinitialstateopacityforcontrolsystemsvianeuralaugmentedbarriercertificates AT wanglin verificationofapproximateinitialstateopacityforcontrolsystemsvianeuralaugmentedbarriercertificates AT yubojia verificationofapproximateinitialstateopacityforcontrolsystemsvianeuralaugmentedbarriercertificates |