COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking (2022-09-15T00:00:00.000000Z)

TL;DR

COOL-MC is presented, a tool that integrates state-of-the-art reinforcement learning (RL) and model checking and algorithms to obtain bounds on the performance of so-called permissive policies.

Abstract

. This paper presents COOL-MC, a tool that integrates state-of-the-art reinforcement learning (RL) and model checking. Speciﬁcally, 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 deﬁned 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 speciﬁed 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.

Authors

Dennis Gross

1 papers

N. Jansen

1 papers

Sebastian Junges

1 papers

TL;DR

Abstract

Authors

References40 items

Specification-Guided Learning of Nash Equilibria with High Social Welfare

Verifiable strategy synthesis for multiple autonomous agents: a scalable approach

Verified Probabilistic Policies for Deep Reinforcement Learning

Scalar reward is not enough: a response to Silver, Singh, Precup and Sutton (2021)

Deep reinforcement learning in transportation research: A review

Mungojerrie: Reinforcement Learning of Linear-Time Objectives

Deep reinforcement learning for energy management in a microgrid with flexible demand

Deep Reinforcement Learning with Temporal Logics

Developing Combat Behavior through Reinforcement Learning in Wargames and Simulations

Enforcing Almost-Sure Reachability in POMDPs

Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning

The Quantitative Verification Benchmark Set

Omega-Regular Objectives in Model-Free Reinforcement Learning

Safe Reinforcement Learning via Shielding

A Storm is Coming: A Modern Probabilistic Model Checker

OpenAI Gym

Safety-Constrained Reinforcement Learning for MDPs

Uppaal Stratego

End-to-End Training of Deep Visuomotor Policies

Human-level control through deep reinforcement learning

On Time with Minimal Expected Cost!

The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification

Permissive Controller Synthesis for Probabilistic Systems

Verification of Markov Decision Processes Using Learning Algorithms

Principles of model checking

Efficient Structure Learning in Factored-State MDPs

Efficient On-the-Fly Algorithms for the Analysis of Timed Games

PRISM 2.0: a tool for probabilistic model checking

Reinforcement Learning by Stochastic Hill Climbing on Discounted Reward

Q-learning

Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning

MoGym: Using Formal Models for Training and Verifying Decision-making Agents

Safe Reinforcement Learning Using Probabilistic Shields (Invited Paper)

Teaching Stratego to Play Ball Optimal Synthesis for Continuous Space MDPs

Towards Verifiable and Safe Model-Free Reinforcement Learning

Accelerating the Machine Learning Lifecycle with MLflow

Handbook of Model Checking

A comprehensive survey on safe reinforcement learning

Simple Statistical Gradient-Following Algorithms for Connectionist Reinforcement Learning

Reinforcement Learning: An Introduction

Field of Study

Venue Information

Name

Type

URL

Alternate Names