Formalization of Finite-State Discrete-Time Markov Chains in HOL

DOI10.1007/978-3-642-24372-1_8zbMath1348.68221OpenAlexW84587889MaRDI QIDQ3172906

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

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 (3)

Formal reasoning about finite-state discrete-time Markov chains in HOL ⋮ Formalization of Normal Random Variables in HOL ⋮ On the formalization of gamma function in HOL

Uses Software

• HOL
• MACOM
• VESTA

This page was built for publication: Formalization of Finite-State Discrete-Time Markov Chains in HOL