Abstract
Value and policy iteration are powerful methods for verifying quantitative properties of Markov Decision Processes (MDPs). In order to accelerate these methods many approaches have been proposed. The performance of these methods depends on the graphical structure of MDPs. Experimental results show that they don’t work much better than normal value/policy iteration when the graph of the MDP is dense. In this paper we present an algorithm which tries to reduce the number of updates in dense MDPs. In this algorithm, instead of saving unnecessary updates we use graph partitioning method to have more important updates.
Chapter PDF
Similar content being viewed by others
Keywords
References
Baier, C., Katoen, J.P.: Principles of model checking. MIT press Cambridge (2008)
Barto, A.G., Bradtke, S.J., Singh, S.P.: Learning to act using real-time dynamic programming. Artificial Intelligence 72(1), 81–138 (1995)
Brázdil, T., Chatterjee, K., Chmelík, M., Forejt, V., Křetínský, J., Kwiatkowska, M., Parker, D., Ujma, M.: Verification of markov decision processes using learning algorithms. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 98–114. Springer, Heidelberg (2014)
Dai, P., Mausam, J.G., Weld, D.S., Goldsmith, J.: Topological value iteration algorithms. J. Artif. Intell. Res(JAIR) 42, 181–209 (2011)
Kwiatkowska, M., Parker, D., Qu, H.: Incremental quantitative verification for markov decision processes. In: 2011 IEEE/IFIP 41st International Conference on Dependable Systems & Networks (DSN), pp. 359–370. IEEE (2011)
Puterman, M.L.: Markov decision processes: discrete stochastic dynamic programming. John Wiley & Sons (1994)
Sanner, S., Goetschalckx, R., Driessens, K., Shani, G.: Bayesian real-time dynamic programming. In: IJCAI, pp. 1784–1789. Citeseer (2009)
Smith, T., Simmons, R.: Focused real-time dynamic programming for mdps: Squeezing more out of a heuristic. In: AAAI, pp. 1227–1232 (2006)
Wingate, D., Seppi, K.D.: Prioritization methods for accelerating mdp solvers. Journal of Machine Learning Research, 851–881 (2005)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 IFIP International Federation for Information Processing
About this paper
Cite this paper
Karimpour, J., Isazadeh, A., Mohagheghi, M., Salehi, K. (2015). Improved Iterative Methods for Verifying Markov Decision Processes. In: Dastani, M., Sirjani, M. (eds) Fundamentals of Software Engineering. FSEN 2015. Lecture Notes in Computer Science(), vol 9392. Springer, Cham. https://doi.org/10.1007/978-3-319-24644-4_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-24644-4_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24643-7
Online ISBN: 978-3-319-24644-4
eBook Packages: Computer ScienceComputer Science (R0)