THIS REPORT HAS BEEN WITHDRAWN

Alberto Alessandro Angelo Puggelli, Wenchao Li, John Finn, Alberto L. Sangiovanni-Vincentelli and Sanjit A. Seshia

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2012-117
May 24, 2012

We address the problem of verifying PCTL properties of Markov Decision Processes whose state transition probabilities are only known to lie within uncertainty sets. Using results from convex theory and duality, we propose a suite of verification algorithms and prove their soundness, completeness and termination when arbitrary convex models of uncertainty are considered. Furthermore, soundness and termination can also be guaranteed when non-convex models of uncertainty are adopted. We validate the proposed approach on two case studies: the verification of a consensus protocol when one of the processes behaves erroneously and the dining philosopher problem.