[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.


The corresponding TACAS 2012 paper:


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