Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Journal of Automated Reasoning
Published in: Journal of Automated Reasoning 3/2017

20-12-2016

Markov Chains and Markov Decision Processes in Isabelle/HOL

Author: Johannes Hölzl

Published in: Journal of Automated Reasoning | Issue 3/2017

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

This paper presents an extensive formalization of Markov chains (MCs) and Markov decision processes (MDPs), with discrete time and (possibly infinite) discrete state-spaces. The formalization takes a coalgebraic view on the transition systems representing MCs and constructs their trace spaces. On these trace spaces properties like fairness, reachability, and stationary distributions are formalized. Similar to MCs, MDPs are represented as transition systems with a construction for trace spaces. These trace spaces provide maximal and minimal expectation over all possible non-deterministic decisions. As applications we provide a certifier for finite reachability problems and we relate the denotational semantics and operational semantics of the probabilistic guarded command language. A distinctive feature of our formalization is the order-theoretic and coalgebraic view on our concepts: we view transition systems as coalgebras, we view traces as coinductive streams, we provide iterative computation rules for expectations, and we define many properties on traces as least or greatest fixed points.
previous article Automated Reducible Geometric Theorem Proving and Discovery by Gröbner Basis Method

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Footnotes
1
The proof in the Isabelle repository is derived from Fubini’s theorem on \(\sigma \)-finite measures. The reason is that Isabelle’s Giry monad is only available on sub-probability measures, hence following the presented proof would result in a weaker theorem.
 
2
A more powerful approach is the extension theorem by Ionescu-Tulcea, e.g. as presented in [43, 46], which allows Markov kernels on arbitrary measurable spaces. While we formalized this extension theorem in Isabelle/HOL it was not available for the formalization of Markov chains. Our formalized version of Ionescu-Tulcea is available in Isabelle 2016.
 
Literature
1.
2.
Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Program. 74(8), 568–589 (2009). (Special Issue on Mathematics of Program Construction (MPC 2006)) MathSciNetCrossRefMATH
3.
4.
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–148 (2000)
5.
Baier, C.: On the algorithmic verification of probabilistic systems. Habilitation, Universität Mannheim (1998)
6.
Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH
7.
Berg, M.: Formal verification of cryptographic security proofs. Ph.D. thesis, Saarland University (2013)
8.
Blanchette, J.C., Hölzl, 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–110. Springer (2014)
9.
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–60. Springer (2014)
10.
Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.): Interactive Theorem Proving (ITP 2013), LNCS, vol. 7998. Springer (2013)
11.
Celiku, O., McIver, A.: Cost-based analysis of probabilistic programs mechanised in HOL. Nord. J. Comput. 11(2), 102–128 (2004)MathSciNetMATH
12.
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–178 (2012)
13.
Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order, 2nd edn. Cambridge University Press, Cambridge (2002)CrossRefMATH
14.
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–294 (2004)
15.
de Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford University. Technical report STAN-CS-TR-98-1601 (1997)
16.
Eberl, M., Hölzl, J., Nipkow, T.: A verified compiler for probability density functions. In: European Symposium on Programming (ESOP 2015), LNCS (2015)
17.
Esparza, J., Kučera, A., Mayr, R.: Model checking probabilistic pushdown automata. In: Logic in Computer Science (LICS 2004), pp. 12–21 (2004)
18.
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–478. Springer (2013)
19.
Etessami, K., Yannakakis, M.: Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. J. ACM 56(1), 1–66 (2009)MathSciNetCrossRefMATH
20.
Giry, M.: A categorical approach to probability theory. In: Categorical Aspects of Topology and Analysis, Lecture Notes in Mathematics, vol. 915, pp. 68–85 (1982)
21.
Gonthier, G., Norrish, M. (eds.): CPP 2013, LNCS, vol. 8307. Springer (2013)
22.
23.
Gretz, F., Katoen, J., McIver, A.: Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Eval. 73, 110–132 (2014)CrossRef
24.
Haddad, S., Monmege, B.: Reachability in MDPS: refining convergence of value iteration. In: Reachability Problems (RP 2014), LNCS, vol. 8762, pp. 125–137 Springer (2014)
25.
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Technical report SICS/R90013, Swedish Institute of Computer Science (1994)
26.
Hölzl, J.: Construction and stochastic applications of measure spaces in higher-order logic. Ph.D. thesis, Technische Universität München (2013)
27.
Hölzl, 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–482. Springer (2016)
28.
Hölzl, 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–151. Springer (2011)
29.
Hölzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle/HOL. In: Blazy et al. [10], pp. 279–294
30.
Hölzl, 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–220 (2015)
31.
Hölzl, 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)
32.
33.
Hölzl, J., Nipkow, T.: Verifying pCTL model checking. In: Flanagan, C., König, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), LNCS, vol. 7214, pp. 347–361 (2012)
34.
Huffman, B., Kunčar, O.: Lifting and transfer: a modular design for quotients in Isabelle/HOL. In: Gonthier and Norrish [21], pp. 131–146
35.
Hurd, J.: Formal verification of probabilistic algorithms. Ph.D. thesis, University of Cambridge (2002)
36.
37.
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–104 (2011)CrossRef
38.
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–270 (2007)
39.
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–591 (2011)
40.
Liu, L., Hasan, O., Aravantinos, V., Tahar, S.: Formal reasoning about classified Markov chains in HOL. In: Blazy et al. [10], pp. 295–310
41.
Lochbihler, A.: Probabilistic functions and cryptographic oracles in higher order logic. In: ESOP, LNCS, vol. 9632, pp. 503–531. Springer (2016)
42.
McIver, A., Morgan, C.: Abstraction, Refinement And Proof For Probabilistic Systems. Monographs in Computer Science. Springer, Berlin (2004)
43.
Monniaux, D.: Abstract interpretation of programs as Markov decision processes. Sci. Comput. Program. 58(1–2), 179–205 (2005). (Special Issue on the Static Analysis Symposium (SAS 2003)) MathSciNetCrossRefMATH
44.
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–212. The MIT Press (2000)
45.
Petcher, A., Morrisett, G.: The foundational cryptography framework. In: POST, LNCS, vol. 9036, pp. 53–72. Springer (2015)
46.
Pollard, D.: A Users’s Guide to Measure Theoretic Probability, Cambridge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, Cambridge (2002)
47.
Popescu, A., Hölzl, J., Nipkow, T.: Formalizing probabilistic noninterference. In: Gonthier and Norrish [21], pp. 259–275
48.
49.
Richter, S.: Formalizing integration theory with an application to probabilistic algorithms. In: TPHOLs, LNCS, vol. 3223, pp. 271–286. Springer (2004)
50.
Trivedi, K.S.: Probability & Statistics with Reliability, Queuing, and Computer Science Applications. Prentice-Hall, Englewood Cliffs (1982)MATH
51.
Metadata
Title
Markov Chains and Markov Decision Processes in Isabelle/HOL
Author
Johannes Hölzl
Publication date
20-12-2016
Publisher
Springer Netherlands
Published in
Journal of Automated Reasoning / Issue 3/2017
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-016-9401-5

Premium Partner

    Image Credits