SceneChecker: Boosting Scenario Verification using Symmetry Abstractions

TL;DR

SceneChecker is a verification tool that leverages symmetry abstractions and a novel refinement algorithm to significantly accelerate the verification of vehicle scenarios in complex environments, compatible with existing reachability tools.

Contribution

It introduces symmetry abstractions and a refinement algorithm to enhance the performance of scenario verification in hybrid systems, compatible with any reachability analysis tool.

Findings

SceneChecker achieves 20x faster verification times compared to leading tools.

It effectively verifies complex vehicle scenarios with nonlinear dynamics and neural network controllers.

The tool is versatile across different vehicle types, symmetries, and workspace complexities.

Abstract

We presentSceneChecker, 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 way-points in complex workspaces. Compared to two leading tools, DryVR and Flow*, SceneChecker shows 20x speedup in verification time, even while using those very tools as reachability subroutines.