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

Alberto Puggelli, Wenchao Li, Alberto Sangiovanni-Vincentelli, and Sanjit A. Seshia. Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties. In Proceedings of the 25th International Conference on Computer-Aided Verification (CAV), July 2013.

Download

[pdf] 

Abstract

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. In addition, we provide an alternative verification procedure based on Value Iteration and experimentally show that it scales better to the verification of larger 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.

BibTeX

@inproceedings{puggelli-cav13,
  author    = {Alberto Puggelli and Wenchao Li and Alberto Sangiovanni-Vincentelli and Sanjit A. Seshia},
  title     = {Polynomial-Time Verification of {PCTL} Properties of {MDP}s with Convex Uncertainties},
 booktitle = {Proceedings of the 25th International Conference on Computer-Aided Verification (CAV)},
 month = "July",
 year = {2013},
 abstract = {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. In addition, we provide 
an alternative verification procedure based on Value Iteration and experimentally 
show that it scales better to the verification of larger 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.},
}