Automated (AI-based) Verification and Control of Large-Scale Stochastic Cyber-Physical Systems
 

In the near future, we expect to see fully autonomous vehicles, aircrafts, robots, and software, all of which should be able to make their own decisions without direct human involvement. Although this technology theme 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 such systems in a formal as well as time- and cost-effective way is the main challenge in the study of those complex systems. Over the past one decade, a number of advances has been made in developing various techniques for autonomous vehicles, especially in the areas of perception, planning, and control. Those techniques have relied on methods from artificial intelligence (AI), machine learning, control theory, and optimization. While, at least in relatively controlled environments, autonomous vehicles 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).

The tight interaction of computational systems with the physical world, known as Cyber-Physical Systems (CPSs), is believed to carry great promises for the competitiveness of many safety-critical industries. Examples of such applications include aerospace, automotive, transportation systems, robotics, chemical process, critical infrastructure, energy, healthcare, etc. Within CPSs, embedded control software plays a significant role by monitoring and adjusting several physical variables through feedback loops where physical processes affect computation and vice versa. Although CPSs have become ubiquitous in modern technology due to advances in computational devices, their designs are still based on ad-hoc solutions trying to make the connection between the classical techniques of control theory and embedded systems engineering. In order to detect and eliminate design flaws and inevitable software bugs, a large portion of the design budget is consumed with validation and verification efforts. On the other hand, by changing the emphasis from verification to design, it is possible to synthesize correct-by-design embedded control software for CPSs while providing formal guarantees of correctness and preventing the need for costly post facto verifications.

Models of CPSs are inherently heterogeneous: discrete systems modeling computational parts and continuous dynamics modeling 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 CPSs. Since the complexity induced by the aforementioned interaction often makes it difficult to obtain analytical results, the verification and policy synthesis for CPSs are often addressed by methods of (in)finite abstractions. More precisely, since the closed-form characterization of synthesized policies for (stochastic) CPSs is not available in general, a suitable approach is to approximate original (concrete) models by simpler ones with possibly lower dimensional (infinite abstractions) or finite state spaces (finite abstractions). A crucial step is to provide formal guarantees during this approximation phase such that the analysis or synthesis on abstract models can be refined back over original ones. When an abstraction with a finite number of states or symbols is available, the synthesis of the controllers can be reduced to either a fixed-point computation over the finite-state abstraction (in the deterministic case) or a value iteration via standard dynamic programming (in the stochastic setting). Moreover, by leveraging computational tools developed for discrete-event systems and games on automata in Computer Science community, one can synthesize controllers satisfying complex specifications which are difficult (if not impossible) to be enforced with classical control design approaches. Examples of such high-level specification classes include logic specifications expressed by linear temporal logic (LTL) formulae such as safety, reachability, reach-avoid, etc.

In order to make the approaches provided by (in)finite abstractions applicable to networks of interacting systems, compositional abstraction-based techniques are proposed in the past few years. In particular, construction of (in)finite abstractions for large-scale stochastic CPSs 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 Infinite Abstractions (Model Order Reduction)

Computational complexity in synthesizing controllers for stochastic CPSs can be alleviated via abstractions in two consecutive stages. In the first stage, original systems can be abstracted by simpler ones with lower dimensions (model order reductions). Then one can employ infinite abstractions as a replacement of original systems, perform analysis and synthesis 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.

Compositional Finite Abstractions (Finite Markov Decision Processes)

Construction of finite abstractions was introduced in recent years as a promising method to reduce the complexity of controller synthesis problems in particular for enforcing complex logical properties. 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 the final abstractions are finite, algorithmic machineries from computer science community are applicable to synthesize controllers over concrete systems enforcing high-level logic properties including safety, reachability, reach-avoid, etc.

Compositional Control Barrier Certificates

Although the proposed compositional techniques in the setting of (in)finite abstractions can mitigate the effects of the state-explosion problem, these approaches still rely on the discretization of the state space of complex networks. In addition, some given dynamics may not be decomposable to very low-dimensional subsystems and the curse of dimensionality problem may exist even in smaller subsystems. These challenges motivate the need to employ some discretization-free approaches using control barrier certificates. In particular, one potential direction to mitigate the computational complexity is to develop the compositional construction of control barrier certificates for temporal logic verification and synthesis of large-scale stochastic CPSs.

Safe AI-based Techniques for Complex Control Missions

Although AI-based techniques have been becoming a promising approach to synthesize controllers for cyber-physical systems enforcing complex control missions, 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 researcline is to formalize this kind of AI-based controllers via the existing tools in formal methods and optimizations.

Model-Free Reinforcement Learning

In order to employ the proposed compositional approaches based on finite abstractions, one needs to know precise models of continuous-space MDPs to construct those finite abstractions and hence are not applicable in the setting where transition structure is unknown. Then one promising direction for the formal controller synthesis of unknown continuous-space MDPs is to employ model-free reinforcement learning approaches and abstract subsystems with finite MDPs with unknown transition probabilities, synthesize strategies over abstract models, and then map the results back over the concrete continuous-space models. Accordingly, one needs to leverage the classical convergence results for reinforcement learning on finite MDPs and propose control strategies maximizing the probability of satisfaction over unknown continuous-space MDPs while providing probabilistic closeness guarantees.

Data-Driven Optimization

Most of the existing works on the temporal logic verification and synthesis of dynamical systems is model-based, whereas in many contexts, e.g., CPSs, a model can be partially unknown. In other words, closed-form models for many complex and heterogeneous systems are either complex or even not available, and hence one cannot employ model-based techniques to analyze this type of complex systems. Although there are some identification approaches available in the relevant literature, acquiring an accurate model for complex systems is always very challenging, time consuming and expensive. Then the presence of data-driven optimization techniques is crucial to bypass the system identification phase and directly employ system measurements for the control analysis. In particular, one potential direction for the temporal logic verification and synthesis of unknown dynamical systems is to leverage scenario optimization techniques for data-driven temporal logic analysis of unknown nonlinear stochastic systems via construction of Lyapunov or barrier functions from any given random set of observations.

Advanced Software Developments in “C++/Python”

Developing efficient software tools (preferably with real-time implementations) based on the proposed theoretical results is always essential for automated verification and synthesis of large-scale stochastic cyber-physical systems.