COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking
This provides a tool for researchers and practitioners in AI and formal methods to enhance the reliability and analysis of RL systems, though it is incremental as it builds on existing frameworks.
The paper tackles the problem of integrating reinforcement learning and model checking by presenting COOL-MC, a tool that combines OpenAI Gym and Storm to train and verify RL policies, demonstrating its features on benchmark environments.
This paper presents COOL-MC, a tool that integrates state-of-the-art reinforcement learning (RL) and model checking. Specifically, the tool builds upon the OpenAI gym and the probabilistic model checker Storm. COOL-MC provides the following features: (1) a simulator to train RL policies in the OpenAI gym for Markov decision processes (MDPs) that are defined as input for Storm, (2) a new model builder for Storm, which uses callback functions to verify (neural network) RL policies, (3) formal abstractions that relate models and policies specified in OpenAI gym or Storm, and (4) algorithms to obtain bounds on the performance of so-called permissive policies. We describe the components and architecture of COOL-MC and demonstrate its features on multiple benchmark environments.