PV4 ⊧ MoGymverifies reach-avoid objective for trained decision-making agent

Application domain/field

• Statistical model checking
• Decision-making agents
• Reinforcement learning

Type of tool

Framework?

Expected input

• Formal representation of a decision-making problem
• Reach-avoid objective

Format:

JANI

Expected output

Trained decision-making agent. The trained agent can be verified w.r.t. reach-avoid objectives.

Internals

Uses a variant of modes for statistical model checking. This variant has been extended with new resolution strategies for non-determinism. Based on Momba