Formal reasoning about finite-state discrete-time Markov chains in HOL

DOI10.1007/s11390-013-1324-6zbMath1280.68124OpenAlexW2016818970MaRDI QIDQ2434565

Liya Liu, Sofiène Tahar, Osman Hasan

Publication date: 6 February 2014

Published in: Journal of Computer Science and Technology (Search for Journal in Brave)

Full work available at URL: https://spectrum.library.concordia.ca/977339/1/JCST-2013.pdf

zbMATH Keywords

higher-order logicprobability theorytheorem proverdiscrete-time Markov chain

Mathematics Subject Classification ID

Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items

The formalization of discrete Fourier transform in HOL, Formal Dependability Modeling and Analysis: A Survey

Uses Software

• Isabelle
• ML
• HOL
• MACOM
• SPNP
• VESTA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Reasoning about conditional probabilities in a higher-order-logic theorem prover
• A theory of type polymorphism in programming
• Three Chapters of Measure Theory in Isabelle/HOL
• Formalization of Entropy Measures in HOL
• Formalization of Finite-State Discrete-Time Markov Chains in HOL
• Stochastic Petri Nets
• Keplers komplizierter Weg zur Wahrheit: Von neuen Schwierigkeiten, die „Astronomia Nova”︁ zu lesen
• Stochastic Processes