Formal Synthesis of Safety Controllers via $k$-Inductive Control Barrier Certificates

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.