PV4 ⊧ DryVRproduces a satisfiability/reachability result for a hybrid control system

Framework for verifying hybrid control systems that are described by a combination of a black-box simulator for trajectories and a white-box transition graph specifying mode switches.

Application domain/field

• Cyber-physical system
• Autonomous systems
• Reachability analysis
• Gray-box systems
• Hybrid control systems

Expected input

• Transition graph
• Initial set
• Set of unsafe states

Format:

JSON file (this used to be a text file in the earlier versions of DryVR)

Expected output

Safe or Unsafe? Any reachtubes or counterexamples are also stored in text files.

Internals

This framework includes:

• A probabilistic algorithm for learning sensitivity of the continuous trajectories from simulation data
• Bounded reachability analysis that uses the learned sensitivity
• Reasoning techniques for verification of complex systems under long switching sequences, from the reachability analysis of a simpler system under short sequences.

Comments

License: MIT