Formalization of finite-state discrete-time Markov chains in HOL
DOI10.1007/978-3-642-24372-1_8zbMATH Open1348.68221OpenAlexW84587889MaRDI QIDQ3172906FDOQ3172906
Authors: Liya Liu, Osman Hasan, Sofiène Tahar 
Publication date: 7 October 2011
Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-24372-1_8
Recommendations
- Formal reasoning about finite-state discrete-time Markov chains in HOL
- Formal reasoning about classified Markov chains in HOL
- Markov chains and Markov decision processes in Isabelle/HOL
- Probabilistic analysis of dynamic fault trees using HOL theorem proving
- Reasoning about conditional probabilities in a higher-order-logic theorem prover
Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (6)
- Formalization of Normal Random Variables in HOL
- Reasoning about conditional probabilities in a higher-order-logic theorem prover
- A compositional framework for Markov processes
- On the formalization of gamma function in HOL
- Verification of Expectation Properties for Discrete Random Variables in HOL
- Formal reasoning about finite-state discrete-time Markov chains in HOL
Uses Software
This page was built for publication: Formalization of finite-state discrete-time Markov chains in HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3172906)
