@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@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.},
}