Safeguarding Learning-based Control for Smart Energy Systems with Sampling Specifications
This work addresses safety-critical control in smart energy systems, offering an incremental improvement by adapting existing formal methods to enhance reinforcement learning safety.
The paper tackles the challenge of ensuring safety in reinforcement learning for energy systems by converting real-time temporal logic safety requirements into linear temporal logic, enabling the use of shields and formal verification to provide probabilistic guarantees.
We study challenges using reinforcement learning in controlling energy systems, where apart from performance requirements, one has additional safety requirements such as avoiding blackouts. We detail how these safety requirements in real-time temporal logic can be strengthened via discretization into linear temporal logic (LTL), such that the satisfaction of the LTL formulae implies the satisfaction of the original safety requirements. The discretization enables advanced engineering methods such as synthesizing shields for safe reinforcement learning as well as formal verification, where for statistical model checking, the probabilistic guarantee acquired by LTL model checking forms a lower bound for the satisfaction of the original real-time safety requirements.