| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Markov Models
| Title: | Markov Models |
| Authors: | Johannes Hölzl and Tobias Nipkow |
| Submission date: | 2012-01-03 |
| 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. |
| BibTeX: |
@article{Markov_Models-AFP,
author = {Johannes Hölzl and Tobias Nipkow},
title = {Markov Models},
journal = {Archive of Formal Proofs},
month = jan,
year = 2012,
note = {\url{https://isa-afp.org/entries/Markov_Models.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Coinductive, Gauss-Jordan-Elim-Fun |
| Used by: | Hidden_Markov_Models, Probabilistic_Noninterference, Probabilistic_Timed_Automata, Stochastic_Matrices |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |