DAE-Embedded Neural Control Verification for Shipboard Microgrids under Transient Shocks

TL;DR

This paper introduces a formal verification method for neural controllers in shipboard microgrids, ensuring safety and performance during transient shocks by modeling and bounding control outputs.

Contribution

It develops a set-based DAE model and a DAE-embedded bound propagation approach for verifying neural control responses under disturbances.

Findings

Effectively certifies SMG control performance under shocks.

Provides tight bounds on neural control outputs during transients.

Demonstrates robustness of the verification method through case studies.

Abstract

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.