Provably Correct Controller Synthesis of Switched Stochastic Systems with Metric Temporal Logic Specifications: A Case Study on Power Systems

TL;DR

This paper introduces a method for synthesizing controllers for switched stochastic systems that guarantees probabilistic correctness with respect to metric temporal logic specifications, demonstrated on power system case studies.

Contribution

It develops a stochastic control bisimulation function and an optimization-based control synthesis method with probabilistic guarantees for systems with stochastic uncertainties.

Findings

Successfully applied to power systems with generation loss disturbances.

Achieved probabilistic guarantees for system specifications.

Validated robustness against initial state variations.

Abstract

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.