Verification of Uncertain POMDPs Using Barrier Certificates

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 can be carried out computationally by sum-of-squares programming. We illustrate the efficacy of our method by applying it to a Mars rover exploration example.