CaltechTHESIS
  A Caltech Library Service

Scalable Synthesis and Verification: Towards Reliable Autonomy

Citation

Dathathri, Sumanth (2020) Scalable Synthesis and Verification: Towards Reliable Autonomy. Dissertation (Ph.D.), California Institute of Technology. doi:10.7907/4j39-v857. https://resolver.caltech.edu/CaltechTHESIS:04292020-165136662

Abstract

We have seen the growing deployment of autonomous systems in our daily life, ranging from safety-critical self-driving cars to dialogue agents. While impactful and impressive, these systems do not often come with guarantees and are not rigorously evaluated for failure cases. This is in part due to the limited scalability of tools available for designing correct-by-construction systems, or verifying them posthoc. Another key limitation is the lack of availability of models for the complex environments with which autonomous systems often have to interact with. In the direction of overcoming these above mentioned bottlenecks to designing reliable autonomous systems, this thesis makes contributions along three fronts.

First, we develop an approach for parallelized synthesis from linear-time temporal logic Specifications corresponding to the generalized reactivity (1) fragment. We begin by identifying a special case corresponding to singleton liveness goals that allows for a decomposition of the synthesis problem, which facilitates parallelized synthesis. Based on the intuition from this special case, we propose a more generalized approach for parallelized synthesis that relies on identifying equicontrollable states.

Second, we consider learning-based approaches to enable verification at scale for complex systems, and for autonomous systems that interact with black-box environments. For the former, we propose a new abstraction refinement procedure based on machine learning to improve the performance of nonlinear constraint solving algorithms on large-scale problems. For the latter, we present a data-driven approach based on chance-constrained optimization that allows for a system to be evaluated for specification conformance without an accurate model of the environment. We demonstrate this approach on several tasks, including a lane-change scenario with real-world driving data.

Lastly, we consider the problem of interpreting and verifying learning-based components such as neural networks. We introduce a new method based on Craig's interpolants for computing compact symbolic abstractions of pre-images for neural networks. Our approach relies on iteratively computing approximations that provably overapproximate and underapproximate the pre-images at all layers. Further, building on existing work for training neural networks for verifiability in the classification setting, we propose extensions that allow us to generalize the approach to more general architectures and temporal specifications.

Item Type:Thesis (Dissertation (Ph.D.))
Subject Keywords:Formal Verification, Control Synthesis, Hybrid Systems, Machine Learning
Degree Grantor:California Institute of Technology
Division:Engineering and Applied Science
Major Option:Computing and Mathematical Sciences
Thesis Availability:Public (worldwide access)
Research Advisor(s):
  • Murray, Richard M.
Thesis Committee:
  • Burdick, Joel Wakeman (chair)
  • Chandy, K. Mani
  • Gao, Sicun
  • Murray, Richard M.
Defense Date:2 March 2020
Record Number:CaltechTHESIS:04292020-165136662
Persistent URL:https://resolver.caltech.edu/CaltechTHESIS:04292020-165136662
DOI:10.7907/4j39-v857
Related URLs:
URLURL TypeDescription
https://doi.org/10.1109/CDC.2017.8263775DOIArticle adapted for Chapter 2.
https://doi.org/10.1007/978-3-030-28619-4_57DOIArticle adapted for Chapter 2.
https://arxiv.org/abs/2001.07233arXivArticle adapted for Chapter 3.
https://doi.org/10.1145/3055378.3055384DOIArticle adapted for Chapter 3.
https://doi.org/10.24963/ijcai.2017/83DOIArticle adapted for Chapter 3.
https://openreview.net/forum?id=BklC2RNKDSOtherArticle adapted for Chapter 4.
https://doi.org/10.1609/aaai.v33i01.33013437DOIArticle adapted for Chapter 4.
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:13689
Collection:CaltechTHESIS
Deposited By: Sumanth Dathathri
Deposited On:06 May 2020 22:58
Last Modified:13 May 2020 16:53

Thesis Files

[img]
Preview
PDF (Main File) - Final Version
See Usage Policy.

1MB

Repository Staff Only: item control page