  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.
