CaltechTHESIS
  A Caltech Library Service

Control of Dynamical Systems with Temporal Logic Specifications

Citation

Wolff, Eric McKenzie (2014) Control of Dynamical Systems with Temporal Logic Specifications. Dissertation (Ph.D.), California Institute of Technology. doi:10.7907/TGFR-SS39. https://resolver.caltech.edu/CaltechTHESIS:02172014-121159358

Abstract

This thesis is motivated by safety-critical applications involving autonomous air, ground, and space vehicles carrying out complex tasks in uncertain and adversarial environments. We use temporal logic as a language to formally specify complex tasks and system properties. Temporal logic specifications generalize the classical notions of stability and reachability that are studied in the control and hybrid systems communities. Given a system model and a formal task specification, the goal is to automatically synthesize a control policy for the system that ensures that the system satisfies the specification. This thesis presents novel control policy synthesis algorithms for optimal and robust control of dynamical systems with temporal logic specifications. Furthermore, it introduces algorithms that are efficient and extend to high-dimensional dynamical systems.

The first contribution of this thesis is the generalization of a classical linear temporal logic (LTL) control synthesis approach to optimal and robust control. We show how we can extend automata-based synthesis techniques for discrete abstractions of dynamical systems to create optimal and robust controllers that are guaranteed to satisfy an LTL specification. Such optimal and robust controllers can be computed at little extra computational cost compared to computing a feasible controller.

The second contribution of this thesis addresses the scalability of control synthesis with LTL specifications. A major limitation of the standard automaton-based approach for control with LTL specifications is that the automaton might be doubly-exponential in the size of the LTL specification. We introduce a fragment of LTL for which one can compute feasible control policies in time polynomial in the size of the system and specification. Additionally, we show how to compute optimal control policies for a variety of cost functions, and identify interesting cases when this can be done in polynomial time. These techniques are particularly relevant for online control, as one can guarantee that a feasible solution can be found quickly, and then iteratively improve on the quality as time permits.

The final contribution of this thesis is a set of algorithms for computing feasible trajectories for high-dimensional, nonlinear systems with LTL specifications. These algorithms avoid a potentially computationally-expensive process of computing a discrete abstraction, and instead compute directly on the system's continuous state space. The first method uses an automaton representing the specification to directly encode a series of constrained-reachability subproblems, which can be solved in a modular fashion by using standard techniques. The second method encodes an LTL formula as mixed-integer linear programming constraints on the dynamical system. We demonstrate these approaches with numerical experiments on temporal logic motion planning problems with high-dimensional (10+ states) continuous systems.

Item Type:Thesis (Dissertation (Ph.D.))
Subject Keywords:Cyberphysical systems, hybrid systems, temporal logic, optimal control, robust control, optimization, automata, dynamic programming
Degree Grantor:California Institute of Technology
Division:Engineering and Applied Science
Major Option:Control and Dynamical Systems
Thesis Availability:Public (worldwide access)
Research Advisor(s):
  • Murray, Richard M.
Thesis Committee:
  • Murray, Richard M. (chair)
  • Burdick, Joel Wakeman
  • Topcu, Ufuk
  • Chandy, K. Mani
Defense Date:12 May 2014
Non-Caltech Author Email:eric.m.wolff (AT) gmail.com
Funders:
Funding AgencyGrant Number
NSF Graduate Research FellowshipUNSPECIFIED
NDSEG FellowshipUNSPECIFIED
The Boeing CompanyUNSPECIFIED
Record Number:CaltechTHESIS:02172014-121159358
Persistent URL:https://resolver.caltech.edu/CaltechTHESIS:02172014-121159358
DOI:10.7907/TGFR-SS39
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:8078
Collection:CaltechTHESIS
Deposited By: Eric Wolff
Deposited On:02 Jun 2014 22:36
Last Modified:04 Oct 2019 00:03

Thesis Files

[img]
Preview
PDF - Final Version
See Usage Policy.

2MB

Repository Staff Only: item control page