Unifying Qualitative and Quantitative Safety Verification of
  DNN-Controlled Systems
Dapeng Zhi Peixin Wang Si Liu Luke Ong Min Zhang
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.