# Scenario-based Compositional Verification of Autonomous Systems with Neural Perception

arXiv: https://arxiv.org/abs/2504.20942 · HTML: https://mlsanity.com/paper/2504.20942/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 20 of its 35 references that are in the map.
- First posted on arXiv 29 Apr 2025.

## Builds on (most cited first, 20 of 20)

- [A Survey of Deep Learning Techniques for Autonomous Driving](https://mlsanity.com/paper/1910.07738/) (2019)
- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [Formal Scenario-Based Testing of Autonomous Vehicles: From Simulation to the Real World](https://mlsanity.com/paper/2003.07739/) (2020)
- [Deep Learning for Large-Scale Traffic-Sign Detection and Recognition](https://mlsanity.com/paper/1904.00649/) (2019)
- [Verification of Image-based Neural Network Controllers Using Generative Models](https://mlsanity.com/paper/2105.07091/) (2021)
- [Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI](https://mlsanity.com/paper/2005.07173/) (2020)
- [Verifying Controllers with Convolutional Neural Network-based Perception: A Case for Intelligible, Safe, and Precise Abstractions](https://mlsanity.com/paper/2111.05534/) (2021)
- [NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing](https://mlsanity.com/paper/2203.15841/) (2022)
- [Closed-loop Analysis of Vision-based Autonomous Systems: A Case Study](https://mlsanity.com/paper/2302.04634/) (2023)
- [Scalable Surrogate Verification of Image-based Neural Network Control Systems using Composition and Unrolling](https://mlsanity.com/paper/2405.18554/) (2024)
- [Discrete-Event Controller Synthesis for Autonomous Systems with Deep-Learning Perception Components](https://mlsanity.com/paper/2202.03360/) (2022)
- [Compositional Probabilistic Model Checking with String Diagrams of MDPs](https://mlsanity.com/paper/2307.08765/) (2023)
- [Certified Vision-based State Estimation for Autonomous Landing Systems using Reachability Analysis](https://mlsanity.com/paper/2309.05167/) (2023)
- [Assuring Safety of Vision-Based Swarm Formation Control](https://mlsanity.com/paper/2210.00982/) (2022)
- [Data-Driven Modeling and Verification of Perception-Based Autonomous Systems](https://mlsanity.com/paper/2312.06848/) (2023)
- [Stochastic Assume-Guarantee Contracts for Cyber-Physical System Design Under Probabilistic Requirements](https://mlsanity.com/paper/1705.09316/) (2017)
- [Leveraging Classification Metrics for Quantitative System-Level Analysis with Temporal Logic Specifications](https://mlsanity.com/paper/2105.07343/) (2021)
- [Learning-based Inverse Perception Contracts and Applications](https://mlsanity.com/paper/2309.13515/) (2023)
- [Verification of Neural Network Control Systems in Continuous Time](https://mlsanity.com/paper/2406.00157/) (2024)
- [Refining Perception Contracts: Case Studies in Vision-based Safe Auto-landing](https://mlsanity.com/paper/2311.08652/) (2023)

## Built on by (most cited first, 3 of 3)

- [Conformal Safety Shielding for Imperfect-Perception Agents](https://mlsanity.com/paper/2506.17275/) (2025)
- [Verification of Visual Controllers via Compositional Geometric Transformations](https://mlsanity.com/paper/2507.04523/) (2025)
- [Scenario-Based Compositional Statistical Model Checking for Safety Specifications](https://mlsanity.com/paper/2610.05571/) (2026)

## Abstract (arXiv)

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.