While Deep Reinforcement Learning (DRL) provides transformational capabilities to the control of Robotics and Autonomous Systems (RAS), the black-box nature of DRL and uncertain deployment environments of RAS pose new challenges on its dependability. Although existing works impose constraints on the DRL policy to ensure successful completion of the mission, it is far from adequate to assess the DRL-driven RAS in a holistic way considering all dependability properties. In this paper, we formally define a set of dependability properties in temporal logic and construct a Discrete-Time Markov Chain (DTMC) to model the dynamics of risk/failures of a DRL-driven RAS interacting with the stochastic environment. We then conduct Probabilistic Model Checking (PMC) on the designed DTMC to verify those properties. Our experimental results show that the proposed method is effective as a holistic assessment framework while uncovering conflicts between the properties that may need trade-offs in training. Moreover, we find that the standard DRL training cannot improve dependability properties, thus requiring bespoke optimisation objectives. Finally, our method offers sensitivity analysis of dependability properties to disturbance levels from environments, providing insights for the assurance of real RAS.

翻译：虽然深强化学习(DRL)为控制机器人和自主系统提供了转化能力,但DRL的黑箱性质和RAS的不确定部署环境对其可靠性提出了新的挑战。虽然现有工程对DRL政策造成限制,以确保成功完成任务,但还远远不足以从整体角度评估DRL驱动的RAS, 同时考虑到所有可靠性特性。在本文件中,我们正式界定了一套时间逻辑上的可靠特性,并建造了一套分立时间马可夫链(DDMC),以模拟DRL驱动的RAS与随机环境发生互动的风险/失败动态。我们随后对设计DTMC核查这些属性的概率模型(PMC)进行测试。我们的实验结果显示,拟议方法作为整体评估框架是有效的,同时发现在培训中可能需要权衡的属性之间的冲突。此外,标准DRL培训无法改善可靠性,因此需要说明对RASS的真实性目标作出选择。最后,我们的方法提供了对设计DTMC的敏感性分析,提供了从真实的稳定性环境提供敏感性分析。