Article

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

Authors:

Alberto Puggelli,

Alberto L. Sangiovanni-Vincentelli,

Sanjit A. SeshiaAuthors Info & Claims

CAV 2013: Proceedings of the 25th International Conference on Computer Aided Verification - Volume 8044

Pages 527 - 542

Published: 13 July 2013 Publication History

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.

References

[1]

Courcoubetis, C., Yannakakis, M.: The Complexity of Probabilistic Verification. Journal of ACM 424, 857---907 1995

Digital Library

[2]

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

Digital Library

[3]

Kwiatkowska, M.: Quantitative Verification: Models, Techniques and Tools. In: Proc. of SIGSOFT, pp. 449---458 2007

Digital Library

[4]

Hansson, H., Jonsson, B.: A Logic for Reasoning About Time and Reliability. Formal Aspects of Computing 65, 512---535 1994

[5]

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

Digital Library

[6]

Kozine, I., Utkin, L.: Interval-Valued Finite Markov Chains. Reliable Computing 82, 97---113 2002

[7]

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

Digital Library

[8]

Chatterjee, K., Sen, K., Henzinger, T.: Model-Checking ω-regular Properties of Interval Markov Chains. In: Proc. of FOSSACS, pp. 302---317 2008

Digital Library

[9]

Ben-Tal, A., Nemirovski, A.: Robust Solutions of Uncertain Linear Programs. Oper. Res. Lett. 251, 1---13 1999

Digital Library

[10]

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

Digital Library

[11]

Nilim, A., El Ghaoui, L.: Robust Control of Markov Decision Processes with Uncertain Transition Matrices. Journal of Operations Research, 780---798 2005

Digital Library

[12]

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

[13]

Vardi, M.Y.: Automatic Verification of Probabilistic Concurrent Finite State Programs. In: Proc. of SFCS, pp. 327---338 1985

Digital Library

[14]

Lehmann, E., Casella, G.: Theory of Point Estimation. Springer, New York 1998

[15]

Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons 1994

Digital Library

[16]

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

[17]

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

Digital Library

[18]

Hahn, E.M., et al.: Synthesis for PCTL in Parametric Markov Decision Processes 2011

[19]

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

Digital Library

[20]

Wolff, E., et al.: Robust Control of Uncertain Markov Decision Processes with Temporal Logic Specifications. In: CDC 2012

[21]

D'Innocenzo, A., et al.: Robust PCTL Model Checking. In: Proc. of HSCC, pp. 275---286 2012

Digital Library

[22]

Clarke, E., Emerson, A.: Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. In: Proc. of WLP, vol. 131 1981

Digital Library

[23]

Nesterov, Y., Nemirovski, A.: Interior-Point Polynomial Algorithms in Convex Programming. Studies in Applied and Numerical Mathematics 1994

[24]

Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge University Press 2004

Digital Library

[25]

MOSEK, http://www.mosek.com

[26]

http://www.eecs.berkeley.edu/~puggelli/

[27]

http://www.prismmodelchecker.org/benchmarks/

[28]

Aspnes, J., Herlihy, M.: Fast Randomized Consensus Using Shared Memory. Journal of Algorithms 113, 441---461 1990

Digital Library

[29]

Cheshire, S., Adoba, B., Gutterman, E.: Dynamic configuration of IPv4 link local addresses, http://www.ietf.org/rfc/rfc3927.txt

[30]

Kwiatkowska, M., et al.: Performance Analysis of Probabilistic Timed Automata Using Digital Clocks. Formal Methods in System Design 29, 33---78 2006

Digital Library

Cited By

Filieri AMaggio MAngelopoulos KD’ippolito NGerostathopoulos IHempel AHoffmann HJamshidi PKalyvianaki EKlein CKrikava FMisailovic SPapadopoulos ARay SSharifloo AShevtsov SUjma MVogel T(2017)Control Strategies for Self-Adaptive Software SystemsACM Transactions on Autonomous and Adaptive Systems10.1145/302418811:4(1-31)Online publication date: 3-Feb-2017
https://dl.acm.org/doi/10.1145/3024188
Seshia SSadigh DSastry S(2015)Formal methods for semi-autonomous drivingProceedings of the 52nd Annual Design Automation Conference10.1145/2744769.2747927(1-5)Online publication date: 7-Jun-2015
https://dl.acm.org/doi/10.1145/2744769.2747927
Puggelli ASangiovanni-Vincentelli ASeshia SMitra TReineke J(2014)Robust strategy synthesis for probabilistic systems applied to risk-limiting renewable-energy pricingProceedings of the 14th International Conference on Embedded Software10.1145/2656045.2656069(1-10)Online publication date: 12-Oct-2014
https://dl.acm.org/doi/10.1145/2656045.2656069
Show More Cited By

Index Terms

Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Modal and temporal logics

Recommendations

Reward is enough for convex MDPs
NIPS '21: Proceedings of the 35th International Conference on Neural Information Processing Systems

Maximising a cumulative reward function that is Markov and stationary, i.e., defined over state-action pairs and independent of time, is sufficient to capture many kinds of goals in a Markov decision process (MDP). However, not all goals can be captured ...
Properties of convex polytopes
Anytime Algorithms for Solving Possibilistic MDPs and Hybrid MDPs
FoIKS 2016: Proceedings of the 9th International Symposium on Foundations of Information and Knowledge Systems - Volume 9616

The ability of an agent to make quick, rational decisions in an uncertain environment is paramount for its applicability in realistic settings. Markov Decision Processes MDP provide such a framework, but can only model uncertainty that can be expressed ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CAV 2013: Proceedings of the 25th International Conference on Computer Aided Verification - Volume 8044

July 2013

1012 pages

ISBN:9783642397981

Editors:
Natasha Sharygina
University of Lugano, Lugano, Switzerland
,
Helmut Veith
University of Technology, Vienna, Austria

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 13 July 2013

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Filieri AMaggio MAngelopoulos KD’ippolito NGerostathopoulos IHempel AHoffmann HJamshidi PKalyvianaki EKlein CKrikava FMisailovic SPapadopoulos ARay SSharifloo AShevtsov SUjma MVogel T(2017)Control Strategies for Self-Adaptive Software SystemsACM Transactions on Autonomous and Adaptive Systems10.1145/302418811:4(1-31)Online publication date: 3-Feb-2017
https://dl.acm.org/doi/10.1145/3024188
Seshia SSadigh DSastry S(2015)Formal methods for semi-autonomous drivingProceedings of the 52nd Annual Design Automation Conference10.1145/2744769.2747927(1-5)Online publication date: 7-Jun-2015
https://dl.acm.org/doi/10.1145/2744769.2747927
Puggelli ASangiovanni-Vincentelli ASeshia SMitra TReineke J(2014)Robust strategy synthesis for probabilistic systems applied to risk-limiting renewable-energy pricingProceedings of the 14th International Conference on Embedded Software10.1145/2656045.2656069(1-10)Online publication date: 12-Oct-2014
https://dl.acm.org/doi/10.1145/2656045.2656069
Su GRosenblum DJalote PBriand LHoek A(2014)Perturbation analysis of stochastic systems with empirical distribution parametersProceedings of the 36th International Conference on Software Engineering10.1145/2568225.2568256(311-321)Online publication date: 31-May-2014
https://dl.acm.org/doi/10.1145/2568225.2568256

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents