Conservative Perception Models for Probabilistic Model Checking
Cleaveland, Matthew; Lu, Pengyuan; Sokolsky, Oleg; Lee, Insup; Ruchkin, Ivan
Loading…
Permalink
https://hdl.handle.net/2142/130278
Description
Title
Conservative Perception Models for Probabilistic Model Checking
Author(s)
Cleaveland, Matthew
Lu, Pengyuan
Sokolsky, Oleg
Lee, Insup
Ruchkin, Ivan
Issue Date
2025-09-17
Keyword(s)
Neural perception
Probabilistic model checking
Interval Markov decision process
Abstract
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 the object detector YOLO11 in the CARLA driving simulator.
Publisher
Allerton Conference on Communication, Control, and Computing
Series/Report Name or Number
2025 61st Allerton Conference on Communication, Control, and Computing Proceedings
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
