Learning Compositional, Time-Varying Neural Barrier Contracts
Matthew Low, Timothy E. Wang, Pierluigi Nuzzo · Frontiers in artificial intelligence and applications · 2024
Certificate functions can be used to efficiently capture and prove various properties of a system or controller. Control barrier functions (CBFs) are certificate functions that define a region of forward-invariance, which makes them a natural choice to enforce a notion of “safety” for a system. However, synthesizing CBFs, especially in the case of complex systems with learning-enabled components, remains a challenge. Recent work achieves promising results by leveraging neural networks as function approximators to learn CBFs. However, a single CBF may not exist or be difficult to obtain for complex hybrid systems. To overcome this difficulty, this paper presents a framework to simultaneously learn simpler, time-varying control barrier functions (TV-CBFs) that are composable. We embed these neural certificates in a compositional framework based on assume-guarantee contracts. The resulting neural barrier contracts can then be combined by leveraging the rigorous contract algebra. Learning multiple, composable CBFs empowers the verification process (1) by simplifying the verification of complex systems via decomposition and (2) by broadening the expressivity in capturing complex systems and controllers. We illustrate the effectiveness of our approach on the verification of an aircraft’s automatic landing system and a quadrotor navigating an indoor environment.