Compositional construction of control barrier functions for continuous-time stochastic hybrid systems

• Published in: Automatica (Oxford) 2022-11, Vol.145, p.110513, Article 110513
• Main Authors: Nejati, Ameneh, Soudjani, Sadegh, Zamani, Majid
• Format: Article
• Language: English
• Subjects: Compositional barrier functions; Continuous-time stochastic hybrid systems; Large-scale stochastic systems; Logic specifications; Small-gain reasoning
• ISSN: 0005-1098; 1873-2836
• DOI: 10.1016/j.automatica.2022.110513

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.