# Dependability Analysis of Deep Reinforcement Learning based Robotics and Autonomous Systems through Probabilistic Model Checking

arXiv: https://arxiv.org/abs/2109.06523 · HTML: https://mlsanity.com/paper/2109.06523/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 25 of its 52 references that are in the map.
- First posted on arXiv 14 Sep 2021.

## Builds on (most cited first, 25 of 25)

- [Continuous control with deep reinforcement learning](https://mlsanity.com/paper/1509.02971/) (2015)
- [Playing Atari with Deep Reinforcement Learning](https://mlsanity.com/paper/1312.5602/) (2013)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Safe Reinforcement Learning via Shielding](https://mlsanity.com/paper/1708.08611/) (2017)
- [Sim-to-Real Transfer in Deep Reinforcement Learning for Robotics: a Survey](https://mlsanity.com/paper/2009.13303/) (2020)
- [Safe Model-based Reinforcement Learning with Stability Guarantees](https://mlsanity.com/paper/1705.08551/) (2017)
- [End-to-End Safe Reinforcement Learning through Barrier Functions for Safety-Critical Continuous Control Tasks](https://mlsanity.com/paper/1903.08792/) (2019)
- [Google Research Football: A Novel Reinforcement Learning Environment](https://mlsanity.com/paper/1907.11180/) (2019)
- [Robust Deep Reinforcement Learning against Adversarial Perturbations on State Observations](https://mlsanity.com/paper/2003.08938/) (2020)
- [Deep Reinforcement Learning framework for Autonomous Driving](https://mlsanity.com/paper/1704.02532/) (2017)
- [Verifiable Reinforcement Learning via Policy Extraction](https://mlsanity.com/paper/1805.08328/) (2018)
- [Action Robust Reinforcement Learning and Applications in Continuous Control](https://mlsanity.com/paper/1901.09184/) (2019)
- [Emergent Complexity via Multi-Agent Competition](https://mlsanity.com/paper/1710.03748/) (2017)
- [Reachability Analysis of Deep Neural Networks with Provable Guarantees](https://mlsanity.com/paper/1805.02242/) (2018)
- [Deep Reinforcement Learning for Industrial Insertion Tasks with Visual Inputs and Natural Rewards](https://mlsanity.com/paper/1906.05841/) (2019)
- [Transfer from Simulation to Real World through Learning Deep Inverse Dynamics Model](https://mlsanity.com/paper/1610.03518/) (2016)
- [An Inductive Synthesis Framework for Verifiable Reinforcement Learning](https://mlsanity.com/paper/1907.07273/) (2019)
- [A storm is Coming: A Modern Probabilistic Model Checker](https://mlsanity.com/paper/1702.04311/) (2017)
- [Safe reinforcement learning for probabilistic reachability and safety specifications: A Lyapunov-based approach](https://mlsanity.com/paper/2002.10126/) (2020)
- [Probabilistic Model Checking of Robots Deployed in Extreme Environments](https://mlsanity.com/paper/1812.04128/) (2018)
- [Adversarial Reinforcement Learning Framework for Benchmarking Collision Avoidance Mechanisms in Autonomous Vehicles](https://mlsanity.com/paper/1806.01368/) (2018)
- [Scalable Synthesis of Verified Controllers in Deep Reinforcement Learning](https://mlsanity.com/paper/2104.10219/) (2021)
- [Efficient Parametric Model Checking Using Domain Knowledge](https://mlsanity.com/paper/1812.09952/) (2018)
- [Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management](https://mlsanity.com/paper/1909.03019/) (2019)
- [Towards Identifying and closing Gaps in Assurance of autonomous Road vehicleS -- a collection of Technical Notes Part 2](https://mlsanity.com/paper/2003.00790/) (2020)

## Built on by (most cited first, 3 of 3)

- [Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training](https://mlsanity.com/paper/2211.11127/) (2022)
- [COOL-MC: Verifying and Explaining RL Policies for Platelet Inventory Management](https://mlsanity.com/paper/2603.02396/) (2026)
- [COOL-MC: Verifying and Explaining RL Policies for Multi-bridge Network Maintenance](https://mlsanity.com/paper/2603.07546/) (2026)

## Abstract (arXiv)

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.