Verification of Uncertain POMDPs Using Barrier Certificates
Mohamadreza Ahmadi, Murat Cubuktepe, Nils Jansen, and Ufuk Topcu

TL;DR
This paper introduces a novel verification method for uncertain POMDPs using barrier certificates and sum-of-squares programming, enabling safety and performance guarantees for autonomous systems with uncertain dynamics.
Contribution
It proposes a new approach to verify uncertain POMDPs by transforming them into switched systems and applying barrier certificates, which is computationally feasible via sum-of-squares programming.
Findings
Effective verification of uncertain POMDPs demonstrated on Mars rover example
Method ensures safety and optimality under probability interval uncertainties
Verification process is computationally tractable using sum-of-squares programming
Abstract
We consider a class of partially observable Markov decision processes (POMDPs) with uncertain transition and/or observation probabilities. The uncertainty takes the form of probability intervals. Such uncertain POMDPs can be used, for example, to model autonomous agents with sensors with limited accuracy, or agents undergoing a sudden component failure, or structural damage [1]. Given an uncertain POMDP representation of the autonomous agent, our goal is to propose a method for checking whether the system will satisfy an optimal performance, while not violating a safety requirement (e.g. fuel level, velocity, and etc.). To this end, we cast the POMDP problem into a switched system scenario. We then take advantage of this switched system characterization and propose a method based on barrier certificates for optimality and/or safety verification. We then show that the verification task…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Fault Detection and Control Systems · Bayesian Modeling and Causal Inference
