From: Tobias Nipkow <nipkow@in.tum.de>
Markov Models
Johannes Hölzl and Tobias Nipkow
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.
http://afp.sourceforge.net/entries/Markov_Models.shtml
The corresponding TACAS 2012 paper:
http://www.in.tum.de/~nipkow/pubs/tacas12.html
Enjoy!
Last updated: Apr 26 2024 at 12:28 UTC