{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/125614"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/125614","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Hierarchical synthesis for finite and infinite horizon specifications of nonlinear systems","abstract":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-02-04 without embargo terms","abstract_html":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-02-04 without embargo terms","abstract_has_math":false,"creators":["Miller, Kristina M"],"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","Viswanathan, Mahesh","Driggs-Campbell, Katherine","Ornik, Melkior","Phillips, Sean"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2024,"date_issued":"2024-07-11","date_published":"2024-07-11","updated_at":"2026-07-22T22:25:02Z","subjects":["Controller Synthesis","Motion Planning","Autonomous Systems","Reach-avoid","Linear Temporal Logic","Nonlinear Control"],"languages":["en","eng"],"rights":["Copyright 2024 Kristina Miller"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2142/125614","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Mitra, Sayan","Viswanathan, Mahesh","Driggs-Campbell, Katherine","Ornik, Melkior","Phillips, Sean"]},{"key":"dc:creator","label":"Author","values":["Miller, Kristina M"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2024-07-11","2024-08"]},{"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":["Controller Synthesis","Motion Planning","Autonomous Systems","Reach-avoid","Linear Temporal Logic","Nonlinear Control"]}]},{"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 2024 Kristina Miller"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/2142/125614"]}]},{"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 2025-02-04 without embargo terms","The student, Kristina Miller, accepted the attached license on 2024-07-11 at 10:32.","The student, Kristina Miller, submitted this Dissertation for approval on 2024-07-11 at 10:42.","This Dissertation was approved for publication on 2024-07-11 at 16:41.","DSpace SAF Submission Ingestion Package generated from Vireo submission #21062 on 2025-02-04 at 21:04:57","Autonomous robots are becoming more widespread, and are revolutionizing industries, with applications ranging from self-driving cars and smart agriculture to advanced satellite missions. These systems are composed of intricate subsystems like perception, decision-making, planning, and control. This dissertation focuses on decision and control by tackling the challenging motion planning problem for nonlinear robot models, with the goal of satisfying both finite and infinite horizon specifications. Controller synthesis aims to provide correct-by-construction policies, or controllers, which ensure that the robot satisfies the given specifications. This is typically done by solving a program using constraints to encode specifications. However, this is a notoriously difficult process. The nonlinear nature of robot models results in nonlinear and often nonconvex constraints that are difficult to solve. Additionally, continuous time dynamics and actuation limits can cause deviations from expected behavior. Finally, encoding specifications over an infinite horizon or with temporal components into a program is a difficult and non-trivial task. This dissertation addresses the issues of motion planning via a hierarchical approach towards synthesis. The main idea is to decompose the motion planning problem into smaller, more tractable parts. We show that the solutions to these smaller problems can then be used to synthesize controllers for both finite and infinite horizon specifications. This hierarchical approach also allows us to bypass the discretization step required by many state-of-the-art synthesis methods, which in turn reduces the issue of state-space explosion. First, we address the finite horizon synthesis problem. Our approach harnesses the physics of agents using traditional control theory to develop heuristics that allow us to linearize constraints, making the synthesis of controllers more manageable. The problem is decomposed into two parts. The first problem is to find a tracking controller which drives the agent towards an arbitrary reference trajectory. Applying reachability techniques such as Lyapunov analysis allows us to find an upper bound on the tracking error over any reference trajectory. The second problem is to find the concrete references which result in correct behavior of the agent. Using the tracking error bound, we can construct the reachable sets which contain the trajectories of the agent. We show that concrete references which result in agent trajectories that satisfy the specifications can be synthesized by solving a satisfiability problem over quantifier free linear real arithmetic. Next, we address infinite horizon specifications by breaking the problem into two parts. First, we need to identify the high-level, discrete behavior of the agent that meets the specifications. This high-level planning can be achieved by finding an automaton that accepts exactly the discrete behaviors satisfying the specifications. Second, we construct simulation relations between the agent’s behavior and the transitions of the automaton. We show that these relations can be constructed using reach-avoid synthesis. By concatenating a sequence of controllers that simulate a sequence of transitions accepted by the automaton, we can synthesize a controller that causes the agent to satisfy the specifications. This results in the first infinite horizon synthesis algorithm that does not require discretizations. Finally, we tackle online finite horizon synthesis in unknown environments by introducing a perception abstraction called a perception oracle. This oracle allows for a comprehensive examination of the correctness of motion planning algorithms. By invoking the perception oracle, we can synthesize controllers based on the predicted behavior of the local environment. Through repeated invocations of the perception oracle, the synthesis algorithm can be employed in a receding horizon manner to ensure the correct behavior of the agent. The algorithms developed here offer formal hard guarantees on the correctness and safety of robot behavior, which are not provided current state-of-the-art learning-based methods. They are implemented in a publicly available tool suite consisting of FACTEST, FACTEST+, ω-FACTEST, which solve for the static reach-avoid, ω-regular, and dynamic reach-avoid specifications respectively. We compare these tools to other state-of-the art synthesis tools across a variety of scenarios and demonstrate their effectiveness at synthesizing correct controllers."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Hierarchical synthesis for finite and infinite horizon specifications of nonlinear systems"]}]}],"canonical_facts":{"dc:contributor":["Mitra, Sayan","Viswanathan, Mahesh","Driggs-Campbell, Katherine","Ornik, Melkior","Phillips, Sean"],"dc:creator":["Miller, Kristina M"],"dc:date":["2024-07-11","2024-08"],"dc:description":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-02-04 without embargo terms","The student, Kristina Miller, accepted the attached license on 2024-07-11 at 10:32.","The student, Kristina Miller, submitted this Dissertation for approval on 2024-07-11 at 10:42.","This Dissertation was approved for publication on 2024-07-11 at 16:41.","DSpace SAF Submission Ingestion Package generated from Vireo submission #21062 on 2025-02-04 at 21:04:57","Autonomous robots are becoming more widespread, and are revolutionizing industries, with applications ranging from self-driving cars and smart agriculture to advanced satellite missions. These systems are composed of intricate subsystems like perception, decision-making, planning, and control. This dissertation focuses on decision and control by tackling the challenging motion planning problem for nonlinear robot models, with the goal of satisfying both finite and infinite horizon specifications. Controller synthesis aims to provide correct-by-construction policies, or controllers, which ensure that the robot satisfies the given specifications. This is typically done by solving a program using constraints to encode specifications. However, this is a notoriously difficult process. The nonlinear nature of robot models results in nonlinear and often nonconvex constraints that are difficult to solve. Additionally, continuous time dynamics and actuation limits can cause deviations from expected behavior. Finally, encoding specifications over an infinite horizon or with temporal components into a program is a difficult and non-trivial task. This dissertation addresses the issues of motion planning via a hierarchical approach towards synthesis. The main idea is to decompose the motion planning problem into smaller, more tractable parts. We show that the solutions to these smaller problems can then be used to synthesize controllers for both finite and infinite horizon specifications. This hierarchical approach also allows us to bypass the discretization step required by many state-of-the-art synthesis methods, which in turn reduces the issue of state-space explosion. First, we address the finite horizon synthesis problem. Our approach harnesses the physics of agents using traditional control theory to develop heuristics that allow us to linearize constraints, making the synthesis of controllers more manageable. The problem is decomposed into two parts. The first problem is to find a tracking controller which drives the agent towards an arbitrary reference trajectory. Applying reachability techniques such as Lyapunov analysis allows us to find an upper bound on the tracking error over any reference trajectory. The second problem is to find the concrete references which result in correct behavior of the agent. Using the tracking error bound, we can construct the reachable sets which contain the trajectories of the agent. We show that concrete references which result in agent trajectories that satisfy the specifications can be synthesized by solving a satisfiability problem over quantifier free linear real arithmetic. Next, we address infinite horizon specifications by breaking the problem into two parts. First, we need to identify the high-level, discrete behavior of the agent that meets the specifications. This high-level planning can be achieved by finding an automaton that accepts exactly the discrete behaviors satisfying the specifications. Second, we construct simulation relations between the agent’s behavior and the transitions of the automaton. We show that these relations can be constructed using reach-avoid synthesis. By concatenating a sequence of controllers that simulate a sequence of transitions accepted by the automaton, we can synthesize a controller that causes the agent to satisfy the specifications. This results in the first infinite horizon synthesis algorithm that does not require discretizations. Finally, we tackle online finite horizon synthesis in unknown environments by introducing a perception abstraction called a perception oracle. This oracle allows for a comprehensive examination of the correctness of motion planning algorithms. By invoking the perception oracle, we can synthesize controllers based on the predicted behavior of the local environment. Through repeated invocations of the perception oracle, the synthesis algorithm can be employed in a receding horizon manner to ensure the correct behavior of the agent. The algorithms developed here offer formal hard guarantees on the correctness and safety of robot behavior, which are not provided current state-of-the-art learning-based methods. They are implemented in a publicly available tool suite consisting of FACTEST, FACTEST+, ω-FACTEST, which solve for the static reach-avoid, ω-regular, and dynamic reach-avoid specifications respectively. We compare these tools to other state-of-the art synthesis tools across a variety of scenarios and demonstrate their effectiveness at synthesizing correct controllers."],"dc:format":["application/pdf"],"dc:identifier":["https://hdl.handle.net/2142/125614"],"dc:language":["en","eng"],"dc:rights":["Copyright 2024 Kristina Miller"],"dc:subject":["Controller Synthesis","Motion Planning","Autonomous Systems","Reach-avoid","Linear Temporal Logic","Nonlinear Control"],"dc:title":["Hierarchical synthesis for finite and infinite horizon specifications of nonlinear systems"],"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:25:02Z"}