### Abstract

This is a formalization of Markov models in Isabelle/HOL. It builds on Isabelle's probability theory. The available models are currently Discrete-Time Markov Chains and a extensions of them with rewards.

As application of these models we formalize probabilistic model checking of pCTL formulas, analysis of IPv4 address allocation in ZeroConf and an analysis of the anonymity of the Crowds protocol. See here for the corresponding paper.

### License

BSD License

### Topics

- Mathematics/Probability theory
- Computer science/Automata and formal languages

### Related publications

- Hölzl, J. (2016). Markov Chains and Markov Decision Processes in Isabelle/HOL. Journal of Automated Reasoning, 59(3), 345–387. https://doi.org/10.1007/s10817-016-9401-5
- Hölzl, J., & Nipkow, T. (2012). Verifying pCTL Model Checking. Lecture Notes in Computer Science, 347–361. https://doi.org/10.1007/978-3-642-28756-5_24
- Case studies in Proceedings QFM 2012

### Session Markov_Models

- Markov_Models_Auxiliary
- Discrete_Time_Markov_Chain
- Trace_Space_Equals_Markov_Processes
- Classifying_Markov_Chain_States
- Markov_Decision_Process
- MDP_Reachability_Problem
- Discrete_Time_Markov_Process
- Continuous_Time_Markov_Chain
- Markov_Models
- Example_A
- Example_B
- PCTL
- PGCL
- Crowds_Protocol
- Zeroconf_Analysis
- Gossip_Broadcast
- MDP_RP_Certification
- MDP_RP

### Depends on

- Coinductive
- Gauss-Jordan Elimination for Matrices Represented as Functions

### Used by

- Hidden Markov Models
- Probabilistic Timed Automata
- Stochastic Matrices and the Perron-Frobenius Theorem
- Probabilistic Noninterference

## Cite

×

Markov_Models-AFP

    @article{Markov_Models-AFP,
      author  = {Johannes Hölzl and Tobias Nipkow},
      title   = {Markov Models},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2012},
      note    = {\url{https://isa-afp.org/entries/Markov_Models.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Jan 8, 2012 : Isabelle2011-1
- Jan 5, 2012 : Isabelle2011-1