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

arXiv: https://arxiv.org/abs/2103.14264 · HTML: https://mlsanity.com/paper/2103.14264/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 7 of its 23 references that are in the map.
- First posted on arXiv 26 Mar 2021.

## Builds on (most cited first, 7 of 7)

- [Transfer of Temporal Logic Formulas in Reinforcement Learning](https://mlsanity.com/paper/1909.04256/) (2019)
- [On-Line Monitoring for Temporal Logic Robustness](https://mlsanity.com/paper/1408.0045/) (2014)
- [An MILP Approach for Real-time Optimal Controller Synthesis with Metric Temporal Logic Specifications](https://mlsanity.com/paper/1603.02650/) (2016)
- [Temporal Logic Control for Stochastic Linear Systems using Abstraction Refinement of Probabilistic Games](https://mlsanity.com/paper/1410.5387/) (2014)
- [Computational methods for stochastic control with metric interval temporal logic specifications](https://mlsanity.com/paper/1503.07193/) (2015)
- [Control Strategies for COVID-19 Epidemic with Vaccination, Shield Immunity and Quarantine: A Metric Temporal Logic Approach](https://mlsanity.com/paper/2007.15114/) (2020)
- [Hybrid Controller for Wind Turbine Generators to Ensure Adequate Frequency Response in Power Networks](https://mlsanity.com/paper/1802.03429/) (2018)

## Abstract (arXiv)

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.