ICMS 2020 Session

Artificial Intelligence and Mathematical Software

Accepted Talk

Naijun Zhan (Chinese Academy of Sciences, Beijing)
Practical Verification of Intelligent Cyber-Physical Systems
Abstract: In this talk, we present a method based on linear programming that facilitates reliable safety verification of dynamical and hybrid systems subject to perturbation inputs over the infinite time horizon. The verification algorithm applies the probably approximately correct (PAC) learning framework and consequently can be regarded as statistically formal verification in the sense that it provides formal safety guarantees expressed using error probabilities and confidences. The safety of hybrid systems in this framework is verified via the computation of so-called PAC barrier certificates, which can be computed by solving a linear programming problem. Based on scenario approaches, the linear program is constructed by a family of independent and identically distributed state samples. In this way we can verify large-scale dynamical and hybrid systems that existing methods are not capable of dealing with. Some preliminary experiments demonstrate the performance of our approach. In addition, we also discuss how to extend this approach to the verificaiton of intelligent systems, also known as black-box systems.