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 for a rich subclass of convex uncertainty models. This result allows us to lower the previously known algorithmic complexity upper bound for IMDPs from co-NP to PTIME. We demonstrate the practical effectiveness of the proposed approach by verifying a consensus protocol and a dynamic configuration protocol for IPv4 addresses.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Courcoubetis, C., Yannakakis, M.: The Complexity of Probabilistic Verification. Journal of ACM 42(4), 857–907 (1995)
Bianco, A., De Alfaro, L.: Model Checking of Probabilistic and Nondeterministic Systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)
Kwiatkowska, M.: Quantitative Verification: Models, Techniques and Tools. In: Proc. of SIGSOFT, pp. 449–458 (2007)
Hansson, H., Jonsson, B.: A Logic for Reasoning About Time and Reliability. Formal Aspects of Computing 6(5), 512–535 (1994)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-Time Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)
Kozine, I., Utkin, L.: Interval-Valued Finite Markov Chains. Reliable Computing 8(2), 97–113 (2002)
Sen, K., Viswanathan, M., Agha, G.: Model-Checking Markov Chains in the Presence of Uncertainties. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 394–410. Springer, Heidelberg (2006)
Chatterjee, K., Sen, K., Henzinger, T.: Model-Checking ω-regular Properties of Interval Markov Chains. In: Proc. of FOSSACS, pp. 302–317 (2008)
Ben-Tal, A., Nemirovski, A.: Robust Solutions of Uncertain Linear Programs. Oper. Res. Lett. 25(1), 1–13 (1999)
Andreychenko, A., Mikeev, L., Spieler, D., Wolf, V.: Parameter Identification for Markov Models of Biochemical Reactions. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 83–98. Springer, Heidelberg (2011)
Nilim, A., El Ghaoui, L.: Robust Control of Markov Decision Processes with Uncertain Transition Matrices. Journal of Operations Research, 780–798 (2005)
Puggelli, A., et al.: Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties, UC-Berkeley, Tech. Rep. UCB/EECS-2013-24 (April 2013), http://www.eecs.berkeley.edu/Pubs/TechRpts/2013/EECS-2013-24.html
Vardi, M.Y.: Automatic Verification of Probabilistic Concurrent Finite State Programs. In: Proc. of SFCS, pp. 327–338 (1985)
Lehmann, E., Casella, G.: Theory of Point Estimation. Springer, New York (1998)
Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons (1994)
Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated Verification Techniques for Probabilistic Systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53–113. Springer, Heidelberg (2011)
Barbuti, R., Levi, F., Milazzo, P., Scatena, G.: Probabilistic Model Checking of Biological Systems with Uncertain Kinetic Rates. In: Bournez, O., Potapov, I. (eds.) RP 2009. LNCS, vol. 5797, pp. 64–78. Springer, Heidelberg (2009)
Hahn, E.M., et al.: Synthesis for PCTL in Parametric Markov Decision Processes (2011)
Kwiatkowska, M., Norman, G., Segala, R.: Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 194. Springer, Heidelberg (2001)
Wolff, E., et al.: Robust Control of Uncertain Markov Decision Processes with Temporal Logic Specifications. In: CDC (2012)
D’Innocenzo, A., et al.: Robust PCTL Model Checking. In: Proc. of HSCC, pp. 275–286 (2012)
Clarke, E., Emerson, A.: Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. In: Proc. of WLP, vol. 131 (1981)
Nesterov, Y., Nemirovski, A.: Interior-Point Polynomial Algorithms in Convex Programming. Studies in Applied and Numerical Mathematics (1994)
Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge University Press (2004)
MOSEK, http://www.mosek.com
Aspnes, J., Herlihy, M.: Fast Randomized Consensus Using Shared Memory. Journal of Algorithms 11(3), 441–461 (1990)
Cheshire, S., Adoba, B., Gutterman, E.: Dynamic configuration of IPv4 link local addresses, http://www.ietf.org/rfc/rfc3927.txt
Kwiatkowska, M., et al.: Performance Analysis of Probabilistic Timed Automata Using Digital Clocks. Formal Methods in System Design 29, 33–78 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., Seshia, S.A. (2013). Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties. In: Sharygina, N., Veith, H. (eds) Computer Aided Verification. CAV 2013. Lecture Notes in Computer Science, vol 8044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39799-8_35
Download citation
DOI: https://doi.org/10.1007/978-3-642-39799-8_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39798-1
Online ISBN: 978-3-642-39799-8
eBook Packages: Computer ScienceComputer Science (R0)