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

DOI10.1007/978-3-642-24372-1_8zbMATH Open1348.68221OpenAlexW84587889MaRDI QIDQ3172906FDOQ3172906

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) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (4)

• Formalization of Normal Random Variables in HOL
• A compositional framework for Markov processes
• On the formalization of gamma function in HOL
• Formal reasoning about finite-state discrete-time Markov chains in HOL

Uses Software

• HOL
• MACOM
• VESTA

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)