{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/113918"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/113918","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Accelerating cerification of cyber-physical systems using symmetry","abstract":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2022-04-06 without embargo terms","abstract_html":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2022-04-06 without embargo terms","abstract_has_math":false,"creators":["Sibai, Hussein"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Electrical & Computer Engr","degree_department":null,"school":null,"contributors":["Mitra, Sayan","Liberzon, Daniel","Forsyth, David","Dullerud, Geir","Misailovic, Sasa"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2022,"date_issued":"2022-04-29T21:34:54Z","date_published":"2022-04-29T21:34:54Z","updated_at":"2026-07-22T22:24:53Z","subjects":["Engineering"],"languages":["en","eng"],"rights":["Copyright 2021 Hussein Sibai"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/113918","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Mitra, Sayan","Liberzon, Daniel","Forsyth, David","Dullerud, Geir","Misailovic, Sasa"]},{"key":"dc:creator","label":"Author","values":["Sibai, Hussein"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2022-04-29T21:34:54Z","2021-12","2021-12-03"]},{"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":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"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 Hussein Sibai"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/113918"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2022-04-06 without embargo terms","The student, Hussein Sibai, accepted the attached license on 2021-12-03 at 14:45.","The student, Hussein Sibai, submitted this Dissertation for approval on 2021-12-03 at 14:56.","This Dissertation was approved for publication on 2021-12-03 at 15:58.","DSpace SAF Submission Ingestion Package generated from Vireo submission #17386 on 2022-04-06 at 17:11:03","Made available in DSpace on 2022-04-29T21:34:54Z (GMT). No. of bitstreams: 2 SIBAI-DISSERTATION-2021.pdf: 68593623 bytes, checksum: 75587b8a8f10471cadbaf2657a218d6c (MD5) LICENSE.txt: 4210 bytes, checksum: e984df708eb8b2059436cd81be09fed3 (MD5) Previous issue date: 2021-12-03","Autonomous systems are increasingly being deployed in safety-critical applications such as transportation and medicine. Numerous approaches to analyze their safety have been considered including testing, falsification, and formal verification. The major challenge for all of these approaches is scalability to large and complex models. To address this challenge, we propose to use the symmetry naturally present in the dynamics of many of these systems. Reachability-based safety analysis simulates the dynamical models of the autonomous systems, such as differential equations or hybrid automata, and checks if any of their reachable states is unsafe. Symmetries in dynamical systems are maps that transform any of their trajectories to other trajectories. In this thesis, we show how to use known symmetries of autonomous systems to cache their reachable states and abstract their dynamical models to accelerate their safety analysis. The main contributions of this thesis are as follows: 1. Augmenting a state-of-the-art data-driven safety verification algorithm with a cache to reuse computed sets of reachable states. The proposed algorithm uses symmetries of the model under verification to increase the cache hit rate. 2. Augmenting traditional hybrid automata safety verification algorithms with a cache to reuse computed sets of reachable states. The proposed algorithm uses symmetries to share computed reachable sets between different modes and automata being verified. 3. Abstracting hybrid automata by combining modes with symmetric dynamics in the same abstract modes. 4. Designing a symmetry-based counter-example guided abstraction-refinement (CEGAR) algorithm for hybrid automata with symmetric continuous dynamics to accelerate their safety verification. 5. Finally, designing an efficient testing algorithm for autonomous systems that uses a cache to share symmetric trajectories among the test cases of a test suite, avoiding repetition of high-fidelity simulations. The algorithmic contributions of this thesis come with theoretical guarantees that ensure their soundness and completeness. The algorithms presented build on top of state-of-the-art reachability analysis and verification algorithms. They accelerate their computations, without affecting their soundness and completeness guarantees. Finally, we present software implementations and empirical analyses of the different algorithms presented, showing up to orders of magnitude speedup in verification and testing time of different dynamical models including a car, fixed-wing aircraft, a neural network-controlled quadrotor, and a Gazebo-based Hector quadrotor."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Accelerating cerification of cyber-physical systems using symmetry"]}]}],"canonical_facts":{"dc:contributor":["Mitra, Sayan","Liberzon, Daniel","Forsyth, David","Dullerud, Geir","Misailovic, Sasa"],"dc:creator":["Sibai, Hussein"],"dc:date":["2022-04-29T21:34:54Z","2021-12","2021-12-03"],"dc:description":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2022-04-06 without embargo terms","The student, Hussein Sibai, accepted the attached license on 2021-12-03 at 14:45.","The student, Hussein Sibai, submitted this Dissertation for approval on 2021-12-03 at 14:56.","This Dissertation was approved for publication on 2021-12-03 at 15:58.","DSpace SAF Submission Ingestion Package generated from Vireo submission #17386 on 2022-04-06 at 17:11:03","Made available in DSpace on 2022-04-29T21:34:54Z (GMT). No. of bitstreams: 2 SIBAI-DISSERTATION-2021.pdf: 68593623 bytes, checksum: 75587b8a8f10471cadbaf2657a218d6c (MD5) LICENSE.txt: 4210 bytes, checksum: e984df708eb8b2059436cd81be09fed3 (MD5) Previous issue date: 2021-12-03","Autonomous systems are increasingly being deployed in safety-critical applications such as transportation and medicine. Numerous approaches to analyze their safety have been considered including testing, falsification, and formal verification. The major challenge for all of these approaches is scalability to large and complex models. To address this challenge, we propose to use the symmetry naturally present in the dynamics of many of these systems. Reachability-based safety analysis simulates the dynamical models of the autonomous systems, such as differential equations or hybrid automata, and checks if any of their reachable states is unsafe. Symmetries in dynamical systems are maps that transform any of their trajectories to other trajectories. In this thesis, we show how to use known symmetries of autonomous systems to cache their reachable states and abstract their dynamical models to accelerate their safety analysis. The main contributions of this thesis are as follows: 1. Augmenting a state-of-the-art data-driven safety verification algorithm with a cache to reuse computed sets of reachable states. The proposed algorithm uses symmetries of the model under verification to increase the cache hit rate. 2. Augmenting traditional hybrid automata safety verification algorithms with a cache to reuse computed sets of reachable states. The proposed algorithm uses symmetries to share computed reachable sets between different modes and automata being verified. 3. Abstracting hybrid automata by combining modes with symmetric dynamics in the same abstract modes. 4. Designing a symmetry-based counter-example guided abstraction-refinement (CEGAR) algorithm for hybrid automata with symmetric continuous dynamics to accelerate their safety verification. 5. Finally, designing an efficient testing algorithm for autonomous systems that uses a cache to share symmetric trajectories among the test cases of a test suite, avoiding repetition of high-fidelity simulations. The algorithmic contributions of this thesis come with theoretical guarantees that ensure their soundness and completeness. The algorithms presented build on top of state-of-the-art reachability analysis and verification algorithms. They accelerate their computations, without affecting their soundness and completeness guarantees. Finally, we present software implementations and empirical analyses of the different algorithms presented, showing up to orders of magnitude speedup in verification and testing time of different dynamical models including a car, fixed-wing aircraft, a neural network-controlled quadrotor, and a Gazebo-based Hector quadrotor."],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/113918"],"dc:language":["en","eng"],"dc:rights":["Copyright 2021 Hussein Sibai"],"dc:subject":["Engineering"],"dc:title":["Accelerating cerification of cyber-physical systems using symmetry"],"dc:type":["text","Thesis"],"thesis:degree_discipline":["Electrical & Computer Engr"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:53Z"}