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 α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.
@article{arxiv.2409.15448,
title = {Optimization-based Verification of Discrete-time Control Barrier Functions: A Branch-and-Bound Approach},
author = {Erfan Shakhesi and W. P. M. H. Heemels and Alexander Katriniok},
journal= {arXiv preprint arXiv:2409.15448},
year = {2025}
}