Research Highlights
Research Highlights
There are many complex cyber-physical systems where the precise model description can not be derived analytically and therefore one cannot use model-based techniques in these situations. This makes verification and synthesis problems ensuring reach complex specifications more challenging. In such cases, due to advances in sensor and processing technologies, one can take advantage of data-driven approaches from machine learning to address these problems. Here, we aim to provide probabilistic guarantees that the system trajectories of unknown dynamical systems satisfying complex specifications.
Barrier functions play the analogous role for safety to that of Lyapunov functions for stability. Such functions have the potential to alleviate the issue of 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).
As the complexity of constructing symbolic models grows exponentially in the number of state variables in the concrete system, the existing monolithic approaches on the construction of discrete abstractions are unfortunately limited to only low-dimensional control systems. Motivated by the above limitation, we currently aim at proposing a compositional framework for constructing symbolic models for interconnected control systems. Our methodology is based on a divide-and-conquer scheme. In particular, we first (1) partition the overall concrete system into a number of concrete subsystems and construct discrete abstractions of them individually; (2) then establish a compositional scheme that allows us to construct a discrete abstraction of the overall network using those of individual ones. We also aim at improving computation time required for synthesis of controllers by leveraging compositional abstractions.
The conventional finite abstraction based synthesis techniques suffer from the issue of the curse of dimensionality (i.e., the computational complexity increases exponentially with respect to the state-space dimensions of the concrete systems). Moreover, these approaches are in general limited to finite dimensional systems. To alleviate these issues one can leverage the state-set discretization-free approach for construction of finite abstractions for incrementally stable systems.
QUEST, for state-set discretization-free synthesis of symbolic controllers.The notion of incremental stability focuses on the convergence of trajectories with respect to each other rather than with respect to an equilibrium point or a fixed trajectory. Considering the advantages of incremental stability property in the construction of symbolic models, our research focuses on providing sufficient conditions and design control strategies enforcing incremental stability property for complex control systems.