Verification of Approximate Initial-State Opacity for Control Systems via Neural Augmented Barrier Certificates

Shengpu Wang, Mi Ding, Wang Lin and Yubo Jia
Additional contact information
Shengpu Wang: School of Information Science and Technology, Zhejiang Sci-Tech University, Hangzhou 310018, China
Mi Ding: School of Information Science and Technology, Zhejiang Sci-Tech University, Hangzhou 310018, China
Wang Lin: School of Information Science and Technology, Zhejiang Sci-Tech University, Hangzhou 310018, China
Yubo Jia: School of Information Science and Technology, Zhejiang Sci-Tech University, Hangzhou 310018, China

Mathematics, 2022, vol. 10, issue 14, 1-19

Abstract: 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 learner and a verifier interact to synthesize augmented barrier certificates in the form of neural networks. The learner trains neural certificates via the deep learning method, and the verifier 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 learner. The experimental results demonstrate that our approach is more scalable and effective than the existing sum of squares programming method.

Keywords: approximate initial-state opacity; barrier certificate; discrete-time control system; deep learning; mixed integer linear programming (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2022
References: View references in EconPapers View complete reference list from CitEc
Citations:

Downloads: (external link)
https://www.mdpi.com/2227-7390/10/14/2388/pdf (application/pdf)
https://www.mdpi.com/2227-7390/10/14/2388/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:10:y:2022:i:14:p:2388-:d:857620

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().