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, machine learning and data science. Compositional Abstraction-based TechniquesModels 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.
Compositional Control Barrier CertificatesAnother 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 GuaranteesAlthough 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 CPSAI-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.
Trustworthy AI for Autonomous VehiclesAutonomy 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. |