A Learner-Refiner Framework for Barrier Certificate Generation

Deng Chen, Wang Lin () and Zuohua Ding
Additional contact information
Deng Chen: School of Computer Science and Technology, Zhejiang Sci-Tech University, Hangzhou 310018, China
Wang Lin: School of Computer Science and Technology, Zhejiang Sci-Tech University, Hangzhou 310018, China
Zuohua Ding: School of Computer Science and Technology, Zhejiang Sci-Tech University, Hangzhou 310018, China

Mathematics, 2025, vol. 13, issue 5, 1-13

Abstract: Barrier certificate is a powerful tool for verifying they safety property of dynamical systems. In this paper, we introduce an innovative learner–refiner framework for synthesizing polynomial barrier certificates. The framework comprises a learner and a refiner , which work inductively to generate barrier certificates. More specifically, the learner trains barrier certificate candidates represented by feedforward neural networks with polynomial activations, while the refiner utilizes sums of squares (SOS) programming to either validate the candidates or recover valid barrier certificates. Our framework achieves great efficiency via supervised learning, and it ensures formal soundness using SOS-based verification. We implement the LR4BC tool, and we perform a comprehensive experimental evaluation using several benchmarks. The results demonstrate that our tool not only successfully synthesizes polynomial barrier certificates undetected via the SOS-based tool PRoTECT but also achieves a significant speedup in efficiency compared to the neural network-based tool FOSSIL 2.0.

Keywords: formal verification; barrier certificate; neural network learning; sums of squares programming (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2025
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
https://www.mdpi.com/2227-7390/13/5/848/pdf (application/pdf)
https://www.mdpi.com/2227-7390/13/5/848/ (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:13:y:2025:i:5:p:848-:d:1605019

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 ().