Location
MC 6460
Candidate
Yating Yuan | Applied Mathematics, University of Waterloo
Title
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 as a representative class of high dimensional nonlinear robotic systems. Geometric controllers on 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 considers control synthesis under LTL specifications through an abstraction free framework based on patching control Lyapunov barrier functions (CLBFs). Certified level sets are used to approximate feasible trajectory sets, enabling control synthesis for long horizon LTL specifications while avoiding the construction of full symbolic abstractions.
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 validated on a Crazyflie platform.