Automated Verification and Synthesis of Large-Scale Stochastic Cyber-Physical Systems

Cyber-physical systems (CPSs) are complex networked models combining both cyber (computation and communication) and physical components, which tightly interact with each other in a feedback loop. In the past few years, stochastic CPSs have received significant attentions as an important modeling framework describing many engineering systems and play significant roles in many real-life applications including traffic networks, transportation systems, power grids, and so on. Most stochastic CPSs are of hybrid nature: discrete dynamics model computation parts including hardware and software, and continuous dynamics model control systems.

Automated verification and policy synthesis for this type of complex models to achieve some high-level specifications, e.g., those expressed as linear temporal logic (LTL) formulae, is inherently very challenging. 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 stochastic CPSs. Consequently, providing automated synthesis of correct-by-design controllers for stochastic CPSs is absolutely crucial in many safety-critical applications such as automated highway driving.

Decomposition and abstraction are introduced as two key tools to alleviate the computational complexity arising in the analysis of large-scale stochastic CPSs. More precisely, since the closed-form characterization of synthesized policies for stochastic CPSs is not available, 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.

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

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 robust optimization techniques for data-driven temporal logic analysis of unknown nonlinear stochastic systems via construction of Lyapunov 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.