Receding Horizon Control Synthesis for Signal Temporal Logic Specifications
Vasu Raman, Alexandre Donze, Richard Murray, Sanjit Seshia

Citation
Vasu Raman, Alexandre Donze, Richard Murray, Sanjit Seshia. "Receding Horizon Control Synthesis for Signal Temporal Logic Specifications". Talk or presentation, 29, October, 2014; Poster presented at the 2014 TerraSwarm Annual Meeting.

Abstract
We present a mathematical programming-based method for model predictive control of discrete-time cyber-physical systems subject to signal temporal logic (STL) specifications. We describe the use of STL to specify a wide range of properties of these systems, including safety, response and bounded liveness. For synthesis, we encode STL specifications as mixed integer-linear constraints on the variables of a discrete-time model of the system, and solve an optimization problem at each step of a model predictive control framework. We also present a counterexample-guided inductive synthesis approach to controller synthesis for systems operating in potentially adversarial nondeterministic environments. We present experimental results for controller synthesis for case studies in building climate control and autonomous driving.

Electronic downloads

Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Vasu Raman, Alexandre Donze, Richard Murray, Sanjit Seshia.
  <a
  href="http://www.terraswarm.org/pubs/454.html"><i>Receding
  Horizon Control Synthesis for Signal Temporal Logic
  Specifications</i></a>, Talk or presentation, 
  29, October, 2014;  Poster presented at the <a
  href="http://www.terraswarm.org/conferences/14/annual"
  >2014 TerraSwarm Annual Meeting</a>.

• Plain text

  Vasu Raman, Alexandre Donze, Richard Murray, Sanjit Seshia.
  "Receding Horizon Control Synthesis for Signal Temporal
  Logic Specifications". Talk or presentation,  29,
  October, 2014;  Poster presented at the <a
  href="http://www.terraswarm.org/conferences/14/annual"
  >2014 TerraSwarm Annual Meeting</a>.

• BibTeX

  @presentation{RamanDonzeMurraySeshia14_RecedingHorizonControlSynthesisForSignalTemporalLogic,
      author = {Vasu Raman and Alexandre Donze and Richard Murray
                and Sanjit Seshia},
      title = {Receding Horizon Control Synthesis for Signal
                Temporal Logic Specifications},
      day = {29},
      month = {October},
      year = {2014},
      note = { Poster presented at the <a
                href="http://www.terraswarm.org/conferences/14/annual"
                >2014 TerraSwarm Annual Meeting</a>.},
      abstract = {We present a mathematical programming-based method
                for model predictive control of discrete-time
                cyber-physical systems subject to signal temporal
                logic (STL) specifications. We describe the use of
                STL to specify a wide range of properties of these
                systems, including safety, response and bounded
                liveness. For synthesis, we encode STL
                specifications as mixed integer-linear constraints
                on the variables of a discrete-time model of the
                system, and solve an optimization problem at each
                step of a model predictive control framework. We
                also present a counterexample-guided inductive
                synthesis approach to controller synthesis for
                systems operating in potentially adversarial
                nondeterministic environments. We present
                experimental results for controller synthesis for
                case studies in building climate control and
                autonomous driving. },
      URL = {http://terraswarm.org/pubs/454.html}
  }
  

Posted by Vasu Raman on 10 Nov 2014.
Groups: tools