Markov chains and Markov decision processes in Isabelle/HOL

DOI10.1007/s10817-016-9401-5zbMath1425.68375OpenAlexW2562825158MaRDI QIDQ1701041

Johannes Hölzl

Publication date: 22 February 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-016-9401-5

zbMATH Keywords

Markov chainsMarkov decision processescoalgebrastransition systemsIsabelle/HOLprobabilistic model checkingtrace spacesprobabilistic guarded command language

Mathematics Subject Classification ID

Markov chains (discrete-time Markov processes on discrete state spaces) (60J10) Markov and semi-Markov decision processes (90C40) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Computational logic: its origins and applications ⋮ Program logic for higher-order probabilistic programs in Isabelle/HOL ⋮ Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL ⋮ Verified analysis of random binary tree structures

Uses Software

• PRISM
• Isabelle/HOL
• MRMC
• pGCL
• Transfer
• Lifting
• Ergodic theory
• Zoo Probabilistic Systems
• Markov Models
• Archive Formal Proofs
• Density Compiler
• CAVA LTL Modelchecker

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Certified programs and proofs. Third international conference, CPP 2013, Melbourne, VIC, Australia, December 11--13, 2013. Proceedings
• Denumerable Markov chains. Generating functions, boundary theory, random walks on trees.
• Proofs of randomized algorithms in Coq
• A logic for reasoning about time and reliability
• A formally verified proof of the central limit theorem
• Formalization of Shannon's theorems
• Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22--26, 2013. Proceedings
• Abstract interpretation of programs as Markov decision processes
• Probabilistic guarded commands mechanized in HOL
• A User's Guide to Measure Theoretic Probability
• A Verified Compiler for Probability Density Functions
• Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
• Formalising Semantics for Expected Running Time of Probabilistic Programs
• Truly Modular (Co)datatypes for Isabelle/HOL
• Verifying pCTL Model Checking
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Formalizing Probabilistic Noninterference
• A Formalized Hierarchy of Probabilistic System Types
• Stochastic Model Checking
• Three Chapters of Measure Theory in Isabelle/HOL
• Unified Classical Logic Completeness
• Reachability in MDPs: Refining Convergence of Value Iteration
• Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations
• Abstraction, Refinement and Proof for Probabilistic Systems
• Model Checking Probabilistic Pushdown Automata
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• Formal Reasoning about Classified Markov Chains in HOL
• A Numerical Lower Bound for the Spectral Radius of Random Walks on Surface Groups
• Theorem Proving in Higher Order Logics
• Theoretical Aspects of Computing - ICTAC 2004
• VPHL: a verified partial-correctness logic for probabilistic programs