Flexible Computational Pipelines for Robust Abstraction-Based Control Synthesis

Eric Kim, Murat Arcak, and Sanjit A. Seshia. Flexible Computational Pipelines for Robust Abstraction-Based Control Synthesis. In 31st International Conference on Computer Aided Verification (CAV), July 2019.

Download

[pdf] 

Abstract

Successfully synthesizing controllers for complex dynamical systems and specifications often requires leveraging domain knowledge as well as making difficult computational or mathematical tradeoffs. This paper presents a flexible and extensible framework for constructing robust control synthesis algorithms and applies this to the traditional abstraction-based control synthesis pipeline. It is grounded in the theory of relational interfaces and provides a principled methodology to seamlessly combine different techniques (such as dynamic precision grids, refining abstractions while synthesizing, or decomposed control predecessors) or create custom procedures to exploit an application's intrinsic structural properties. A Dubins vehicle is used as a motivating example to showcase memory and runtime improvements.

BibTeX

@inproceedings{kim-cav19,
  author    = {Eric Kim and
               Murat Arcak and
               Sanjit A. Seshia},
  title     = {Flexible Computational Pipelines for Robust Abstraction-Based Control Synthesis},
  booktitle = {31st International Conference on Computer Aided Verification (CAV)},
  month = jul,
  year = {2019},
  abstract = {Successfully synthesizing controllers for complex dynamical 
systems and specifications often requires leveraging domain knowledge 
as well as making difficult computational or mathematical tradeoffs. 
This paper presents a flexible and extensible framework for constructing 
robust control synthesis algorithms and applies this to the traditional 
abstraction-based control synthesis pipeline. It is grounded in the theory 
of relational interfaces and provides a principled methodology to seamlessly 
combine different techniques (such as dynamic precision grids, refining abstractions while synthesizing, or decomposed control predecessors) 
or create custom procedures to exploit an application's intrinsic 
structural properties. A Dubins vehicle is used as a motivating example 
to showcase memory and runtime improvements.},
}