Neural-Symbolic System Control Adjustment Based on Runtime Verification
摘要
Neural-Symbolic Systems (NSSs) have been widely deployed in safety-critical domains. However, due to the inherent uncertainty and opaqueness of DNNs, there is an increasing demand for security assurance. In this work, we propose an adjustment framework based on runtime verification (RV, for short) to ensure NSS compliance with given signal temporal logic (STL) properties. To identify unsafe control signal in time, we utilize Runge-Kutta method to predict the system trajectory under scrutiny at discrete time-steps. Our framework also supports the switching of control signals upon violation of safety properties. This capability is achieved through the deployment of predictive strategies, including the construction of a state tree and forward-search algorithms, enabling the system to dynamically select and switch to alternative control signals in real time. We conduct an evaluation on publicly available control systems. The evaluation results show that our method successfully repairs critical safety issues, and significantly improves the reliability of NSSs.