PV2 ⊧ SceneCheckertransforms scenarios for hybrid control systems to reachability problems, requires an external solver

Tool for verifying scenarios involving vehicles executing complex plans in large cluttered workspaces.

Application domain/field

• Hybrid systems
• Safety verification
• Reachability verification
• Cyber-physical systems
• Scenario verification

Expected input

• Scenario file, this describes e.g. fixed obstacles, a plan, and an agent that is supposed to execute the plan without running into the obstacles.
• Dynamics file

Format:

• Scenario description: JSON file
• Dynamics file: ?

Expected output

safe in case the reachset of automaton H does not intersect with the unsafe set. unknown otherwise. It also gives some performance metrics and it can visualize various computed reachsets.

Internals

Scenario verification: check that a vehicle or an agent can safely execute a plan through a complex environment Tool for verifying scenarios involving vehicles executing complex plans in large cluttered workspaces. It converts the scenario verification problem to a standard hybrid system verification problem, and solves it by exploiting structural properties in the plan and vehicle dynamics. It uses reachability tools for verification. Uses Flow*, DryVR for reachability analysis.