SceneChecker: Boosting Scenario Verification Using Symmetry Abstractions

Hussein Sibai, Yangge Li, Sayan Mitra

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 33rd International Conference, CAV 2021, Proceedings
EditorsAlexandra Silva, K. Rustan Leino
PublisherSpringer
Pages580-594
Number of pages15
ISBN (Print)9783030816841
DOIs
StatePublished - 2021
Event33rd International Conference on Computer Aided Verification, CAV 2021 - Virtual, Online
Duration: Jul 20 2021Jul 23 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12759 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference33rd International Conference on Computer Aided Verification, CAV 2021
CityVirtual, Online
Period7/20/217/23/21

Keywords

  • Hybrid systems
  • Safety verification
  • Symmetry

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'SceneChecker: Boosting Scenario Verification Using Symmetry Abstractions'. Together they form a unique fingerprint.

Cite this