A Caltech Library Service

An Iterative Abstraction Algorithm for Reactive Correct-by-Construction Controller Synthesis

Mattila, Robert and Mo, Yilin and Murray, Richard M. (2015) An Iterative Abstraction Algorithm for Reactive Correct-by-Construction Controller Synthesis. In: 54th IEEE Conference on Decision and Control (CDC), 2015. IEEE , Piscataway, NJ, pp. 6147-6152. ISBN 978-1-4799-7886-1.

[img] PDF - Submitted Version
See Usage Policy.


Use this Persistent URL to link to this item:


In this paper, we consider the problem of synthesizing correct-by-construction controllers for discrete-time dynamical systems. A commonly adopted approach in the literature is to abstract the dynamical system into a Finite Transition System (FTS) and thus convert the problem into a two player game between the environment and the system on the FTS. The controller design problem can then be solved using synthesis tools for general linear temporal logic or generalized reactivity(1) specifications. In this article, we propose a new abstraction algorithm. Instead of generating a single FTS to represent the system, we generate two FTSs, which are under- and over-approximations of the original dynamical system. We further develop an iterative abstraction scheme by exploiting the concept of winning sets, i.e., the sets of states for which there exists a winning strategy for the system. Finally, the efficiency of the new abstraction algorithm is illustrated by numerical examples.

Item Type:Book Section
Related URLs:
URLURL TypeDescription Paper
Mo, Yilin0000-0001-7937-6737
Murray, Richard M.0000-0002-5785-7481
Additional Information:© 2015 IEEE. Date Added to IEEE Xplore: 11 February 2016. This work is supported in part by IBM and UTC through the Industrial Cyber-Physical Systems Center (iCyPhy) consortium.
Funding AgencyGrant Number
Industrial Cyber-Physical Systems Center (iCyPhy)UNSPECIFIED
Record Number:CaltechAUTHORS:20161208-102939866
Persistent URL:
Official Citation:R. Mattila, Y. Mo and R. M. Murray, "An iterative abstraction algorithm for reactive correct-by-construction controller synthesis," 2015 54th IEEE Conference on Decision and Control (CDC), Osaka, 2015, pp. 6147-6152. doi: 10.1109/CDC.2015.7403186
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:72660
Deposited By: Ruth Sustaita
Deposited On:08 Dec 2016 21:41
Last Modified:31 Jan 2020 17:26

Repository Staff Only: item control page