PV3 ⊧ Trainifychecks properties of a deep reinforcement learning systems

Application domain/field

• Deep reinforcement learning
• Counterexample-guided abstraction refinement (CEGAR)
• Model checking

Type of tool

Framework for training & verification of deep reinforcement learning systems

Expected input

• Deep neural network
• Properties in ACTL (segment of CTL where only universal path quantifiers are allowed and negation can only be used on atomic propositions)

Format:

? (seems to all be hardcoded in Python)

Expected output

Whether the property holds or not.

Internals

The tool builds a finite abstract state space using the trained neural network.