Provably Correct Controller Synthesis of Switched Stochastic Systems with Metric Temporal Logic Specifications: A Case Study on Power Systems
This work addresses the challenge of ensuring reliable control in power grids under stochastic disturbances, representing an incremental advance in applying formal methods to stochastic systems.
The paper tackles the problem of synthesizing controllers for switched stochastic systems with metric temporal logic specifications, achieving provably correct control with probabilistic guarantees. It demonstrates the approach on power systems, handling disturbances like generation loss while meeting grid frequency, rotor speed, and power flow constraints.
In this paper, we present a provably correct controller synthesis approach for switched stochastic control systems with metric temporal logic (MTL) specifications with provable probabilistic guarantees. We first present the stochastic control bisimulation function for switched stochastic control systems, which bounds the trajectory divergence between the switched stochastic control system and its nominal deterministic control system in a probabilistic fashion. We then develop a method to compute optimal control inputs by solving an optimization problem for the nominal trajectory of the deterministic control system with robustness against initial state variations and stochastic uncertainties. We implement our robust stochastic controller synthesis approach on both a four-bus power system and a nine-bus power system under generation loss disturbances, with MTL specifications expressing requirements for the grid frequency deviations, wind turbine generator rotor speed variations and the power flow constraints at different power lines.