Diagnosis and Repair for Synthesis from Signal Temporal Logic Specifications
Shromona Ghosh, Sadigh Dorsa, Pierluigi Nuzzo, Vasu Raman, Alexandre Donze, Alberto Sangiovanni-Vincentelli, S. Shankar Sastry, Sanjit Seshia

Citation
Shromona Ghosh, Sadigh Dorsa, Pierluigi Nuzzo, Vasu Raman, Alexandre Donze, Alberto Sangiovanni-Vincentelli, S. Shankar Sastry, Sanjit Seshia. "Diagnosis and Repair for Synthesis from Signal Temporal Logic Specifications". Hybrid Systems: Computation and Control, 12, April, 2016.

Abstract
We address the problem of diagnosing and repairing speci cations for hybrid systems formalized in signal temporal logic (STL). Our focus is on the setting of automatic synthesis of controllers in a model predictive control (MPC) framework. We build on recent approaches that reduce the controller synthesis problem to solving one or more mixed integer linear programs (MILPs), where infeasibility of a MILP usually indicates unrealizability of the controller synthesis problem. Given an infeasible STL synthesis problem, we present algorithms that provide feedback on the reasons for unrealizability, and suggestions for making it realizable. Our algorithms are sound and complete, i. e., they provide a correct diagnosis, and always terminate with a non-trivial speci cation that is feasible using the chosen synthesis method, when such a solution exists. We demonstrate the eectiveness of our approach on the synthesis of controllers for various cyber-physical systems, including an autonomous driving application and an aircraft electric power system.

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

  Shromona Ghosh, Sadigh Dorsa, Pierluigi Nuzzo, Vasu Raman,
  Alexandre Donze, Alberto Sangiovanni-Vincentelli, S. Shankar
  Sastry, Sanjit Seshia. <a
  href="http://www.terraswarm.org/pubs/736.html"
  >Diagnosis and Repair for Synthesis from Signal Temporal
  Logic Specifications</a>, Hybrid Systems: Computation
  and Control, 12, April, 2016.

• Plain text

  Shromona Ghosh, Sadigh Dorsa, Pierluigi Nuzzo, Vasu Raman,
  Alexandre Donze, Alberto Sangiovanni-Vincentelli, S. Shankar
  Sastry, Sanjit Seshia. "Diagnosis and Repair for
  Synthesis from Signal Temporal Logic Specifications".
  Hybrid Systems: Computation and Control, 12, April, 2016.

• BibTeX

  @inproceedings{GhoshDorsaNuzzoRamanDonzeSangiovanniVincentelliSastry16_DiagnosisRepairForSynthesisFromSignalTemporalLogicSpecifications,
      author = {Shromona Ghosh and Sadigh Dorsa and Pierluigi
                Nuzzo and Vasu Raman and Alexandre Donze and
                Alberto Sangiovanni-Vincentelli and S. Shankar
                Sastry and Sanjit Seshia},
      title = {Diagnosis and Repair for Synthesis from Signal
                Temporal Logic Specifications},
      booktitle = {Hybrid Systems: Computation and Control},
      day = {12},
      month = {April},
      year = {2016},
      abstract = {We address the problem of diagnosing and repairing
                speci cations for hybrid systems formalized in
                signal temporal logic (STL). Our focus is on the
                setting of automatic synthesis of controllers in a
                model predictive control (MPC) framework. We build
                on recent approaches that reduce the controller
                synthesis problem to solving one or more mixed
                integer linear programs (MILPs), where
                infeasibility of a MILP usually indicates
                unrealizability of the controller synthesis
                problem. Given an infeasible STL synthesis
                problem, we present algorithms that provide
                feedback on the reasons for unrealizability, and
                suggestions for making it realizable. Our
                algorithms are sound and complete, i. e., they
                provide a correct diagnosis, and always terminate
                with a non-trivial speci cation that is feasible
                using the chosen synthesis method, when such a
                solution exists. We demonstrate the eectiveness
                of our approach on the synthesis of controllers
                for various cyber-physical systems, including an
                autonomous driving application and an aircraft
                electric power system.},
      URL = {http://terraswarm.org/pubs/736.html}
  }
  

Posted by Elizabeth Coyne on 8 Feb 2016.
Groups: tools