{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/114011"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/114011","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Software tools for scenario verification of autonomous systems exploiting dynamical symmetries","abstract":"Submission published under a 24 month embargo labeled 'U of I Access', the embargo will last until 2023-12-01","abstract_html":"Submission published under a 24 month embargo labeled 'U of I Access', the embargo will last until 2023-12-01","abstract_has_math":false,"creators":["Li, Yangge"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Electrical & Computer Engr","degree_department":null,"school":null,"contributors":["Mitra, Sayan"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2022,"date_issued":"2022-04-29T21:46:19Z","date_published":"2022-04-29T21:46:19Z","updated_at":"2026-07-22T22:24:54Z","subjects":["Engineering"],"languages":["en","eng"],"rights":["Copyright 2021 Yangge Li"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/114011","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Mitra, Sayan"]},{"key":"dc:creator","label":"Author","values":["Li, Yangge"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2022-04-29T21:46:19Z","2024-04-29T21:47:53Z","2021-12","2021-12-06"]},{"key":"dc:type","label":"Dc Type","values":["text","Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Electrical & Computer Engr"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Engineering"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en","eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2021 Yangge Li"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/114011"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Submission published under a 24 month embargo labeled 'U of I Access', the embargo will last until 2023-12-01","The student, Yangge Li, accepted the attached license on 2021-12-06 at 15:39.","The student, Yangge Li, submitted this Thesis for approval on 2021-12-06 at 16:08.","This Thesis was approved for publication on 2021-12-06 at 16:30.","DSpace SAF Submission Ingestion Package generated from Vireo submission #17393 on 2022-04-06 at 17:17:56","Made available in DSpace on 2022-04-29T21:46:19Z (GMT). No. of bitstreams: 2 LI-THESIS-2021.pdf: 3056683 bytes, checksum: 7f2c59f98c06ea3e190abbaa6179b13a (MD5) LICENSE.txt: 4206 bytes, checksum: d2456dff4f67d41461426012486e2156 (MD5) Previous issue date: 2021-12-06","Embargo set by: Seth Robbins for item 123375 Lift date: 2024-04-29T21:46:25Z Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD system","Embargo set by: Seth Robbins for item 123375 Lift date: 2024-04-29T21:47:53Z Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD system","Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD system","U of I Only","In this thesis, we discuss using formal verification techniques to ensure the safety of autonomous systems. We present a particular type of verification problem called scenario verification, which involves vehicles executing complex plans in large cluttered workspaces. To solve the scenario verification problem, we present the tool SceneChecker. 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 implements symmetry abstractions, a novel refinement algorithm, and is built to enhance the performance of existing reachability analysis tools as a plug-in subroutine. We evaluated SceneChecker on several complicated scenarios with different types of agents. Compared to two leading tools, DryVR and Flow*, SceneChecker shows 20x speedup in verification time, even while using those tools as reachability subroutines. We further look into a variation of the scenario verification problem, with multiple agents running independently in the shared workspace. In addition, the plan is generated as the agent executing the scenario, which requires safety checking to be performed during runtime. To solve this problem, we present Swerve, an open-source cloud computing toolkit for efficient runtime collision checking for multi-agent autonomous systems. Swerve implements a remote server to check safety for different agents by using boundedtime reachability analysis. In addition, Swerve implements a cache to store already computed reachable sets and reuses them to avoid repeated computations. We evaluate Swerve on several scenarios and are able to show that Swerve is able to properly detect potential collisions between agents and static obstacles. In addition, we show that with symmetry and caching, Swerve is able to obtain 16x average speedup in service response time."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Software tools for scenario verification of autonomous systems exploiting dynamical symmetries"]}]}],"canonical_facts":{"dc:contributor":["Mitra, Sayan"],"dc:creator":["Li, Yangge"],"dc:date":["2022-04-29T21:46:19Z","2024-04-29T21:47:53Z","2021-12","2021-12-06"],"dc:description":["Submission published under a 24 month embargo labeled 'U of I Access', the embargo will last until 2023-12-01","The student, Yangge Li, accepted the attached license on 2021-12-06 at 15:39.","The student, Yangge Li, submitted this Thesis for approval on 2021-12-06 at 16:08.","This Thesis was approved for publication on 2021-12-06 at 16:30.","DSpace SAF Submission Ingestion Package generated from Vireo submission #17393 on 2022-04-06 at 17:17:56","Made available in DSpace on 2022-04-29T21:46:19Z (GMT). No. of bitstreams: 2 LI-THESIS-2021.pdf: 3056683 bytes, checksum: 7f2c59f98c06ea3e190abbaa6179b13a (MD5) LICENSE.txt: 4206 bytes, checksum: d2456dff4f67d41461426012486e2156 (MD5) Previous issue date: 2021-12-06","Embargo set by: Seth Robbins for item 123375 Lift date: 2024-04-29T21:46:25Z Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD system","Embargo set by: Seth Robbins for item 123375 Lift date: 2024-04-29T21:47:53Z Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD system","Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD system","U of I Only","In this thesis, we discuss using formal verification techniques to ensure the safety of autonomous systems. We present a particular type of verification problem called scenario verification, which involves vehicles executing complex plans in large cluttered workspaces. To solve the scenario verification problem, we present the tool SceneChecker. 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 implements symmetry abstractions, a novel refinement algorithm, and is built to enhance the performance of existing reachability analysis tools as a plug-in subroutine. We evaluated SceneChecker on several complicated scenarios with different types of agents. Compared to two leading tools, DryVR and Flow*, SceneChecker shows 20x speedup in verification time, even while using those tools as reachability subroutines. We further look into a variation of the scenario verification problem, with multiple agents running independently in the shared workspace. In addition, the plan is generated as the agent executing the scenario, which requires safety checking to be performed during runtime. To solve this problem, we present Swerve, an open-source cloud computing toolkit for efficient runtime collision checking for multi-agent autonomous systems. Swerve implements a remote server to check safety for different agents by using boundedtime reachability analysis. In addition, Swerve implements a cache to store already computed reachable sets and reuses them to avoid repeated computations. We evaluate Swerve on several scenarios and are able to show that Swerve is able to properly detect potential collisions between agents and static obstacles. In addition, we show that with symmetry and caching, Swerve is able to obtain 16x average speedup in service response time."],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/114011"],"dc:language":["en","eng"],"dc:rights":["Copyright 2021 Yangge Li"],"dc:subject":["Engineering"],"dc:title":["Software tools for scenario verification of autonomous systems exploiting dynamical symmetries"],"dc:type":["text","Thesis"],"thesis:degree_discipline":["Electrical & Computer Engr"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:54Z"}