{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T05:54:55Z","timestamp":1783490095534,"version":"3.55.0"},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2016,12,20]],"date-time":"2016-12-20T00:00:00Z","timestamp":1482192000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["NI 491\/15-1"],"award-info":[{"award-number":["NI 491\/15-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.1007\/s10817-016-9401-5","type":"journal-article","created":{"date-parts":[[2016,12,20]],"date-time":"2016-12-20T15:22:37Z","timestamp":1482247357000},"page":"345-387","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Markov Chains and Markov Decision Processes in Isabelle\/HOL"],"prefix":"10.1007","volume":"59","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0869-9250","authenticated-orcid":false,"given":"Johannes","family":"H\u00f6lzl","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,12,20]]},"reference":[{"issue":"1","key":"9401_CR1","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/s10817-013-9298-1","volume":"53","author":"R Affeldt","year":"2014","unstructured":"Affeldt, R., Hagiwara, M., S\u00e9nizergues, J.: Formalization of Shannon\u2019s theorems. J. Autom. Reason. 53(1), 63\u2013103 (2014)","journal-title":"J. Autom. Reason."},{"issue":"8","key":"9401_CR2","doi-asserted-by":"crossref","first-page":"568","DOI":"10.1016\/j.scico.2007.09.002","volume":"74","author":"P Audebaud","year":"2009","unstructured":"Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Program. 74(8), 568\u2013589 (2009). (Special Issue on Mathematics of Program Construction (MPC 2006))","journal-title":"Sci. Comput. Program."},{"key":"9401_CR3","unstructured":"Avigad, J., H\u00f6lzl, J., Serafin, L.: A formally verified proof of the central limit theorem. CoRR arxiv:1405.7012 (2014)"},{"key":"9401_CR4","doi-asserted-by":"crossref","unstructured":"Backhouse, R.C.: Galois connections and fixed point calculus. In: Backhouse, R.C., Crole, R.L., Gibbons, J. (eds.) Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, LNCS, vol. 2297, pp. 89\u2013148 (2000)","DOI":"10.1007\/3-540-47797-7_4"},{"key":"9401_CR5","unstructured":"Baier, C.: On the algorithmic verification of probabilistic systems. Habilitation, Universit\u00e4t Mannheim (1998)"},{"key":"9401_CR6","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"9401_CR7","unstructured":"Berg, M.: Formal verification of cryptographic security proofs. Ph.D. thesis, Saarland University (2013)"},{"key":"9401_CR8","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., H\u00f6lzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle\/HOL. In: Klein, G., Gamboa, R. (eds.) Interactive Theorem Proving (ITP 2014), LNCS, vol. 8558, pp. 93\u2013110. Springer (2014)","DOI":"10.1007\/978-3-319-08970-6_7"},{"key":"9401_CR9","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Unified classical logic completeness. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Automated Reasoning (IJCAR 2014), LNCS, vol. 8562, pp. 46\u201360. Springer (2014)","DOI":"10.1007\/978-3-319-08587-6_4"},{"key":"9401_CR10","doi-asserted-by":"crossref","unstructured":"Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.): Interactive Theorem Proving (ITP 2013), LNCS, vol. 7998. Springer (2013)","DOI":"10.1007\/978-3-642-39634-2"},{"issue":"2","key":"9401_CR11","first-page":"102","volume":"11","author":"O Celiku","year":"2004","unstructured":"Celiku, O., McIver, A.: Cost-based analysis of probabilistic programs mechanised in HOL. Nord. J. Comput. 11(2), 102\u2013128 (2004)","journal-title":"Nord. J. Comput."},{"key":"9401_CR12","doi-asserted-by":"crossref","unstructured":"Cock, D.: Verifying probabilistic correctness in Isabelle with pGCL. In: Cassez, F., Huuck, R., Klein, G., Schlich, B. (eds.) Systems Software Verification (SSV 2012), EPTCS, vol. 102, pp. 167\u2013178 (2012)","DOI":"10.4204\/EPTCS.102.15"},{"key":"9401_CR13","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511809088","volume-title":"Introduction to Lattices and Order","author":"BA Davey","year":"2002","unstructured":"Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order, 2nd edn. Cambridge University Press, Cambridge (2002)","edition":"2"},{"key":"9401_CR14","doi-asserted-by":"crossref","unstructured":"Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. In: Liu, Z., Araki, K. (eds.) Theoretical Aspects of Computing (ICTAC 2004), LNCS, vol. 3407, pp. 280\u2013294 (2004)","DOI":"10.1007\/978-3-540-31862-0_21"},{"key":"9401_CR15","unstructured":"de\u00a0Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford University. Technical report STAN-CS-TR-98-1601 (1997)"},{"key":"9401_CR16","doi-asserted-by":"crossref","unstructured":"Eberl, M., H\u00f6lzl, J., Nipkow, T.: A verified compiler for probability density functions. In: European Symposium on Programming (ESOP 2015), LNCS (2015)","DOI":"10.1007\/978-3-662-46669-8_4"},{"key":"9401_CR17","doi-asserted-by":"crossref","unstructured":"Esparza, J., Ku\u010dera, A., Mayr, R.: Model checking probabilistic pushdown automata. In: Logic in Computer Science (LICS 2004), pp. 12\u201321 (2004)","DOI":"10.1109\/LICS.2004.1319596"},{"key":"9401_CR18","doi-asserted-by":"crossref","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.: A fully verified executable LTL model checker. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification (CAV 2013), LNCS, vol. 8044, pp. 463\u2013478. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_31"},{"issue":"1","key":"9401_CR19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1462153.1462154","volume":"56","author":"K Etessami","year":"2009","unstructured":"Etessami, K., Yannakakis, M.: Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. J. ACM 56(1), 1\u201366 (2009)","journal-title":"J. ACM"},{"key":"9401_CR20","doi-asserted-by":"crossref","unstructured":"Giry, M.: A categorical approach to probability theory. In: Categorical Aspects of Topology and Analysis, Lecture Notes in Mathematics, vol. 915, pp. 68\u201385 (1982)","DOI":"10.1007\/BFb0092872"},{"key":"9401_CR21","unstructured":"Gonthier, G., Norrish, M. (eds.): CPP 2013, LNCS, vol. 8307. Springer (2013)"},{"key":"9401_CR22","unstructured":"Gouezel, S.: Ergodic theory. The Archive of Formal Proofs (Formal Proof Development). https:\/\/www.isa-afp.org\/entries\/Ergodic_Theory.shtml (2015)"},{"key":"9401_CR23","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1016\/j.peva.2013.11.004","volume":"73","author":"F Gretz","year":"2014","unstructured":"Gretz, F., Katoen, J., McIver, A.: Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Eval. 73, 110\u2013132 (2014)","journal-title":"Perform. Eval."},{"key":"9401_CR24","doi-asserted-by":"crossref","unstructured":"Haddad, S., Monmege, B.: Reachability in MDPS: refining convergence of value iteration. In: Reachability Problems (RP 2014), LNCS, vol. 8762, pp. 125\u2013137 Springer (2014)","DOI":"10.1007\/978-3-319-11439-2_10"},{"key":"9401_CR25","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Technical report SICS\/R90013, Swedish Institute of Computer Science (1994)"},{"key":"9401_CR26","unstructured":"H\u00f6lzl, J.: Construction and stochastic applications of measure spaces in higher-order logic. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2013)"},{"key":"9401_CR27","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J.: Formalising semantics for expected running time of probabilistic programs. In: Blanchette, C.J., Merz, S. (eds.) Interactive Theorem Proving (ITP 2016), LNCS, vol. 9807, pp. 475\u2013482. Springer (2016)","DOI":"10.1007\/978-3-319-43144-4_30"},{"key":"9401_CR28","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J., Heller, A.: Three chapters of measure theory in Isabelle\/HOL. In: van Eekelen, M.C.J.D., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) Interactive Theorem Proving (ITP 2011), LNCS, vol. 6898, pp. 135\u2013151. Springer (2011)","DOI":"10.1007\/978-3-642-22863-6_12"},{"key":"9401_CR29","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle\/HOL. In: Blazy et\u00a0al. [10], pp. 279\u2013294","DOI":"10.1007\/978-3-642-39634-2_21"},{"key":"9401_CR30","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J., Lochbihler, A., Traytel, D.: A formalized hierarchy of probabilistic system types (proof pearl). In: Urban, C., Zhang, X. (eds.) Interactive Theorem Proving (ITP 2015), LNCS, vol. 9236, pp. 203\u2013220 (2015)","DOI":"10.1007\/978-3-319-22102-1_13"},{"key":"9401_CR31","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J., Nipkow, T.: Interactive verification of Markov chains: two distributed protocol case studies. In: Fahrenberg, U., Legay, A., Thrane, C. (eds.) Quantities in Formal Methods (QFM 2012), EPTCS, vol. 103(2012)","DOI":"10.4204\/EPTCS.103.2"},{"key":"9401_CR32","unstructured":"H\u00f6lzl, J., Nipkow, T.: Markov models. The Archive of Formal Proofs (Formal Proof Development). https:\/\/www.isa-afp.org\/entries\/Markov_Models.shtml (2012)"},{"key":"9401_CR33","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J., Nipkow, T.: Verifying pCTL model checking. In: Flanagan, C., K\u00f6nig, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), LNCS, vol. 7214, pp. 347\u2013361 (2012)","DOI":"10.1007\/978-3-642-28756-5_24"},{"key":"9401_CR34","doi-asserted-by":"crossref","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and transfer: a modular design for quotients in Isabelle\/HOL. In: Gonthier and Norrish [21], pp. 131\u2013146","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"9401_CR35","unstructured":"Hurd, J.: Formal verification of probabilistic algorithms. Ph.D. thesis, University of Cambridge (2002)"},{"issue":"1","key":"9401_CR36","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1016\/j.tcs.2005.08.005","volume":"346","author":"J Hurd","year":"2005","unstructured":"Hurd, J., McIver, A., Morgan, C.: Probabilistic guarded commands mechanized in HOL. Theor. Comput. Sci. 346(1), 96\u2013112 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"9401_CR37","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","volume":"68","author":"JP Katoen","year":"2011","unstructured":"Katoen, J.P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68, 90\u2013104 (2011)","journal-title":"Perform. Eval."},{"key":"9401_CR38","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM 2007), LNCS, vol. 4486, pp. 220\u2013270 (2007)","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"9401_CR39","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Computer Aided Verification (CAV 2011), LNCS, vol. 6806, pp. 585\u2013591 (2011)"},{"key":"9401_CR40","doi-asserted-by":"crossref","unstructured":"Liu, L., Hasan, O., Aravantinos, V., Tahar, S.: Formal reasoning about classified Markov chains in HOL. In: Blazy et\u00a0al. [10], pp. 295\u2013310","DOI":"10.1007\/978-3-642-39634-2_22"},{"key":"9401_CR41","doi-asserted-by":"crossref","unstructured":"Lochbihler, A.: Probabilistic functions and cryptographic oracles in higher order logic. In: ESOP, LNCS, vol. 9632, pp. 503\u2013531. Springer (2016)","DOI":"10.1007\/978-3-662-49498-1_20"},{"key":"9401_CR42","volume-title":"Abstraction, Refinement And Proof For Probabilistic Systems. Monographs in Computer Science","author":"A McIver","year":"2004","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement And Proof For Probabilistic Systems. Monographs in Computer Science. Springer, Berlin (2004)"},{"issue":"1\u20132","key":"9401_CR43","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/j.scico.2005.02.008","volume":"58","author":"D Monniaux","year":"2005","unstructured":"Monniaux, D.: Abstract interpretation of programs as Markov decision processes. Sci. Comput. Program. 58(1\u20132), 179\u2013205 (2005). (Special Issue on the Static Analysis Symposium (SAS 2003))","journal-title":"Sci. Comput. Program."},{"key":"9401_CR44","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: A fixedpoint approach to (co)inductive and (co)datatype definitions. In: Plotkin, G.D., Stirling, C., Tofte M. (eds.) Proof, Language, and Interaction, Essays in Honour of Robin Milner, pp. 187\u2013212. The MIT Press (2000)","DOI":"10.7551\/mitpress\/5641.003.0013"},{"key":"9401_CR45","doi-asserted-by":"crossref","unstructured":"Petcher, A., Morrisett, G.: The foundational cryptography framework. In: POST, LNCS, vol. 9036, pp. 53\u201372. Springer (2015)","DOI":"10.1007\/978-3-662-46666-7_4"},{"key":"9401_CR46","volume-title":"A Users\u2019s Guide to Measure Theoretic Probability, Cambridge Series in Statistical and Probabilistic Mathematics","author":"D Pollard","year":"2002","unstructured":"Pollard, D.: A Users\u2019s Guide to Measure Theoretic Probability, Cambridge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, Cambridge (2002)"},{"key":"9401_CR47","doi-asserted-by":"crossref","unstructured":"Popescu, A., H\u00f6lzl, J., Nipkow, T.: Formalizing probabilistic noninterference. In: Gonthier and Norrish [21], pp. 259\u2013275","DOI":"10.1007\/978-3-319-03545-1_17"},{"key":"9401_CR48","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1016\/j.entcs.2015.12.021","volume":"319","author":"R Rand","year":"2015","unstructured":"Rand, R., Zdancewic, S.: VPHL: a verified partial-correctness logic for probabilistic programs. ENTCS 319, 351\u2013367 (2015). doi: 10.1016\/j.entcs.2015.12.021","journal-title":"ENTCS"},{"key":"9401_CR49","doi-asserted-by":"crossref","unstructured":"Richter, S.: Formalizing integration theory with an application to probabilistic algorithms. In: TPHOLs, LNCS, vol. 3223, pp. 271\u2013286. Springer (2004)","DOI":"10.1007\/978-3-540-30142-4_20"},{"key":"9401_CR50","volume-title":"Probability & Statistics with Reliability, Queuing, and Computer Science Applications","author":"KS Trivedi","year":"1982","unstructured":"Trivedi, K.S.: Probability & Statistics with Reliability, Queuing, and Computer Science Applications. Prentice-Hall, Englewood Cliffs (1982)"},{"key":"9401_CR51","doi-asserted-by":"crossref","DOI":"10.4171\/071","volume-title":"Denumerable Markov Chains","author":"W Woess","year":"2009","unstructured":"Woess, W.: Denumerable Markov Chains. European Mathematical Society, Warsaw (2009)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9401-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9401-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9401-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,21]],"date-time":"2024-06-21T09:39:36Z","timestamp":1718962776000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9401-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,12,20]]},"references-count":51,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,10]]}},"alternative-id":["9401"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9401-5","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,12,20]]}}}