Verifying the behaviors of autonomous systems with learned perception components is a challenging problem due to the complexity of the perception and the uncertainty of operating environments. Probabilistic model checking is a powerful tool for providing guarantees on stochastic models of systems. However, constructing model-checkable models of black-box perception components for system-level mathematical guarantees has been an enduring challenge. In this paper, we propose a method for constructing provably conservative Interval Markov Decision Process (IMDP) models of closed-loop systems with perception components. We prove that our technique results in conservative abstractions with a user-specified probability. We evaluate our approach in an automatic braking case study using both a synthetic perception component and the object detector YOLO11 in the CARLA driving simulator.
@article{arxiv.2503.18077,
title = {Conservative Perception Models for Probabilistic Verification},
author = {Matthew Cleaveland and Pengyuan Lu and Oleg Sokolsky and Insup Lee and Ivan Ruchkin},
journal= {arXiv preprint arXiv:2503.18077},
year = {2025}
}