Verification and Synthesis of (Stochastic) Hybrid Systems using Barrier Certificates

Barrier certificates help to provide analysis for the safety of different classes of dynamical systems. Barrier certificates play the analogical role for safety to that of Lyapunov functions for stability. Such certificates have the potential to resolve the issue of so-called curse of dimensionality existing in discretization-based techniques (i.e., computational complexity grows exponentially with the dimension of the state set) in formal verification and synthesis of dynamical systems against high-level complex specification.

In recent years, there have been many results providing verification and synthesis for safety properties. In HyConSys lab, we are interested in extending those ideas of utilizing barrier certificate for formal verification and synthesis of (stochastic) hybrid systems against a more general class of high-level specifications (e.g. those expresses in linear temporal logic on finite traces).

The following are a few problems that we are interested to address using (control) barrier certificates:

• verification and synthesis of (stochastic) hybrid systems against high-level specifications.

• compositional verification and synthesis of (stochastic) interconnected systems.

• developing efficient techniques for computation of (control) barrier certificates.

Active lab members

The following lab members are actively working on this topic:

• Pushpak Jagtap

• Mahathi Anand

• Majid Zamani

Related publications

The following publications are related to this topic:

• P. Jagtap, S. Soudjani, and M. Zamani. Formal synthesis of stochastic systems via control barrier certificates. Submitted for publication.

• P. Jagtap, S. Soudjani, and M. Zamani. Temporal logic verification of stochastic systems using barrier certificates. 16th International Symposium on Automated Technology for Verification and Analysis (ATVA), Lecture Notes in Computer Science 11138, pp. 177-193, October 2018.