Deep reinforcement learning (DRL) has emerged as a powerful paradigm for solving complex decision-making problems. However, DRL-based systems still face significant dependability challenges particularly in real-time environments due to the simulation-to-reality gap, out-of-distribution observations, and the critical impact of latency. Latency-induced faults, in particular, can lead to unsafe or unstable behaviour, yet existing fault-tolerance approaches to DRL systems lack formal methods to rigorously analyse and optimise performance and safety simultaneously in real-time settings. To address this, we propose a formal framework for designing and analysing real-time switching mechanisms between DRL agents and alternative controllers. Our approach leverages Timed Automata (TAs) for explicit switch logic design, which is then syntactically converted to a Markov Decision Process (MDP) for formal analysis. We develop a novel convex query technique for multi-objective model checking, enabling the optimisation of soft performance objectives while ensuring hard safety constraints for MDPs. Furthermore, we present MOPMC, a GPU-accelerated software tool implementing this technique, demonstrating superior scalability in both model size and objective numbers.

翻译：深度强化学习已成为解决复杂决策问题的强大范式。然而，基于深度强化学习的系统仍面临严峻的可信赖性挑战，尤其是在实时环境中，这源于仿真与现实的差距、分布外观测以及延迟的关键影响。特别是延迟引发的故障可能导致不安全或不稳定的行为，但现有面向深度强化学习系统的容错方法缺乏在实时环境下同时严格分析和优化性能与安全性的形式化方法。为此，我们提出一个用于设计和分析深度强化学习代理与替代控制器之间实时切换机制的形式化框架。该方法利用时间自动机进行显式切换逻辑设计，随后通过语法转换将其转化为马尔可夫决策过程以进行形式化分析。我们开发了一种新颖的凸查询技术，用于多目标模型检测，能够在确保马尔可夫决策过程硬性安全约束的同时优化软性性能目标。此外，我们提出了MOPMC——一个实现该技术的GPU加速软件工具，在模型规模和目标数量方面均展现出卓越的可扩展性。