Formal Verification, Learning and Control of Large-Scale Stochastic Cyber-Physical Systems

In the past few years, large-scale stochastic cyber-physical systems (CPS) have received remarkable attentions as a beneficial modeling framework describing a wide range of real-life safety-critical systems including automotive, robotics, transportation systems, energy, healthcare, critical infrastructures, and so on. Formal verification and policy synthesis for this type of complex systems to enforce high-level logic properties, e.g., those expressed as linear temporal logic (LTL) formulae, are inherently very challenging mainly due to (i) large dimension of state/input sets, (ii) stochastic nature of dynamics, (iii) tight interaction between physical and cyber components, (iv) dealing with complex logic requirements, and (v) lack of mathematical closed-form models in many real-world applications. My line of research mainly focuses on developing different compositional (AI-based) techniques to tackle the aforementioned difficulties and design highly-reliable CPS by bringing together interdisciplinary concepts from formal methods in computer science, control theory, data science and machine learning.

Compositional Abstraction-based Techniques

Models of CPS are inherently heterogeneous: discrete systems modelling computational parts and continuous dynamics modelling physical processes. In particular, the ability to handle the interaction between continuous and discrete dynamics is a prerequisite for providing a rigorous formal framework for the automated verification and synthesis of CPS. Since the complexity induced by the aforementioned interaction often makes it difficult to obtain analytical results, the verification and policy synthesis for CPS are often addressed by methods of (in)finite abstractions. 

  • Infinite Abstractions (Reduced-order Models). In the first stage, original systems can be abstracted by simpler ones with lower dimensions using model order reduction techniques. Then one can employ infinite abstractions as a replacement of original systems, perform formal analysis over abstract models, and finally carry the results back (via an interface map) over concrete systems. Since the mismatch between outputs of original systems and those of their infinite abstractions are well-quantified, one can guarantee that concrete systems also satisfy the same specifications as abstract ones with guaranteed error bounds.

  • Finite Abstractions (Finite Markov Decision Processes). In the second phase of the abstract procedure, one can construct finite abstractions (a.k.a., finite Markov decision processes (MDPs)) as approximate descriptions of (reduced-order) systems in which each discrete state corresponds to a collection of continuous states of (reduced-order) systems. Since final abstractions are finite, algorithmic machineries from computer science literature are applicable to synthesize controllers over concrete systems enforcing high-level logic properties.

  • Compositional Abstraction-based Techniques. In order to make the approaches provided by (in)finite abstractions applicable to networks of interacting systems, compositional abstraction-based techniques have been proposed in the past few years. In particular, construction of (in)finite abstractions for large-scale stochastic CPS in a monolithic manner suffers severely from the so-called curse of dimensionality: the complexity exponentially grows as the number of state variables increases. To mitigate this issue, one promising solution is to consider the large-scale complex system as an interconnected system composed of several smaller subsystems, and provide a compositional framework for the construction of (in)finite abstractions for the given interconnected system using abstractions of smaller subsystems.

Compositional Control Barrier Certificates

Another promising approach for the formal analysis of CPS is to employ control barrier certificates (CBC), as a discretization-free approach. Intuitively speaking, barrier certificates are Lyapunov-like functions defined over the state space of the system to enforce a set of inequalities on both the function itself and the one-step transition (or the infinitesimal generator along the flow) of the system. An appropriate level set of a barrier certificate can separate an unsafe region from all system trajectories starting from a given set of initial conditions. Consequently, the existence of such a function provides a formal probabilistic certificate fo safety of the system. On the downside, finding CBC for complex CPS is computationally very expensive, especially if the dimension of underlying systems is high. This main challenge motivates a need to develop compositional techniques for the construction of CBC for large-scale stochastic CPS based on local CBC of smaller subsystems.

Data-Driven Analysis of CPS with Provable Guarantees

Although the proposed approaches on (in)finite abstractions and barrier certificates have been promising, they require knowing precise models of the systems; and hence, those approaches are not applicable when the model is unknown. In particular, closed-form models for many physical CPS are either not available or too complex to be of any practical use and one cannot employ model-based techniques to analyze those complex systems. Although there are some results in the relevant literature to provide analysis frameworks for unknown CPS by learning approximate models utilizing identification approaches, obtaining an accurate model is always very challenging, time-consuming, and expensive, especially when the underlying dynamics are too complex which is the case in many real-world applications. This critical challenge motivates a need to bypass the system identification phase and develop a direct data-driven approach to analyze underling CPS by collecting finite data from trajectories of unknown CPS.

Safe Autonomy & AI for Safety-critical CPS

AI-based techniques have been becoming a promising approach to synthesize controllers for CPS enforcing complex control missions; however, guaranteeing safety and reliability of physical systems with this kind of controllers is currently very challenging, which is of vital importance in many real-life safety-critical applications. One potential research line is to formalize this kind of AI-based controllers via the existing tools in formal methods and machine learning.

  • Model-Free (Two-Player) Reinforcement Learning. In order to employ the proposed compositional approaches based on finite abstractions, one needs to know precise models of continuous-space MDPs. One promising approach for formal controller synthesis of continuous-space MDPs with unknown dynamics is to employ model-free two-player reinforcement learning (RL) in an assume-guarantee fashion and compositionally computes strategies for continuous-space interconnected systems without explicitly constructing their finite-state abstractions. In particular, the proposed approach is based on implicitly abstracting each subsystem in the network with a finite MDP with unknown transition probabilities, synthesizing a strategy for each abstract model in an assume-guarantee fashion using RL, and then mapping the results back over the network while providing approximate optimality guarantees. Accordingly, a guaranteed lower bound for the probability of property satisfaction by the interconnected system is provided based on those of individual controllers over subsystems. A key contribution is to leverage the classical convergence results for two-player stochastic games RL on finite models and provide control strategies maximizing the probability of satisfaction over networks of unknown continuous-space systems.

  • Safety Advisor-Supervisor (Safe-Visor) Architecture. Another way of formalizing the AI-based controllers is to develop a Safe-visor architecture for sandboxing unverified controllers over CPS operating in noisy environments. The proposed architecture can contain a history-based supervisor, which checks inputs from the unverified controller and makes a compromise between functionality and safety of the system, and a safety advisor that provides fallback when the unverified controller endangers the safety of the system. By employing this architecture, one can provide formal probabilistic guarantees on preserving the safety of the system. Accordingly, unverified controllers can still be employed in the control loop even though they are not reliable.

Trustworthy AI for Autonomous Vehicles

Autonomy is certainly one of the main themes of the 21st-century technology. In the near future, we expect to see fully autonomous vehicles (AVs), aircrafts, robots, and software, all of which should be able to make their own decisions without direct human involvement. Although this technology theme for AVs provides many potential advantages, e.g., fewer traffic collisions, reduced traffic congestion, increased roadway capacity, relief of vehicle occupants from driving, etc., guaranteeing safety and reliability of AVs in a formal as well as time- and cost-effective way is the main challenge in the study of those complex systems. In particular, while, at least in relatively controlled environments, AVs have been demonstrated to be functioning, they are still not ready to be deployed for regular use. One stumbling block in their deployment is the lack of any guarantee of correctness. In other words, even if such vehicles are extensively tested in varied environments, there is no guarantee that something unforeseen would not happen in a new environment. This in turn opens up several unanswered questions related to liability in the case of accidents or other unforeseen events. While one may, in the unlikely case, even be able to design provably-correct methods for navigation and control in specific scenarios, the moment either the scenario or the specifications of correctness change, a completely new design will be required along with the associated proof of correctness.

Advanced Software Development in “C++/Python/OpenCL”

In order to bridge the gap between academia and industry, one aspect of my research is to develop efficient open-source software tools (preferably with real-time implementations) based on theoretical results for the automated verification and synthesis of large-scale stochastic CPS.