Formal Synthesis of Safety Controllers via $k$-Inductive Control Barrier Certificates
Tianxiang Ren, Wang Lin, Zuohua Ding · IEEE Transactions on Reliability · 2024
Control barrier certificate is an ingenious and practical approach of safety controller synthesis for cyber-physical systems. In this article, we present an approach for synthesizing safety controllers for controlled discrete-time systems subject to safety constraints. We first introduce a new type of$k$-inductive control barrier certificates ($k$-ICBCs), which relaxes the strict nonincreasing condition of general control barrier certificates. Apart from this, we propose a certificate synthesis framework that includes a learner and a verifier. They collaborate continuously to search for safety controllers and their corresponding$k$-ICBCs simultaneously. The learner obtains neural controllers and candidate$k$-ICBCs through supervised learning, while the verifier addresses a series of mixed integer linear programming problems to validate the candidate$k$-ICBCs or provide counterexamples to guide the learner further. Thanks to the less conservatism of$k$-inductive conditions, safety neural controllers, and$k$-ICBCs can be easily and quickly obtained. We showcase through benchmark examples that our method is efficient, and$k$-inductive conditions can improve the effectiveness of control barrier certificate synthesis methods by successfully verifying systems that are challenging to handle with general control barrier certificate conditions.