Reactive Synthesis from Signal Temporal Logic Specifications
Vasumathi Raman, Alexandre Donzé, Dorsa Sadigh, Richard M. Murray, and Sanjit A. Seshia. Reactive Synthesis from Signal Temporal Logic Specifications. In Proceedings of the 8th International Conference on Hybrid Systems: Computation and Control (HSCC 2015), pp. 239–248, April 2015.
Download
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.
BibTeX
@inproceedings{raman-hscc15, author = {Vasumathi Raman and Alexandre Donz{\'{e}} and Dorsa Sadigh and Richard M. Murray and Sanjit A. Seshia}, title = {Reactive Synthesis from Signal Temporal Logic Specifications}, booktitle = {Proceedings of the 8th International Conference on Hybrid Systems: Computation and Control (HSCC 2015)}, month = "April", year = {2015}, pages = {239--248}, 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.}, }