[isabelle] New AFP entry: Markov Models
- To: Isabelle Users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] New AFP entry: Markov Models
- From: Tobias Nipkow <nipkow at in.tum.de>
- Date: Sun, 08 Jan 2012 21:44:48 +0100
- User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:8.0) Gecko/20111105 Thunderbird/8.0
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