COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking
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.
Code (2)
Tasks
OpenAI Gymreinforcement-learningReinforcement Learning (RL)Similar Papers 제목 키워드 기반
COOL-MC: Verifying and Explaining RL Policies for Multi-bridge Network Maintenance
Aging bridge networks require proactive, verifiable, and interpretable maintenance strategies, yet reinforcement learning (RL) policies trained solely on reward signals provide no formal safety guarantees and remain opaq…
Reinforcement LearningCOOL-MC: Verifying and Explaining RL Policies for Platelet Inventory Management
Platelets expire within five days. Blood banks face uncertain daily demand and must balance ordering decisions between costly wastage from overstocking and life-threatening shortages from understocking. Reinforcement lea…
Reinforcement LearningBuildingGym: An open-source toolbox for AI-based building energy management using reinforcement learning
Reinforcement learning (RL) has proven effective for AI-based building energy management. However, there is a lack of flexible framework to implement RL across various control problems in building energy management. To a…
Reinforcement LearningFormally Verifying and Explaining Sepsis Treatment Policies with COOL-MC
Safe and interpretable sequential decision-making is critical in healthcare, yet reinforcement learning (RL) policies for sepsis treatment optimization remain opaque and difficult to verify. Standard probabilistic model …
Reinforcement LearningSemi-analytical Industrial Cooling System Model for Reinforcement Learning
We present a hybrid industrial cooling system model that embeds analytical solutions within a multi-physics simulation. This model is designed for reinforcement learning (RL) applications and balances simplicity with sim…
reinforcement-learningReinforcement LearningReinforcement Learning (RL)