Article Highlight | 9-Nov-2025

Model predictive control for on-orbit inspection mission with signal temporal logic specifications

Shanghai Jiao Tong University Journal Center

Shanghai Jiao Tong University Research Team Develops Model Predictive Control with Signal Temporal Logic for On-Orbit Inspection Missions

Thermal management has always been a critical challenge for high-power-density devices and components. Similarly, in the field of aerospace, the control of small satellites for on-orbit inspection missions faces multiple complex constraints and precise task requirements. Model Predictive Control (MPC), with its ability to handle constraints and optimize performance, shows great potential. However, traditional control methods struggle with complex spatiotemporal task specifications and high computational complexity, limiting their application. The introduction of Signal Temporal Logic (STL) provides a formal language to precisely describe task specifications with temporal constraints, while the novel auxiliary function design and optimized terminal parameter calculation significantly enhance the feasibility and efficiency of the MPC algorithm.

Highlights of this Research:

An STL-based MPC algorithm is developed for small satellite on-orbit inspection missions, effectively handling multiple constraints including input saturation, obstacle avoidance, and velocity limits.

 

The auxiliary function is innovatively designed as a cubic power function, considering the impact of input saturation and aligning better with the actual behavior of the satellite's robust function.

 

The number of constraints in the terminal parameter calculation is significantly reduced via Linear Matrix Inequality techniques, greatly improving computational efficiency.

Summary:
A research team from Shanghai Jiao Tong University has proposed a novel Model Predictive Control (MPC) algorithm integrated with Signal Temporal Logic (STL) specifications for small satellites performing on-orbit inspection missions. The relative dynamics of the satellite are modeled using the Clohessy-Wiltshire equations. The algorithm comprehensively considers practical constraints such as thruster input saturation, obstacle avoidance (modeling the target spacecraft as an obstacle with safety regions), and velocity limits.

The core innovation lies in transforming complex temporal logic task specifications (e.g., "visit region A between time t1 and t2 and stay there for duration D") into constraints manageable by MPC. This is achieved by designing a non-decreasing auxiliary function based on the robust semantics of STL. Unlike previous exponential auxiliary functions, the team designed a cubic power function auxiliary function, which more accurately reflects the satellite's velocity change trends under input saturation (slow initial acceleration, followed by increase, and final deceleration), thereby enhancing the feasibility of the optimization problem.

Furthermore, the team designed the terminal ingredients (terminal cost, terminal control law, and terminal set) crucial for ensuring MPC stability and recursive feasibility. By leveraging Linear Matrix Inequality (LMI) techniques, the parameters for the terminal set and control law are computed efficiently. Compared to existing methods where the number of LMI constraints depends on the total mission duration, this new approach drastically reduces the number of constraints, leading to significantly faster offline/online computation times for terminal parameters.

Simulation results demonstrate the effectiveness of the proposed algorithm. The satellite successfully navigates through multiple predefined target regions within specified time windows while adhering to all safety and physical constraints. Comparisons with an existing MPC method using exponential auxiliary functions show that the cubic function aligns better with the actual robust function, reducing potential infeasibility. While the inclusion of slack variables as optimization variables slightly increases the MPC solve time compared to using a fixed upper bound, the difference is minimal (~0.05s). More notably, comparisons with Mixed-Integer Linear Programming (MILP) based STL methods reveal that the proposed algorithm is less conservative (can handle nonlinear constraints like spherical regions directly) and solves the optimization problem much faster due to avoiding numerous binary variables.

Research Context and Application Potential
With the advancement of small satellite technology, on-orbit inspection services are garnering significant attention. These missions require satellites to perform multi-position patrols around large target spacecraft (like space stations or other satellites) to gather comprehensive information. This research addresses the critical need for guaranteeing complex, time-bound task completion under multiple stringent constraints, paving the way for more reliable and autonomous on-orbit servicing and inspection.

The proposed STL-based MPC framework offers a powerful and computationally efficient tool for planning and controlling complex robotic missions beyond on-orbit inspection, potentially extending to areas like autonomous vehicles, multi-robot systems, and industrial automation where temporal logic specifications are essential.

Disclaimer: AAAS and EurekAlert! are not responsible for the accuracy of news releases posted to EurekAlert! by contributing institutions or for the use of any information through the EurekAlert system.