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

DOI10.1007/S11390-013-1324-6MaRDI QIDQ2434565zbMATH OpenOpenAlexFDO

Authors Liya Liu, Osman Hasan, Sofiène Tahar

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

discrete-time Markov chainhigher-order logicprobability theorytheorem prover

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)

Recommendations

• Formalization of 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
• Theoretical Aspects of Computing - ICTAC 2004
• Model checking finite-horizon Markov chains with probabilistic inference
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• Bisimulations and logical characterizations on continuous-time Markov decision processes
• Relational reasoning for Markov chains in a probabilistic guarded lambda calculus
• Tools and Algorithms for the Construction and Analysis of Systems
• scientific article; zbMATH DE number 1361121

Cites work

• A theory of type polymorphism in programming
• Formalization of entropy measures in HOL
• Formalization of finite-state discrete-time Markov chains in HOL
• scientific article; zbMATH DE number 47283 (Why is no real title available?)
• scientific article; zbMATH DE number 1222285 (Why is no real title available?)
• scientific article; zbMATH DE number 1259143 (Why is no real title available?)
• scientific article; zbMATH DE number 1927425 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Keplers komplizierter Weg zur Wahrheit: Von neuen Schwierigkeiten, die „Astronomia Nova”︁ zu lesen
• Reasoning about conditional probabilities in a higher-order-logic theorem prover
• Stochastic Petri Nets
• Stochastic Processes
• Three chapters of measure theory in Isabelle/HOL

Cited in

(7)

• The formalization of discrete Fourier transform in HOL
• Markov chains and Markov decision processes in Isabelle/HOL
• Formal dependability modeling and analysis: a survey
• Formalization of finite-state discrete-time Markov chains in HOL
• Formal verification of tail distribution bounds in the HOL theorem prover
• Characterization and computation of infinite-horizon specifications over Markov processes
• Formal reasoning about classified Markov chains in HOL

Describes a project that uses

Uses Software

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

This page was built for publication: Formal reasoning about 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 Q2434565)