Certifying the Intersection of Reach Sets of Integrator Agents with Set-valued Input Uncertainties

TL;DR

This paper addresses safety verification of integrator agents with set-valued uncertainties by formulating the problem as a support function minimization, enabling computationally tractable and distributed certification methods.

Contribution

It introduces a novel variational approach to certify reach set intersections for agents with complex input uncertainties, including hyperrectangular cases.

Findings

Support function minimization effectively certifies reach set intersections.

Distributed certification is feasible via second order cone programming.

The approach handles time-varying and hyperrectangular uncertainties.

Abstract

We consider the problem of verifying safety for a pair of identical integrator agents in continuous time with compact set-valued input uncertainties. We encode this verification problem as that of certifying or falsifying the intersection of their reach sets. We transcribe the same into a variational problem, namely that of minimizing the support function of the difference of the two reach sets over the unit sphere. We illustrate the computational tractability of the proposed formulation by developing two cases in detail, viz. when the inputs have time-varying norm-bounded and generic hyperrectangular uncertainties. We show that the latter case allows distributed certification via second order cone programming.