PV3 ⊧ Mungojerriegenerates a reward scheme from an ω-regular objective and checks it on finite models

Tool for testing reinforcement learning reward schemes for $\omega$-regular objectives

Application domain/field

• Reinforcement learning
• $\omega$-regular objectives
• Linear Temporal Logic (LTL)
• Branching Markov Decision Processes (BMDPs)
• Reward functions

Expected input

• Model (Branching Markov Decision Processes (BMDPs))
• Properties ($\omega$-automata)

Format:

• Model: finite state and action models in PRISM language
• Properties: $\omega$-automata in HOA