Continuous-Time Planning and Control Synthesis under Temporal Logic Specifications with Applications to Quadrotors

Abstract

Modern robotic systems are increasingly required to perform complex, safety-critical tasks in which system behaviors must be achieved under specified conditions and temporal constraints. Temporal logic provides a formal language for specifying such requirements in a precise and interpretable manner. In this thesis, signal temporal logic (STL) is used for continuous-time trajectory planning with quantitative temporal constraints, while linear temporal logic (LTL) is considered for control synthesis with qualitative task requirements. This thesis focuses on continuous-time planning and control synthesis for robotic systems under temporal logic specifications, with the goal of generating dynamically feasible control strategies that satisfy high-level task requirements.

The first aspect of this thesis considers continuous-time trajectory planning under STL specifications. We represent trajectories using Bézier curves so that the generated plans are continuous in time and possess inherent smoothness properties. Within this trajectory representation, we introduce a time-varying robustness formulation for STL specifications, which replaces the conventional use of a uniform robustness margin over the entire task horizon. The proposed formulation allows different portions of the trajectory to be associated with different robustness requirements, thereby reducing unnecessary conservatism while maintaining satisfaction of the STL specification. This framework connects continuous-time trajectory generation with STL robustness analysis and yields smooth trajectories that are suitable for control execution.

The second aspect of this thesis studies control synthesis for executing trajectories that satisfy STL specifications. Since the closed-loop trajectory may deviate from the planned trajectory, the proposed framework integrates tracking-error bounds into the STL robustness analysis to ensure that specification satisfaction is preserved during execution. In this thesis, quadrotor systems are considered a representative class of high-dimensional nonlinear robotic systems. Geometric controllers on $\mathrm{SE}(3)$ with diagonal matrix gains are developed and analyzed to characterize tracking convergence and execution errors. Compared with controllers using scalar gains, the formulation with diagonal matrix gains yields tighter tracking error bounds, which can be incorporated into the robustness analysis. Building on this framework, the thesis further extends the approach to multi-quadrotor systems by deriving inter-agent safety conditions for STL planning using Bézier curves.

For long-horizon task execution, this thesis develops an abstraction-free LTL control-synthesis framework for continuous-time systems by patching together locally certified control Lyapunov–barrier function (CLBF) solutions. By decomposing temporal-logic specifications into a sequence of safe-stabilization problems, the framework constructs switching feedback controllers that realize the required transitions over continuous-state regions. This enables efficient execution of long-horizon LTL tasks, without requiring the explicit construction of a global symbolic abstraction.

Through numerical simulations and robotic case studies, we demonstrate the effectiveness of the proposed methods for reach-avoid planning, quadrotor trajectory execution, multi-agent coordination, and long-horizon temporal logic tasks. The proposed LTL control synthesis framework is further demonstrated on a Crazyflie platform.