Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Markov Models

view this post on Zulip Email Gateway (Aug 18 2022 at 18:55):

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