Abstract
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. See here for the corresponding paper.
License
Topics
Related publications
- Hölzl, J. (2016). Markov Chains and Markov Decision Processes in Isabelle/HOL. Journal of Automated Reasoning, 59(3), 345–387. https://doi.org/10.1007/s10817-016-9401-5
- Hölzl, J., & Nipkow, T. (2012). Verifying pCTL Model Checking. Tools and Algorithms for the Construction and Analysis of Systems, 347–361. https://doi.org/10.1007/978-3-642-28756-5_24
- Case studies in Proceedings QFM 2012
Session Markov_Models
- Markov_Models_Auxiliary
- Discrete_Time_Markov_Chain
- Trace_Space_Equals_Markov_Processes
- Classifying_Markov_Chain_States
- Markov_Decision_Process
- MDP_Reachability_Problem
- Discrete_Time_Markov_Process
- Continuous_Time_Markov_Chain
- Markov_Models
- Example_A
- Example_B
- PCTL
- PGCL
- Crowds_Protocol
- Zeroconf_Analysis
- Gossip_Broadcast
- MDP_RP_Certification
- MDP_RP