Workflows

We provide a set of example workflows on how verigym may be used.

• VeriGym - Comparing abstraction policies: Learns an abstract MDP of CartPole, computes a policy for it with stormpy, and evaluates that policy on the abstract and the original environment.

• Workflow: Abstraction Refinement: Learns finer and finer abstractions of CartPole until the policy computed by the model checker performs well enough on the original environment.

• Workflow: Benchmark your Reinforcement Learning policy against a model checked optimal policy: Trains a DQN agent on a PRISM model and compares it with the optimal policy computed by model checking.

• VeriGym - Comparing exploration policies: Compares the exploration policies built into VeriGym for model learning on MountainCar, and shows how to write your own.

• Workflow: External Tools (Julia): Exports a learned abstraction, solves it with a Julia solver (MCTS.jl), and evaluates the resulting policy in VeriGym.

• Workflow: Feature Selection: Removes state features from the MuJoCo Ant environment and compares RL training on the full and the reduced observations.

• Workflow: Implementing a simple shield for a gymnasium environment: Builds a safety shield for CartPole from model checking results and compares PPO agents trained with and without it.