Scenario-based Compositional Verification of Autonomous Systems with Neural Perception

TL;DR

The paper tackles the challenge of verifying safety for autonomous systems that rely on deep neural networks for perception, where both the perception model size and changing environments hinder traditional verification. It introduces scenario-based probabilistic abstractions that build environment-specific perception models $\alpha_e$, integrates them into a closed-loop DTMC via $\mathcal{M}_e$, and represents scenario sequences with compact summaries $(A,B)$ to enable compositional analysis. The authors develop symbolic forward/backward analyses and novel acceleration rules (Hoare-style and composition-based) to provide bounds on the probability of reaching an error state under arbitrary interleavings of scenarios, without requiring a priori knowledge of the exact environmental sequence. The framework is demonstrated on TaxiNet for airport taxiing and a simulated F1Tenth car with LiDAR observations, showing improved precision over pooled abstractions and substantial scalability compared with non-compositional approaches. Overall, the work delivers a scalable, scenario-driven verification pipeline that couples data-driven probabilistic abstractions with formal reasoning to produce parametric safety guarantees in changing operating conditions.

Abstract

Recent advances in deep learning have enabled the development of autonomous systems that use deep neural networks for perception. Formal verification of these systems is challenging due to the size and complexity of the perception DNNs as well as hard-to-quantify, changing environment conditions. To address these challenges, we propose a probabilistic verification framework for autonomous systems based on the following key concepts: (1) Scenario-based Modeling: We decompose the task (e.g., car navigation) into a composition of scenarios, each representing a different environment condition. (2) Probabilistic Abstractions: For each scenario, we build a compact abstraction of perception based on the DNN's performance on an offline dataset that represents the scenario's environment condition. (3) Symbolic Reasoning and Acceleration: The abstractions enable efficient compositional verification of the autonomous system via symbolic reasoning and a novel acceleration proof rule that bounds the error probability of the system under arbitrary variations of environment conditions. We illustrate our approach on two case studies: an experimental autonomous system that guides airplanes on taxiways using high-dimensional perception DNNs and a simulation model of an F1Tenth autonomous car using LiDAR observations.

Figures (7)

• Figure 1: Components of an autonomous system with DNN-based perception.
• Figure 2: TaxiNet achieves 91.25% accuracy when estimating heading for a bright image dataset but only 53.87% accuracy for a dark image dataset.
• Figure 3: Scenario-based compositional analysis of autonomous systems.
• Figure 4: Each F1Tenth scenario corresponds to a track segment.
• Figure 5: Error probability by initial point distribution for bright;bright and dark scenarios. Initial point distributions that ensure error probability at most $0.305$, $0.05$ and $0.01$ are highlighted in gray, blue, and green, respectively.

Theorems & Definitions (3)

• proof
• proof
• proof