{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/122050"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/122050","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Certifiable synthesis and analysis for autonomy: Data-driven and analytical techniques","abstract":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2024-03-01 without embargo terms","abstract_html":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2024-03-01 without embargo terms","abstract_has_math":false,"creators":["Sun, Dawei"],"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","Dullerud, Geir E.","Srikant, Rayadurgam","Belabbas, Mohamed Ali"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2023,"date_issued":"2023-12","date_published":"2023-12","updated_at":"2026-07-22T22:25:00Z","subjects":["Machine Learning","Control Theory","Safe Autonomy","Robotics"],"languages":["en","eng"],"rights":["Copyright 2023 Dawei Sun"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2142/122050","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Mitra, Sayan","Dullerud, Geir E.","Srikant, Rayadurgam","Belabbas, Mohamed Ali"]},{"key":"dc:creator","label":"Author","values":["Sun, Dawei"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2023-12","2023-12-01"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"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":["Machine Learning","Control Theory","Safe Autonomy","Robotics"]}]},{"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 2023 Dawei Sun"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/2142/122050"]}]},{"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 2024-03-01 without embargo terms","The student, Dawei Sun, accepted the attached license on 2023-12-01 at 12:42.","The student, Dawei Sun, submitted this Dissertation for approval on 2023-12-01 at 12:49.","This Dissertation was approved for publication on 2023-12-01 at 14:43.","DSpace SAF Submission Ingestion Package generated from Vireo submission #20110 on 2024-03-01 at 13:15:21","Over the past few decades, progress in control theory, robotics, and machine learning has enabled autonomy across diverse application domains such as the chemical industry, mechanical manufacturing, and the aerospace industry. Despite these advances, the development and implementation of autonomous systems continue to confront numerous technical challenges. One particular issue is ensuring the certifiability of autonomous systems. As these systems enter more and more safety-critical applications, constructing certifiable systems becomes a crucial task for the community. In traditional industrial applications such as aircraft manufacturing, this problem has been extensively addressed with established certification standards. However, the same cannot be said for emerging autonomous systems interacting with complex environments, for instance, autonomous vehicles. Certifiability in these contexts remains a distant goal. In this dissertation, we focus on two types of problems, namely, the synthesis problem and the analysis problem. We combine data-driven approaches and analytical approaches to solve these two types of problems. The core contributions of this dissertation include (1) A formal definition of a general synthesis problem for temporal logic specifications. (2) A learning-based approach that incorporates contraction theory into machine learning to construct a tracking controller for a given dynamical system. Moreover, the tracking error of the synthesized controller is formally bounded. (3) An optimization-based path planner for signal temporal logic specifications. By combining the path planner and the tracking controller, we solve the synthesis problem defined in (1). (4) The notion of reachability functions and a tool, NeuReach, that can automatically construct a reachability function for a black-box system. (5) Demonstration of the proposed approaches on a perception-based control synthesis problem. For all the proposed approaches, we arm them with rigorous theoretical analysis. On the experimental side, we evaluate the proposed approaches on a variety of benchmarks in simulation. Moreover, we deploy some of the approaches on a quadcopter to complete a trajectory-tracking task and a safe landing task."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Certifiable synthesis and analysis for autonomy: Data-driven and analytical techniques"]}]}],"canonical_facts":{"dc:contributor":["Mitra, Sayan","Dullerud, Geir E.","Srikant, Rayadurgam","Belabbas, Mohamed Ali"],"dc:creator":["Sun, Dawei"],"dc:date":["2023-12","2023-12-01"],"dc:description":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2024-03-01 without embargo terms","The student, Dawei Sun, accepted the attached license on 2023-12-01 at 12:42.","The student, Dawei Sun, submitted this Dissertation for approval on 2023-12-01 at 12:49.","This Dissertation was approved for publication on 2023-12-01 at 14:43.","DSpace SAF Submission Ingestion Package generated from Vireo submission #20110 on 2024-03-01 at 13:15:21","Over the past few decades, progress in control theory, robotics, and machine learning has enabled autonomy across diverse application domains such as the chemical industry, mechanical manufacturing, and the aerospace industry. Despite these advances, the development and implementation of autonomous systems continue to confront numerous technical challenges. One particular issue is ensuring the certifiability of autonomous systems. As these systems enter more and more safety-critical applications, constructing certifiable systems becomes a crucial task for the community. In traditional industrial applications such as aircraft manufacturing, this problem has been extensively addressed with established certification standards. However, the same cannot be said for emerging autonomous systems interacting with complex environments, for instance, autonomous vehicles. Certifiability in these contexts remains a distant goal. In this dissertation, we focus on two types of problems, namely, the synthesis problem and the analysis problem. We combine data-driven approaches and analytical approaches to solve these two types of problems. The core contributions of this dissertation include (1) A formal definition of a general synthesis problem for temporal logic specifications. (2) A learning-based approach that incorporates contraction theory into machine learning to construct a tracking controller for a given dynamical system. Moreover, the tracking error of the synthesized controller is formally bounded. (3) An optimization-based path planner for signal temporal logic specifications. By combining the path planner and the tracking controller, we solve the synthesis problem defined in (1). (4) The notion of reachability functions and a tool, NeuReach, that can automatically construct a reachability function for a black-box system. (5) Demonstration of the proposed approaches on a perception-based control synthesis problem. For all the proposed approaches, we arm them with rigorous theoretical analysis. On the experimental side, we evaluate the proposed approaches on a variety of benchmarks in simulation. Moreover, we deploy some of the approaches on a quadcopter to complete a trajectory-tracking task and a safe landing task."],"dc:format":["application/pdf"],"dc:identifier":["https://hdl.handle.net/2142/122050"],"dc:language":["en","eng"],"dc:rights":["Copyright 2023 Dawei Sun"],"dc:subject":["Machine Learning","Control Theory","Safe Autonomy","Robotics"],"dc:title":["Certifiable synthesis and analysis for autonomy: Data-driven and analytical techniques"],"dc:type":["text"],"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:25:00Z"}