The rapid advance of deep reinforcement learning techniques enables the
oversight of safety-critical systems through the utilization of Deep Neural
Networks (DNNs). This underscores the pressing need to promptly establish
certified safety guarantees for such DNN-controlled systems. Most of the
existing verification approaches rely on qualitative approaches, predominantly
employing reachability analysis. However, qualitative verification proves
inadequate for DNN-controlled systems as their behaviors exhibit stochastic
tendencies when operating in open and adversarial environments. In this paper,
we propose a novel framework for unifying both qualitative and quantitative
safety verification problems of DNN-controlled systems. This is achieved by
formulating the verification tasks as the synthesis of valid neural barrier
certificates (NBCs). Initially, the framework seeks to establish almost-sure
safety guarantees through qualitative verification. In cases where qualitative
verification fails, our quantitative verification method is invoked, yielding
precise lower and upper bounds on probabilistic safety across both infinite and
finite time horizons. To facilitate the synthesis of NBCs, we introduce their
$k$-inductive variants. We also devise a simulation-guided approach for
training NBCs, aiming to achieve tightness in computing precise certified lower
and upper bounds. We prototype our approach into a tool called $\textsf{UniQQ}$
and showcase its efficacy on four classic DNN-controlled systems.

通过定性和定量安全性验证问题的综合合成有效的神经屏障证书，本文提出了一种用于 DNN 控制系统的新型框架，并通过 $	extsf {UniQQ}$ 工具在四个经典 DNN 控制系统上展示了其有效性。