{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,30]],"date-time":"2026-08-30T01:05:33Z","timestamp":1788051933569,"version":"build-2784847793"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319249520","type":"print"},{"value":"9783319249537","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24953-7_10","type":"book-chapter","created":{"date-parts":[[2015,10,7]],"date-time":"2015-10-07T11:00:11Z","timestamp":1444215611000},"page":"131-147","source":"Crossref","is-referenced-by-count":20,"title":["Explicit Model Checking of Very Large MDP Using Partitioning and Secondary Storage"],"prefix":"10.1007","author":[{"given":"Arnd","family":"Hartmanns","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"issue":"9","key":"10_CR1","doi-asserted-by":"publisher","first-page":"1116","DOI":"10.1145\/48529.48535","volume":"31","author":"A Aggarwal","year":"1988","unstructured":"Aggarwal, A., Vitter, J.S.: The input\/output complexity of sorting and related problems. Commun. ACM 31(9), 1116\u20131127 (1988)","journal-title":"Commun. ACM"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-46419-0_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Alfaro de","year":"2000","unstructured":"de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of probabilistic processes using MTBDDs and the kronecker representation. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, pp. 395\u2013410. Springer, Heidelberg (2000)"},{"issue":"2","key":"10_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"10_CR4","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/j.entcs.2005.10.034","volume":"153","author":"C Baier","year":"2006","unstructured":"Baier, C., D\u2019Argenio, P.R., Gr\u00f6\u00dfer, M.: Partial order reduction for probabilistic branching time. Electron. Notes Theor. Comput. Sci. 153(2), 97\u2013116 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/978-3-540-31980-1_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Bao","year":"2005","unstructured":"Bao, T., Jones, M.: Time-efficient model checking with magnetic disk. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 526\u2013540. Springer, Heidelberg (2005)"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-540-73368-3_32","volume-title":"Computer Aided Verification","author":"J Barnat","year":"2007","unstructured":"Barnat, J., Brim, L., \u0160ime\u010dek, P.: I\/O efficient accepting cycle detection. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 281\u2013293. Springer, Heidelberg (2007)"},{"issue":"2","key":"10_CR7","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/s10703-006-0007-0","volume":"29","author":"A Bell","year":"2006","unstructured":"Bell, A., Haverkort, B.R.: Distributed disk-based algorithms for model checking very large Markov chains. Formal Methods Syst. Des. 29(2), 177\u2013196 (2006)","journal-title":"Formal Methods Syst. Des."},{"issue":"10","key":"10_CR8","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"32","author":"HC Bohnenkamp","year":"2006","unstructured":"Bohnenkamp, H.C., D\u2019Argenio, P.R., Hermanns, H., Katoen, J.: MoDeST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Softw. Eng. 32(10), 812\u2013830 (2006)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10_CR9","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"10_CR10","unstructured":"Dai, P., Goldsmith, J.: Topological value iteration algorithm for Markov decision processes. In: IJCAI, pp. 1860\u20131865 (2007)"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/BFb0022197","volume-title":"Computer Performance Evaluation Modelling Techniques and Tools","author":"DD Deavours","year":"1997","unstructured":"Deavours, D.D., Sanders, W.H.: An efficient disk-based tool for solving very large Markov models. In: Marie, R., Plateau, B., Calzarossa, M., Rubino, G. (eds.) Computer Performance Evaluation Modelling Techniques and Tools. LNCS, vol. 1245, pp. 58\u201371. Springer, Heidelberg (1997)"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-36126-X_13","volume-title":"Formal Methods in Computer-Aided Design","author":"GD Penna","year":"2002","unstructured":"Penna, G.D., Intrigila, B., Tronci, E., Zilli, M.V.: Exploiting transition locality in the disk based Mur\n                    \n                      \n                    \n                    $$\\phi $$\n                    \n                      \n                        \u03d5\n                      \n                    \n                   verifier. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) Formal Methods in Computer-Aided Design. LNCS, vol. 2517, pp. 202\u2013219. Springer, Heidelberg (2002)"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11691617_1","volume-title":"Model Checking Software","author":"S Edelkamp","year":"2006","unstructured":"Edelkamp, S., Jabbar, S.: Large-scale directed model checking LTL. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 1\u201318. Springer, Heidelberg (2006)"},{"key":"10_CR14","unstructured":"Edelkamp, S., Jabbar, S., Bonet, B.: External memory value iteration. In: ICAPS, pp. 128\u2013135. AAAI (2007)"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/978-3-540-70545-1_50","volume-title":"Computer Aided Verification","author":"S Edelkamp","year":"2008","unstructured":"Edelkamp, S., Sanders, P., \u0160ime\u010dek, P.: Semi-external LTL model checking. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 530\u2013542. Springer, Heidelberg (2008)"},{"issue":"7","key":"10_CR16","doi-asserted-by":"publisher","first-page":"778","DOI":"10.1016\/j.scico.2011.09.005","volume":"78","author":"S Evangelista","year":"2013","unstructured":"Evangelista, S., Kristensen, L.M.: Dynamic state space partitioning for external memory state space exploration. Sci. Comput. Program. 78(7), 778\u2013795 (2013)","journal-title":"Sci. Comput. Program."},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-21455-4_3","volume-title":"Formal Methods for Eternal Networked Software Systems","author":"V Forejt","year":"2011","unstructured":"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\u2013113. Springer, Heidelberg (2011)"},{"key":"10_CR18","unstructured":"Hahn, E.M., Hartmanns, A., Hermanns, H.: Reachability and reward checking for stochastic timed automata. ECEASST 70 (2014)"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-540-70952-7_4","volume-title":"Formal Methods: Applications and Technology","author":"M Hammer","year":"2007","unstructured":"Hammer, M., Weber, M.: \u201cTo store or not to store\u201d reloaded: reclaiming memory on demand. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol. 4346, pp. 51\u201366. Springer, Heidelberg (2007)"},{"key":"10_CR20","unstructured":"Harrison, P.G., Knottenbelt, W.J.: Distributed disk-based solution techniques for large Markov models. In: Numerical Solution of Markov Chains, pp. 58\u201375 (1999)"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Hermanns, H.: A Modest approach to checking probabilistic timed automata. In: QEST, pp. 187\u2013196. IEEE Computer Society (2009)","DOI":"10.1109\/QEST.2009.41"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/978-3-642-54862-8_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2014","unstructured":"Hartmanns, A., Hermanns, H.: The Modest Toolset: an integrated environment for quantitative modelling and verification. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 593\u2013598. Springer, Heidelberg (2014)"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-70545-1_16","volume-title":"Computer Aided Verification","author":"H Hermanns","year":"2008","unstructured":"Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 162\u2013175. Springer, Heidelberg (2008)"},{"issue":"4","key":"10_CR24","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1016\/S1571-0661(05)80394-9","volume":"68","author":"MZ Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M.Z., Mehmood, R., Norman, G., Parker, D.: A symbolic out-of-core solution method for Markov models. Electron. Notes Theor. Comput. Sci. 68(4), 589\u2013604 (2002)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"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\u2013591. Springer, Heidelberg (2011)"},{"issue":"1","key":"10_CR26","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10703-006-0005-2","volume":"29","author":"MZ Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods Syst. Des. 29(1), 33\u201378 (2006)","journal-title":"Formal Methods Syst. Des."},{"issue":"1","key":"10_CR27","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"282","author":"MZ Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M.Z., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theoretical Comput. Sci. 282(1), 101\u2013150 (2002)","journal-title":"Theoretical Comput. Sci."},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-45605-8_11","volume-title":"Process Algebra and Probabilistic Methods. Performance Modeling and Verification","author":"M Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol. 2399, pp. 169\u2013187. Springer, Heidelberg (2002)"},{"key":"10_CR29","unstructured":"LZ4. \n                    http:\/\/www.lz4.info\/\n                    \n                  . Accessed 2 July 2015"},{"key":"10_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-540-24611-4_7","volume-title":"Validation of Stochastic Systems: A Guide to Current Research","author":"R Mehmood","year":"2004","unstructured":"Mehmood, R.: Serial disk-based analysis of large stochastic models. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 230\u2013255. Springer, Heidelberg (2004)"},{"issue":"2","key":"10_CR31","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/s10703-012-0177-x","volume":"43","author":"G Norman","year":"2013","unstructured":"Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Formal Methods Syst. Des. 43(2), 164\u2013190 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"10_CR32","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"ML Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (1994)"},{"key":"10_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/BFb0028743","volume-title":"Computer Aided Verification","author":"U Stern","year":"1998","unstructured":"Stern, U., Dill, D.L.: Using magnetic disk instead of main memory in the Mur\n                    \n                      \n                    \n                    $$\\phi $$\n                    \n                      \n                        \u03d5\n                      \n                    \n                   verifier. In: Hu, A.J., Vardi, M.Y. (eds.) Computer Aided Verification. LNCS, vol. 1427, pp. 172\u2013183. Springer, Heidelberg (1998)"},{"key":"10_CR34","volume-title":"Introduction to the Numerical Solution of Markov Chains","author":"WJ Stewart","year":"1994","unstructured":"Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton (1994)"},{"key":"10_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-642-19835-9_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Timmer","year":"2011","unstructured":"Timmer, M., Stoelinga, M., van de Pol, J.: Confluence reduction for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 311\u2013325. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24953-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T00:20:43Z","timestamp":1559262043000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24953-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319249520","9783319249537"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24953-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}