Reactive Synthesis from Signal Temporal Logic Specifications: Difference between revisions
From Murray Wiki
Jump to navigationJump to search
(htdb2wiki: creating page for 2014j_ram+15-hscc.html) |
No edit summary |
||
| Line 9: | Line 9: | ||
| abstract = | | 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. | 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. | ||
| flags = NCS | |||
| flags = | |||
| filetype = PDF | | filetype = PDF | ||
| filesize = 1.2M | | filesize = 1.2M | ||
Latest revision as of 06:07, 10 June 2016
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.
- Conference Paper: http://www.cds.caltech.edu/~murray/preprints/ram+15-hscc.pdf
- Project(s): SRC TerraSwarm
