Trajectory-guided ellipsoidal abstractions for reach-avoid control : A certification pipeline for nonlinear systems

Details

Supervisors

Jungers, Raphaël M.

Faculty

Ecole polytechnique de Louvain

Degree label

Master [120] : ingénieur civil en mathématiques appliquées, à finalité spécialisée

Abstract

enThis thesis studies reach-avoid control for nonlinear systems, where the objective is to synthesize feedback controllers that drive a set of initial states to a target set while avoiding unsafe states. Abstraction-based control provides a systematic way to obtain formal guarantees, but global symbolic abstractions may become large or conservative. Conversely, trajectory optimization and sampling-based model predictive methods often find useful motions, but their outputs are nominal and do not, by themselves, provide robustness guarantees for the resulting control sequence. The central idea of this thesis is to use nominal trajectories not as certificates, but as guides for constructing local partial abstractions. We formalize this viewpoint through certified local reach-avoid chains: finite sequences of local sets equipped with feedback laws whose robust one-step reachable images are included in the next set. The proposed pipeline first computes a nominal trajectory using a coarse centered abstraction and MPPI refinement, and then attempts to lift it into a chain of ellipsoidal sets with affine feedback laws using a backward LMI-based certifier. The method is implemented in Dionysos.jl and evaluated on nonlinear benchmarks. The experiments show that nontrivial certified behaviours can be obtained, while also identifying key certifiability bottlenecks: local model conservatism, limited feedback authority near input saturation, numerical conditioning, and insufficient geometric clearance. Overall, the thesis proposes a task-oriented alternative to monolithic abstraction construction: certify relevant behaviours locally, while preserving the soundness of abstraction-based control.