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.

Highlights of the proposed results include:

• We propose the synthesis of unknown dynamical systems by utilizing the notions of control barrier functions and Gaussian process models.

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).

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.

Related Publications:

• P. Jagtap, S. Soudjani, and M. Zamani, "Formal Synthesis of Stochastic Systems via Control Barrier Certificates," IEEE Transactions on Automatic Control, conditionally accepted. [pdf]
• N. Jahanshahi*, P. Jagtap*, and M. Zamani, "Synthesis of Stochastic Systems with Partial Information via Control Barrier Functions," 21st IFAC World Congress, 2020, to appear.
• P. Jagtap*, A. Swikir*, and M. Zamani, "Compositional Construction of Control Barrier Functions for Interconnected Control Systems," 23rd ACM International Conference on Hybrid Systems: Computation and Control (HSCC), 2020, to appear. [pdf]
• M. Anand*, P. Jagtap*, and M. Zamani, "Verification of Switched Stochastic Systems via Barrier Certificates," IEEE Conference on Decision and Control (CDC), 2019, to appear.
• P. Jagtap, S. Soudjani, and M. Zamani, "Temporal Logic Verification of Stochastic Systems using Barrier Certificates," Automated Technology for Verification and Analysis (ATVA), Los Angeles, CA, Lecture Notes in Computer Science 11138, pp 177-193, Springer, 2018. [Link][pdf]

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.

Highlights of the proposed results include:

• We propose the notion of approximate composition which allow us to use different types abstractions for each subsystem.
• We provide compositional construction of abstractions by utilizing the notion of approximate composition.
• We develop an incremental procedure for controller synthesis which helps to reduce the computational complexity while ensuring completeness with respect to the monolithic synthesis.

Related publications:

• A. Saoud*, P. Jagtap*, M. Zamani, and A. Girard, "Compositional Abstraction and Controller Synthesis for Interconnected Systems: An Approximate Composition Approach," Submitted for publication. [pdf]
• A. Saoud*, P. Jagtap*, M. Zamani, and A. Girard, "Compositional Abstraction-Based Synthesis for Cascade Discrete-Time Control Systems," IFAC Conference on Analysis and Design of Hybrid Systems (ADHS), Oxford, UK, pp. 13-18, 2018. [Link][pdf]

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.

Highlights of the proposed results include:

• We provide a systematic approach for construction of state-set discretization-free finite abstractions for a class of infinite dimensional systems.
• We develop an open source toolbox (in C++), called QUEST, for state-set discretization-free synthesis of symbolic controllers.

Related publications:

• P. Jagtap and M. Zamani, "Symbolic Models for Retarded Jump-Diffusion System," Automatica, 2019. [Link][pdf]
• P. Jagtap and M. Zamani, "QUEST: A Tool for State-Space Quantization-free Synthesis of Symbolic Controllers," 14th International Conference on Quantitative Evaluation of SysTems (QEST), Lecture Notes in Computer Science 10503, pp 309-313, Springer, 2017. [Link]

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.

Highlight of the proposed results include:

• We proposed a coordinate invariant notion of incremental stability for stochastic control systems.
• We proposed a backstepping controller design for stochastic Hamiltonian systems with jumps.
• We introduce a notion of incremental stability for retarded jump-diffusion systems and provide sufficient conditions for it in terms of the existence of a notion of incremental Lyapunov functions.

Related Publications:

• P. Jagtap and M. Zamani, "Symbolic Models for Retarded Jump-Diffusion System," Automatica, 2019. [Link][pdf]
• P. Jagtap and M. Zamani, "Backstepping Design for Incremental Stability of Stochastic Hamiltonian Systems with Jumps," IEEE Transactions on Automatic Control, vol. 63, no. 1, pp. 255-261, 2018. [Link] [pdf]
• P. Jagtap and M. Zamani, "On Incremental Stability of Time-Delayed Stochastic Control Systems," The 54th Annual Allerton Conference on Communication, Control, and Computing, Monticello, IL, USA, pp. 577-581, 2016. [Link]
• P. Jagtap and M. Zamani, "Backstepping Design for Incremental Stability of Stochastic Hamiltonian Systems," The 55th IEEE Conference on Decision and Control (CDC), Las Vegas, USA, pp. 5367-5372, 2016. [Link]