Diagnosis and repair for synthesis from signal temporal logic specifications

DOI10.1145/2883817.2883847zbMATH Open1366.68169DBLPconf/hybrid/GhoshSNRDSSS16OpenAlexW2256658272WikidataQ57380127 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)

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

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)

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.

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

Cited in

(8)

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

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)