CaltechTHESIS
  A Caltech Library Service

Incremental Control Synthesis for Robotics in the Presence of Temporal Logic Specifications

Citation

Livingston, Scott Carlton (2016) Incremental Control Synthesis for Robotics in the Presence of Temporal Logic Specifications. Dissertation (Ph.D.), California Institute of Technology. doi:10.7907/Z94Q7RW3. http://resolver.caltech.edu/CaltechTHESIS:12312015-131513787

Abstract

This thesis presents methods for incrementally constructing controllers in the presence of uncertainty and nonlinear dynamics. The basic setting is motion planning subject to temporal logic specifications. Broadly, two categories of problems are treated. The first is reactive formal synthesis when so-called discrete abstractions are available. The fragment of linear-time temporal logic (LTL) known as GR(1) is used to express assumptions about an adversarial environment and requirements of the controller. Two problems of changes to a specification are posed that concern the two major aspects of GR(1): safety and liveness. Algorithms providing incremental updates to strategies are presented as solutions. In support of these, an annotation of strategies is developed that facilitates repeated modifications. A variety of properties are proven about it, including necessity of existence and sufficiency for a strategy to be winning. The second category of problems considered is non-reactive (open-loop) synthesis in the absence of a discrete abstraction. Instead, the presented stochastic optimization methods directly construct a control input sequence that achieves low cost and satisfies a LTL formula. Several relaxations are considered as heuristics to address the rarity of sampling trajectories that satisfy an LTL formula and demonstrated to improve convergence rates for Dubins car and single-integrators subject to a recurrence task.

Item Type:Thesis (Dissertation (Ph.D.))
Subject Keywords:hybrid systems; reactive synthesis; incremental control; stochastic optimization; LTL; GR(1); formal specification; task planning
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
  • Holzmann, Gerard J.
  • Perona, Pietro
Defense Date:23 November 2015
Funders:
Funding AgencyGrant Number
Boeing CorporationUNSPECIFIED
United Technologies CorporationUNSPECIFIED
IBMUNSPECIFIED
Record Number:CaltechTHESIS:12312015-131513787
Persistent URL:http://resolver.caltech.edu/CaltechTHESIS:12312015-131513787
DOI:10.7907/Z94Q7RW3
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:9348
Collection:CaltechTHESIS
Deposited By: Scott Livingston
Deposited On:11 Jan 2016 21:58
Last Modified:18 May 2017 18:32

Thesis Files

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

1667Kb

Repository Staff Only: item control page