Reactive Synthesis from Signal Temporal Logic Specifications

From Murray Wiki
Jump to navigationJump to search

Vasumathi Raman, Alexandre Donze, Dorsa Sadigh, Richard M. Murray and Sanjit A. Seshia
2015 International Conference on Hybrid Systems: Computation and Control (HSCC)

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.