TY - GEN
T1 - SceneChecker
T2 - 33rd International Conference on Computer Aided Verification, CAV 2021
AU - Sibai, Hussein
AU - Li, Yangge
AU - Mitra, Sayan
N1 - Funding Information:
The authors are supported by a research grant from The Boeing Company and a research grant from NSF (FMITF: 1918531). We would like to thank John L. Olson, Aaron A. Mayne, and Michael R. Abraham from The Boeing Company for valuable technical discussions.
Publisher Copyright:
© 2021, The Author(s).
PY - 2021
Y1 - 2021
N2 - We present SceneChecker, a tool for verifying scenarios involving vehicles executing complex plans in large cluttered workspaces. SceneChecker 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. SceneChecker 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 SceneChecker 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*, SceneChecker shows 14 × average speedup in verification time, even while using those very tools as reachability subroutines.
AB - We present SceneChecker, a tool for verifying scenarios involving vehicles executing complex plans in large cluttered workspaces. SceneChecker 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. SceneChecker 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 SceneChecker 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*, SceneChecker shows 14 × average speedup in verification time, even while using those very tools as reachability subroutines.
KW - Hybrid systems
KW - Safety verification
KW - Symmetry
UR - http://www.scopus.com/inward/record.url?scp=85113525838&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85113525838&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-81685-8_28
DO - 10.1007/978-3-030-81685-8_28
M3 - Conference contribution
AN - SCOPUS:85113525838
SN - 9783030816841
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 580
EP - 594
BT - Computer Aided Verification - 33rd International Conference, CAV 2021, Proceedings
A2 - Silva, Alexandra
A2 - Leino, K. Rustan
PB - Springer
Y2 - 20 July 2021 through 23 July 2021
ER -