Overview
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).
Software
Virtual machine for CAV 2021 repeatability package can be found in Google drive or Figshare.
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.
Experiments
SceneChecker has been tested on various benchmark examples with both DryVR and Flow* as reachability subroutine and the results are formulated below.
| SceneChecker+DR | SceneChecker+F* | ||||||||
|---|---|---|---|---|---|---|---|---|---|
| sc. | |S| | Nrefs | Rc | Rt | Tt | Nrefs | Rc | Rt | Tt |
| C-S1 | 6 | 1 | 4 | 0.14 | 0.15 | 1 | 4 | 0.51 | 0.52 |
| C-S2 | 140 | 0 | 1 | 0.04 | 0.65 | 0 | 1 | 0.18 | 0.79 |
| C-S3 | 458 | 0 | 1 | 0.04 | 4.24 | 0 | 1 | 0.11 | 4.34 |
| C-S4.a | 520 | 2 | 7 | 0.26 | 4.37 | 2 | 7 | 0.8 | 4.96 |
| C-S4.b | 520 | 10 | 39 | 1.43 | 8.69 | 10 | 39 | 2.83 | 31.73 |
| Q-S1 | 6 | 1 | 4 | 0.04 | 0.05 | 1 | 4 | 13.85 | 14.13 |
| Q-S2 | 140 | 0 | 1 | 0.04 | 0.88 | 0 | 1 | 3.38 | 12.62 |
| Q-S3 | 458 | 0 | 1 | 0.06 | 5.9 | 0 | 1 | 4.98 | 62.66 |
| Q-S4.a | 520 | 0 | 1 | 0.06 | 3.17 | 0 | 1 | 4.8 | 34.89 |
| Q-S5 | 280 | 0 | 36 | 0.85 | 3.04 | NA | NA | NA | TO |
People Involved
- Hussein Sibai
- Yangge Li
- Sayan Mitra
Publications
Sibai H., Li Y., Mitra S. (2021) SceneChecker: 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]