Algebraic Proofs of Path Disconnectedness using Time-Dependent Barrier Functions

TL;DR

The paper tackles certifying path-disconnectedness between two compact sets $X_0$ and $X_1$ within a larger compact set $X$ by formulating the search for a connecting path as a single-integrator optimal control problem and recasting it as an infinite-dimensional LP over occupation measures. It proves that a time-dependent barrier function exists if and only if path-disconnectedness holds under reasonable compactness assumptions, and then computes such barriers via the Moment-SOS hierarchy of semidefinite programs, with control-elimination techniques to reduce complexity. The authors demonstrate the approach on univariate and higher-dimensional examples, showing that SOS relaxations yield certificates of disconnection and offering guidance on computational trade-offs, such as using box inputs to eliminate control variables. This method provides verifiable, certificate-based disconnectedness results that can complement traditional roadmap or sampling-based planners, with potential for scalable, verifiable analysis in robotics and motion planning. Future work includes tightening numerical conditioning, exploring universal disconnection proofs, and extending the framework to unbounded domains and more complex semialgebraic descriptions of the state space.

Abstract

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.

Figures (3)

• Figure 1: Univariate barrier certificate
• Figure 2: Elliptic curve separation contour
• Figure 3: Elliptic curve separation contour (3d)

Theorems & Definitions (31)

• Lemma 2.1: Farkas' Lemma CK77
• Theorem 2.2: Theorem 1 of prajna2005necessity
• Theorem 3.1: Theorem 2.1 of d2003bounds
• proof
• Proposition 3.2
• Proposition 3.3
• proof
• Theorem 4.1
• proof
• Proposition 4.2