Formal Synthesis of Barrier Certificates Using Fourier Kolmogorov-Arnold Network

Abstract

Barrier certificate generation is an efficient and powerful technique for formally verifying safety properties of cyber-physical systems. Feed-forward neural networks (FNNs) are commonly used to synthesize barrier certificates, but the fixed activation functions limit their efficiency and scalability. In this paper, we propose a novel method for generating barrier certificates using Fourier Kolmogorov-Arnold Networks (KANs). Specifically, it utilizes Fourier KANs to replace FNNs as the template of barrier certificates. Since Fourier KAN has learnable activation functions and uses trigonometric functions as its basis functions, it can efficiently improve the representation power and is easy to train for neural barrier certificates. Then, it formally verifies the validity of the candidate Fourier KAN barrier certificates using both the Lipschitz method and the Satisfiability Modulo Theories, improving the efficiency and success rate of verification. We implement the tool KAN4BC, and evaluate its performance over a set of benchmarks. The experimental results demonstrate the effectiveness and efficiency of our method.