[isabelle] New AFP entry: Markov Models



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!





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.