Algebraic Proofs of Path Disconnectedness using Time-Dependent Barrier Functions
<|reference_start|>Algebraic Proofs of Path Disconnectedness using Time-Dependent Barrier Functions: Two subsets of a given set are path-disconnected if they lie in different connected components of the larger set. Verification of path-disconnectedness is essential in proving the infeasibility of motion planning and trajectory optimization algorithms. We formulate path-disconnectedness as the infeasibility of a single-integrator control task to move between an initial set and a target set in a sufficiently long time horizon. This control-infeasibility task is certified through the generation of a time-dependent barrier function that separates the initial and final sets. The existence of a time-dependent barrier function is a necessary and sufficient condition for path-disconnectedness under compactness conditions. Numerically, the search for a polynomial barrier function is formulated using the moment-sum-of-squares hierarchy of semidefinite programs. The barrier function proves path-disconnectedness at a sufficiently large polynomial degree. The computational complexity of these semidefinite programs can be reduced by elimination of the control variables. Disconnectedness proofs are synthesized for example systems.<|reference_end|>
@article{henrion2024algebraic,
    title={Algebraic Proofs of Path Disconnectedness using Time-Dependent Barrier
  Functions},
    author={Didier Henrion, Jared Miller, Mohab Safey El Din},
    journal={arXiv preprint arXiv:2404.06985},
    year={2024},
    archivePrefix={arXiv},
    eprint={2404.06985},
    primaryClass={math.OC cs.SY eess.SY}
}