Control Synthesis with Temporal Logic

Signal Temporal Logic (STL) is widely used for specifying complex time-dependent behaviors in cyber-physical systems (CPSs), particularly in safety-critical domains. However, fault diagnosis (FD) and fault tolerant control (FTC) under nested STL (NSTL) specifications remain challenging, especially for nonlinear systems. This paper proposes a collaborative design (CoD) framework that jointly integrates FD and FTC under NSTL constraints to enhance detection accuracy and ensure robust system performance. First, a fault detection observer is developed by constructing fault tolerant feasible sets that can predict whether ongoing system trajectories satisfy NSTL specifications. To address the feasibility issue in real-time control synthesis, we introduce the concept of fault tolerant control with recursive feasibility (FTCRF), enabling the controller to maintain constraint satisfaction and system stability even under faults. A model predictive control scheme guided by control barrier functions (CBFs) ensures safe trajectory tracking within specified bounds. Simulation studies on single integrator and unicycle models demonstrate the effectiveness of the proposed method in accurately detecting faults and maintaining task satisfaction under NSTL constraints. Note to Practitioners—This work is motivated by the need for robust fault management in safety-critical cyber-physical systems such as autonomous vehicles, smart manufacturing systems, and robotic healthcare platforms. In these environments, rapid and accurate fault diagnosis—alongside continued safe operation despite faults—is essential to prevent downtime and maintain system integrity. Our proposed framework provides a practical methodology to jointly design fault detection and control strategies, explicitly accounting for complex temporal task constraints specified using nested Signal Temporal Logic. The key contribution is the collaborative integration of a fault diagnosis observer with a fault tolerant controller based on recursive feasibility, ensuring that the system can continue operating safely even when faults occur. Moreover, the use of STL Trees (STLTs) provides a tractable means of reasoning over complex time-based specifications. Practitioners can adopt this framework to improve system reliability, reduce intervention costs, and ensure compliance with temporal task requirements in dynamic and uncertain environments.

We study control synthesis for uncertain systems subject to nested STL tasks and propose a decomposition-based MPC framework. The method resolves nested specifications into atomic subtasks and combines them with distributed shrinking-horizon MPC to improve tractability and control performance under bounded disturbances.

We study control/physical co-design for LPV systems with spectral temporal logic specifications. By transforming spectral-temporal requirements into mixed-integer matrix inequality constraints, the paper develops an iterative optimization framework and demonstrates its effectiveness on MEMS applications.