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 April 2015 | Submitted
Book Section - Chapter Open

Reactive Synthesis from Signal Temporal Logic Specifications

Abstract

We present a counterexample-guided inductive synthesis approach to controller synthesis for cyber-physical systems subject to signal temporal logic (STL) specifications, operating in potentially adversarial nondeterministic environments. We encode STL specifications as mixed integer-linear constraints on the variables of a discrete-time model of the system and environment dynamics, and solve a series of optimization problems to yield a satisfying control sequence. We demonstrate how the scheme can be used in a receding horizon fashion to fulfill properties over unbounded horizons, and present experimental results for reactive controller synthesis for case studies in building climate control and autonomous driving.

Additional Information

© 2015 ACM. This work was supported in part by TerraSwarm, one of six centers of STARnet, a Semiconductor Research Corporation program sponsored by MARCO and DARPA, by an NDSEG Fellowship, and by NSF grant # CCF-1116993.

Attached Files

Submitted - raman-hscc2015.pdf

Files

raman-hscc2015.pdf
Files (947.3 kB)
Name Size Download all
md5:050d3424a548037be1c6b1ff8f8a8ed3
947.3 kB Preview Download

Additional details

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