DAE-Embedded Neural Control Verification for Shipboard Microgrids under Transient Shocks
For shipboard microgrid operators, this method addresses the safety verification problem of black-box neural controllers during transient shocks, though it is domain-specific and incremental.
This paper proposes a formal verification method for neural controllers in shipboard microgrids to assess shock responses, using a DAE-embedded bound propagation approach to compute tight envelopes of neural control outputs. Case studies demonstrate effectiveness in certifying control performance under uncertain disturbances.
Neural control offers strong potential for handling highly nonlinear dynamics in shipboard microgrids (SMGs), yet its black-box nature can trigger abrupt control spikes and actuator saturation during initial transient shocks. This letter devises a formal verification method for SMG neural controller to assess its shock responses. Our contributions include: 1) a set-based SMG differential-algebraic equation(DAE) model compatible with set propagation; 2) a DAE-embedded bound propagation approach to compute tight envelopes of all possible neural control output. Extensive case studies demonstrate the effectiveness of the devised method in formally certifying SMG control performance under uncertain disturbances.