SceneChecker is a software library for verifying scenarios involving vehicles executing complex plans in large cluttered workspaces. SceneChecker converts the scenario description into to a hybrid automaton, and attempts verification by exploiting the symmetries in the underlying dynamics. It can use any existing reachability analysis tool as a subroutine although this implementation has been tested with DryVR and Flow*. The details of the theory are available in the publications listed below. In experiments, SceneChecker shows up to 20x speedup in verification time (over using DryVR and Flow* directly).
SceneChecker is developed using Python. SceneChecker can be downloaded from here. SceneChecker can use existing reachability tools as subroutione. Currently supported tools are DryVR and Flow*. However, SceneChecker can also be extended to handle other reachability tools.
SceneChecker has been tested on various benchmark examples with both DryVR and Flow* as reachability subroutine and the results are formulated below.
Sibai H., Li Y., Mitra S. (2021) : Boosting Scenario Verification Using Symmetry Abstractions. In: Silva A., Leino K.R.M. (eds) Computer Aided Verification. CAV 2021. Lecture Notes in Computer Science, vol 12759. Springer, Cham. https://doi.org/10.1007/978-3-030-81685-8_28. [bibtex], [doi]