Markov chains and Markov decision processes in Isabelle/HOL
type: Item
instance of: scholarly article
title: Markov chains and Markov decision processes in Isabelle/HOL
zbMATH Open document ID: 1425.68375
author: Johannes Hölzl
published in: Journal of Automated Reasoning
publication date: 2018-02-22T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 60J10
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 90C40
zbMATH DE Number: 6842149
zbMATH Keywords: Markov chains
zbMATH Keywords: Markov decision processes
zbMATH Keywords: probabilistic guarded command language
zbMATH Keywords: probabilistic model checking
zbMATH Keywords: coalgebras
zbMATH Keywords: transition systems
zbMATH Keywords: trace spaces
zbMATH Keywords: Isabelle/HOL
describes a project that uses: Zoo Probabilistic Systems
describes a project that uses: Isabelle/HOL
describes a project that uses: MRMC
describes a project that uses: PRISM
describes a project that uses: pGCL
describes a project that uses: Lifting
describes a project that uses: Transfer
describes a project that uses: Ergodic theory
describes a project that uses: Markov Models
describes a project that uses: Density Compiler
describes a project that uses: CAVA LTL Modelchecker
describes a project that uses: Archive Formal Proofs
MaRDI profile type: Publication
full work available at URL: s10817-016-9401-5
OpenAlex ID: W2562825158
cites work: Formalization of Shannon's theorems
cites work: Proofs of randomized algorithms in Coq
cites work: A formally verified proof of the central limit theorem
cites work: Q4738112
cites work: Q5322945
cites work: Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations
cites work: Truly Modular (Co)datatypes for Isabelle/HOL
cites work: Unified Classical Logic Completeness
cites work: Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22--26, 2013. Proceedings
cites work: Q4658722
cites work: Abstract interpretation of programs as Markov decision processes
cites work: Q4530231
cites work: Theoretical Aspects of Computing - ICTAC 2004
cites work: A Verified Compiler for Probability Density Functions
cites work: Model Checking Probabilistic Pushdown Automata
cites work: Q3946875
cites work: Certified programs and proofs. Third international conference, CPP 2013, Melbourne, VIC, Australia, December 11--13, 2013. Proceedings
cites work: A Numerical Lower Bound for the Spectral Radius of Random Walks on Surface Groups
cites work: Reachability in MDPs: Refining Convergence of Value Iteration
cites work: A logic for reasoning about time and reliability
cites work: Formalising Semantics for Expected Running Time of Probabilistic Programs
cites work: Three Chapters of Measure Theory in Isabelle/HOL
cites work: Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
cites work: A Formalized Hierarchy of Probabilistic System Types
cites work: Verifying pCTL Model Checking
cites work: Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
cites work: Q4484343
cites work: Probabilistic guarded commands mechanized in HOL
cites work: Stochastic Model Checking
cites work: Formal Reasoning about Classified Markov Chains in HOL
cites work: Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
cites work: Abstraction, Refinement and Proof for Probabilistic Systems
cites work: A user's guide to measure theoretic probability
cites work: Formalizing Probabilistic Noninterference
cites work: VPHL: a verified partial-correctness logic for probabilistic programs
cites work: Theorem Proving in Higher Order Logics
cites work: Q3658792
cites work: Denumerable Markov chains. Generating functions, boundary theory, random walks on trees.
DOI: 10.1007/S10817-016-9401-5
description: scientific article; zbMATH DE number 6842149