Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences

COLLEGE OF ENGINEERING

UC Berkeley

Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties

THIS REPORT HAS BEEN WITHDRAWN

Alberto Alessandro Angelo Puggelli

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2014-27
April 4, 2014

We address the problem of verifying Probabilistic Computation Tree Logic (PCTL) properties of Markov Decision Processes (MDPs) whose state transition probabilities are only known to lie within uncertainty sets. We first introduce the model of Convex-MDPs (CMDPs), i.e., MDPs with convex uncertainty sets. CMDPs generalize Interval-MDPs (IMDPs) by allowing also more expressive (convex) descriptions of uncertainty. Using results on strong duality for convex programs, we then present a PCTL verification algorithm for CMDPs, and prove that it runs in time polynomial in the size of a CMDP. This result allows us to lower the previously known algorithmic complexity upper bound for IMDPs from co-NP to PTIME, and it is valid also for more expressive (convex) uncertainty models. We validate the proposed approach on two case studies: the verification of a consensus protocol and of a dynamic configuration protocol for IPv4 addresses. A concise version of the results presented in this thesis can be found in: A. Puggelli, W. Li, A. L. Sangiovanni-Vincentelli, S. A. Seshia, Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties, Computer Aided Verification, 2013.

Advisor: Alberto L. Sangiovanni-Vincentelli and Elad Alon