Compositional Construction of Control Barrier Functions for Continuous-Time Stochastic Hybrid Systems

TL;DR

This paper introduces a compositional method for constructing control barrier functions for stochastic hybrid systems, enabling complex logic enforcement with probabilistic guarantees through systematic synthesis techniques.

Contribution

It presents a novel compositional framework using pseudo-barrier functions and small-gain conditions for interconnected systems, with two systematic methods for synthesis: SOS optimization and CEGIS.

Findings

Successfully applied to a network of 100 nonlinear oscillators

Provided probabilistic guarantees for complex specifications

Demonstrated effectiveness through a Kuramoto network example

Abstract

In this work, we propose a compositional framework for the construction of control barrier functions for networks of continuous-time stochastic hybrid systems enforcing complex logic specifications expressed by finite-state automata. The proposed scheme is based on a notion of so-called pseudo-barrier functions computed for subsystems, by employing which one can synthesize hybrid controllers for interconnected systems enforcing complex specifications over a finite-time horizon. Particularly, we first leverage sufficient small-gain type conditions to compositionally construct control barrier functions for interconnected systems based on the corresponding pseudo-barrier functions computed for subsystems. Then, using the constructed control barrier functions, we provide probabilistic guarantees on the satisfaction of given complex specifications in a bounded time horizon. In this respect, we decompose the given complex specification to simpler reachability tasks based on automata representing the complements of original finite-state automata. We then provide systematic approaches to solve those simpler reachability tasks by computing corresponding pseudo-barrier functions. Two different systematic techniques are provided based on (i) the sum-of-squares (SOS) optimization program and (ii) counter-example guided inductive synthesis (CEGIS) to search for pseudo-barrier functions of subsystems while synthesizing local controllers. We demonstrate the effectiveness of our proposed results by applying them to a fully-interconnected Kuramoto network of 100 nonlinear oscillators with Markovian switching signals.