Optimization-based Verification of Discrete-time Control Barrier Functions: A Branch-and-Bound Approach

TL;DR

This paper introduces an optimization-based branch-and-bound algorithm inspired by alpha-BB for verifying discrete-time control barrier functions, ensuring safety in nonlinear systems with or without known control policies.

Contribution

It presents a novel verification method for DTCBFs using optimization, applicable to general nonlinear systems with input constraints, regardless of control policy availability.

Findings

Effective verification of DTCBFs demonstrated on numerical case study

Can falsify candidate DTCBFs by providing counterexamples

Applicable to systems with known or unknown control policies

Abstract

Discrete-time Control Barrier Functions (DTCBFs) form a powerful control theoretic tool to guarantee safety and synthesize safe controllers for discrete-time dynamical systems. In this paper, we provide an optimization-based algorithm, inspired by the $\alpha$BB algorithm, for the verification of a candidate DTCBF, i.e., either verifying a given candidate function as a valid DTCBF or falsifying it by providing a counterexample for a general nonlinear discrete-time system with input constraints. This method is applicable whether a corresponding control policy is known or unknown. We apply our method to a numerical case study to illustrate its efficacy.