Welcome to the new version of CaltechAUTHORS. Login is currently restricted to library staff. If you notice any issues, please email coda@library.caltech.edu
Published December 2015 | Submitted
Book Section - Chapter Open

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

Abstract

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.

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.

Attached Files

Submitted - 1509.04125.pdf

Files

1509.04125.pdf
Files (378.4 kB)
Name Size Download all
md5:02e52b673f20f6c8733058e9d9022efd
378.4 kB Preview Download

Additional details

Created:
August 20, 2023
Modified:
October 23, 2023