Formal Verification and Synthesis using Barrier Functions

Barrier functions play an analogous role for safety to that of Lyapunov functions for stability. Such functions have the potential to alleviate the issue of the so-called curse of dimensionality (i.e., computational complexity grows exponentially with the dimension of the state set) in formal verification and synthesis of dynamical systems using discretization-based techniques.

In recent years, there have been many results providing verification and synthesis for safety properties. Here, we are interested in extending those ideas of utilizing barrier functions for formal verification and synthesis of (stochastic) hybrid systems against a more general class of high-level specifications (e.g. those expressed in linear temporal logic or (in)finite strings over automata).

Highlights of the proposed results include:

• We provide systematic verification and synthesis of (stochastic) control systems against high-level specifications.
• We proposed a compositional framework for the construction of barrier functions to improve the scalability of approach to large-scale interconnected systems.