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

[pdf] 

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.},
}