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

arXiv: https://arxiv.org/abs/2012.07296 · HTML: https://mlsanity.com/paper/2012.07296/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Dec 2020.

## Built on by (most cited first, 1 of 1)

- [Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics](https://mlsanity.com/paper/2212.00679/) (2022)

## Abstract (arXiv)

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.