Diagnosis and Repair for Synthesis from Signal Temporal Logic Specifications

Shromona Ghosh, Dorsa Sadigh, Pierluigi Nuzzo, Vasumathi Raman, Alexandre Donzé, Alberto L. Sangiovanni-Vincentelli, S. Shankar Sastry, and Sanjit A. Seshia. Diagnosis and Repair for Synthesis from Signal Temporal Logic Specifications. In Proceedings of the 9th International Conference on Hybrid Systems: Computation and Control (HSCC), April 2016.

Download

[pdf] 

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.

BibTeX

@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.},
}