Abstraction-based formal synthesis relies on obtaining a finite-state abstraction (or symbolic model) of the original and possibly nonlinear systems. Computational methods, such as graph-based model checking and automaton-guided controller synthesis, are then developed based on the abstraction to verify the system or synthesize controllers with respect to a temporal logic specification. Abstractions enable autonomous decision-making of physical systems to achieve more complex tasks and have received significant success in the past decade. Regardless of heavy state-space discretization and complicated abstraction analysis, formal methods compute with guarantees a set of initial states from which a controller exists to realize the given specification. So far, abstraction-based formal verification and control synthesis for deterministic systems has gained its maturity. Sound and approximately complete finite (not just finite-state) abstractions can be achieved.

However, to determine the "size" of the abstractions for stochastic systems, we need to work on the weak* topology of the solution processes (here, we treat the solutions as functionals rather than absolute continuous functions). The obtained abstractions based on the state-space discretization are essentially a family of "discrete-version" transition kernels of the original systems. However, there are uncountably infinite of them, which is why we name it a "finite-state" abstraction. To prevent a sound stochastic abstraction from generating significant deviation, we perform a completeness analysis. The purpose is to investigate whether such deviations can be reflected in some continuous-state systems with arbitrarily small perturbations when compared to the original concrete systems. By conducting this type of comparison, we aim to release the abstraction from the "virtual" systems and establish a perception that even small deviations would not lead to substantial issues for the original system.

Some key results are summarized below.

1. Robustly Complete Finite-State Abstractions for Verification of Stochastic Systems

Note: The theorem says we can create an abstraction sufficiently "large" to dominate the original system. To measure the size of abstractions, one needs to "release" them from the "virtual" systems and compare them with the original system in terms of the weak* topology. For nonlinear systems, it is inevitable to create a slight deviation.

Each element in the abstraction can formulate a probability law, and when this law acts on some specification, it returns a real number (probability). Given all elements within this abstraction are connected and form a compact space (w.r.t. the weak* topology), the measuring result is a subinterval of [0, 1]. The satisfaction probability of the original system should be within that subinterval.

The work also provides a perspective that when the maximal deviation between elements within the abstraction converges, the measuring result (i.e. the interval of satisfaction probability) also converges to a singleton, which should be the actual satisfaction probability of the original system.

We refer readers with technical interests to the theoretical paper (FORMATS'22).

2. Robustly Complete Finite-State Abstractions for Control Synthesis of Stochastic Systems

A similar result holds for control systems. In addition, given an arbitrarily small prescribed precision, an abstraction always exists to decide whether a control strategy exists for the concrete system to satisfy the probabilistic specification (OJCSYS'23) .

Future Directions

1. Refining Formal Abstractions for Control-Free Discrete-Time Stochastic Systems: It is necessary to develop task and system-oriented adaptive discretization techniques to enhance the computational efficiency of the current scheme. Conducting a comprehensive system-wise analysis and development would greatly enhance the accuracy and efficiency of the existing scheme.

2. Leveraging the current advances to design control synthesis algorithms for complex probabilistic specifications and generate winning sets. This will provide decision-makers with a quantitative guide and feasible solutions within uncertain environments.

3. Formal Abstractions for Continuous-Time Stochastic Systems: This is to bridge the final gap between the continuous environments and symbolic models ready for the verification and control synthesis computation.