PV4 ⊧ DryVRproduces a satisfiability/reachability result for a hybrid control systemFramework 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.
- Cyber-physical system
- Autonomous systems
- Reachability analysis
- Gray-box systems
- Hybrid control systems
- Transition graph
- Initial set
- Set of unsafe states
Format:JSON file (this used to be a text file in the earlier versions of DryVR)
Any reachtubes or counterexamples are also stored in text files.
InternalsThis 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.