Search for: All records

We present 𝖲𝖼𝖾𝗇𝖾𝖢𝗁𝖾𝖼𝗄𝖾𝗋, a tool for verifying scenarios involving vehicles executing complex plans in large cluttered workspaces. 𝖲𝖼𝖾𝗇𝖾𝖢𝗁𝖾𝖼𝗄𝖾𝗋 converts the scenario verification problem to a standard hybrid system verification problem, and solves it effectively by exploiting structural properties in the plan and the vehicle dynamics. 𝖲𝖼𝖾𝗇𝖾𝖢𝗁𝖾𝖼𝗄𝖾𝗋 uses symmetry abstractions, a novel refinement algorithm, and importantly, is built to boost the performance of any existing reachability analysis tool as a plug-in subroutine. We evaluated 𝖲𝖼𝖾𝗇𝖾𝖢𝗁𝖾𝖼𝗄𝖾𝗋 on several scenarios involving ground and aerial vehicles with nonlinear dynamics and neural network controllers, employing different kinds of symmetries, using different reachability subroutines, and following plans with hundreds of waypoints in complex workspaces. Compared to two leading tools, DryVR and Flow*, 𝖲𝖼𝖾𝗇𝖾𝖢𝗁𝖾𝖼𝗄𝖾𝗋 shows 14× average speedup in verification time, even while using those very tools as reachability subroutines.