@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@inproceedings{ghosh-hscc16,
author    = {Shromona Ghosh and
               Dorsa Sadigh and
               Pierluigi Nuzzo and
               Vasumathi Raman and
               Alexandre Donz{\'{e}} and
               Alberto L. Sangiovanni{-}Vincentelli and
               S. Shankar Sastry and
               Sanjit A. Seshia},
  title     = {Diagnosis and Repair for Synthesis from Signal Temporal Logic Specifications},
 booktitle = {Proceedings of the 9th International Conference on Hybrid Systems: Computation and Control (HSCC)},
 month = "April",
 year = {2016},
 OPTpages = {239--248},
 abstract = {We address the problem of diagnosing and repairing specifications 
for hybrid systems, formalized in signal temporal logic (STL). 
Our focus is on automatic synthesis of controllers from specifications using 
model predictive control. 
We build on recent approaches that reduce the controller 
synthesis problem to solving one or more mixed integer linear programs 
(MILPs), where infeasibility of an 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 diagnosis that makes the synthesis problem infeasible,  
and always terminate with a non-trivial specification that 
is feasible using the chosen synthesis method, when such a solution 
exists. We demonstrate the effectiveness of our approach on controller  
synthesis for various cyber-physical systems, including an 
autonomous driving application and an aircraft 
electric power system.},
}