Formal Control Synthesis via Safe Reinforcement Learning Under Real-Time Specifications

In recent years, reinforcement learning techniques have gained widespread application in control synthesis. However, in the context of safety-critical systems, employing trial-and-error based reinforcement learning may be unacceptable due to the potential risks it poses during the learning process. Consequently, the development of safe reinforcement learning techniques has become imperative. This paper addresses the challenge of safe reinforcement learning for controller synthesis, particularly when safety specifications are intricately linked to the real-time behavior of the system. To articulate time-sensitive requirements, we leverage Metric Interval Temporal Logic (MITL). To ensure safety throughout the learning process, we introduce an additional reactive controller called a shield. Specifically, the shield functions to reject any behavior that violates the real-time specifications, thus mitigating potential risks. The efficacy of our proposed approach is demonstrated through simulation results, highlighting its ability to satisfy safety constraints in the dynamic environment of controller synthesis.