Safeguarding Learning-based Control for Smart Energy Systems with Sampling Specifications

TL;DR

This paper presents a method to enhance safety in reinforcement learning for energy systems by translating real-time safety requirements into linear temporal logic, enabling formal verification and safety guarantees.

Contribution

It introduces a discretization approach that strengthens safety specifications in real-time logic, facilitating formal verification and shield synthesis for safe reinforcement learning.

Findings

Discretization of real-time safety requirements into LTL enables formal verification.

Probabilistic guarantees from LTL model checking serve as lower bounds for safety.

Method improves safety assurance in energy system control using reinforcement learning.

Abstract

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.