Diagnosis and repair for synthesis from signal temporal logic specifications

DOI10.1145/2883817.2883847zbMATH Open1366.68169DBLPconf/hybrid/GhoshSNRDSSS16arXiv1602.01883OpenAlexW2256658272WikidataQ57380127 ScholiaQ57380127MaRDI QIDQ2988959FDOQ2988959

Authors: Shromona Ghosh, Dorsa Sadigh, Pierluigi Nuzzo, Vasumathi Raman, Alexandre Donzé, Sanjit A. Seshia, Alberto L. Sangiovanni-Vincentelli, S. Shankar Sastry 

Publication date: 19 May 2017

Published in: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control (Search for Journal in Brave)

Abstract: We address the problem of diagnosing and repairing specifications 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 specification that is feasible using the chosen synthesis method, when such a solution exists. We demonstrate the effectiveness of our approach on the synthesis of controllers for various cyber-physical systems, including an autonomous driving application and an aircraft electric power system.

Full work available at URL: https://arxiv.org/abs/1602.01883

Recommendations

• Reactive synthesis from signal temporal logic specifications
• Duality-based nested controller synthesis from STL specifications for stochastic linear systems
• Reactive synthesis with maximum realizability of linear temporal logic specifications
• Formal controller synthesis from specifications given by discrete-time hybrid automata
• Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications

zbMATH Keywords

synthesishybrid systemsdiagnosisrepairsignal temporal logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Synthesis problems (93B50) Automated systems (robots, etc.) in control theory (93C85)

Cited In (6)

• Robust control for signal temporal logic specifications using discrete average space robustness
• Introspective perception for mobile robots
• Monitoring of perception systems: deterministic, probabilistic, and learning-based fault detection and identification
• Funnel control for fully actuated systems under a fragment of signal temporal logic specifications
• Extracting counterexamples induced by safety violation in linear hybrid systems
• Automated repair for timed systems

This page was built for publication: Diagnosis and repair for synthesis from signal temporal logic specifications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2988959)