Hierarchical synthesis for finite and infinite horizon specifications of nonlinear systems

Miller, Kristina M

Permalink

https://hdl.handle.net/2142/125614 Copy

Description

Title

Hierarchical synthesis for finite and infinite horizon specifications of nonlinear systems

Author(s)

Miller, Kristina M

Issue Date

2024-07-11

Director of Research (if dissertation) or Advisor (if thesis)

Mitra, Sayan

Doctoral Committee Chair(s)

Mitra, Sayan

Committee Member(s)

• Viswanathan, Mahesh
• Driggs-Campbell, Katherine
• Ornik, Melkior
• Phillips, Sean

Department of Study

Electrical & Computer Eng

Discipline

Electrical & Computer Engr

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

• Controller synthesis
• motion planning
• autonomous systems
• reach-avoid
• linear temporal logic
• nonlinear control

Abstract

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.

Graduation Semester

2024-08

Type of Resource

Thesis

Handle URL

https://hdl.handle.net/2142/125614

Copyright and License Information

Copyright 2024 Kristina Miller

Owning Collections