Probabilistic Model Checking Of Stochastic Reinforcement Learning Policies

Abstract

We introduce a method to verify stochastic reinforcement learning (RL) policies. This approach is compatible with any RL algorithm as long as the algorithm and its corresponding environment collectively adhere to the Markov property. In this setting, the future state of the environment should depend solely on its current state and the action executed, independent of any previous states or actions. Our method integrates a verification technique, referred to as model checking, with RL, leveraging a Markov decision process, a trained RL policy, and a probabilistic computation tree logic (PCTL) formula to build a formal model that can be subsequently verified via the model checker Storm. We demonstrate our method's applicability across multiple benchmarks, comparing it to baseline methods called deterministic safety estimates and naive monolithic model checking. Our results show that our method is suited to verify stochastic RL policies.

Stats

• citations0
• S2 citations—
• github stars0
• HF likes0
• heat score0.00
• arxiv keygross2024probabilistic

Related papers

• An Abstraction-based Method To Check Multi-agent Deep Reinforcement-learning Behaviors (2021)2.26
• Targeted Adversarial Attacks On Deep Reinforcement Learning Policies Via Model Checking (2022)2.26
• Algorithmic Framework For Model-based Deep Reinforcement Learning With Theoretical Guarantees (2018)0.00
• Runtime Verification Of Learning Properties For Reinforcement Learning Algorithms (2023)3.58
• Concurrent Learning Of Policy And Unknown Safety Constraints In Reinforcement Learning (2024)0.00
• On Learning History Based Policies For Controlling Markov Decision Processes (2022)0.00
• PC-MLP: Model-based Reinforcement Learning With Policy Cover Guided Exploration (2021)0.00
• Learning Probabilistic Temporal Logic Specifications For Stochastic Systems (2025)0.00