Diagnosis and Repair for Synthesis from Signal Temporal Logic Specifications

TL;DR

This paper introduces algorithms for diagnosing and repairing unrealizable specifications in hybrid systems formalized with signal temporal logic, enhancing controller synthesis in model predictive control frameworks.

Contribution

It presents sound and complete algorithms for diagnosing and repairing unrealizable STL specifications, ensuring feasible controller synthesis when solutions exist.

Findings

Algorithms effectively diagnose unrealizability in STL specifications.

Approach successfully synthesizes controllers for cyber-physical systems.

Demonstrated on autonomous driving and aircraft power systems.

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.