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

DOI10.1007/S11390-013-1324-6zbMATH Open1280.68124OpenAlexW2016818970MaRDI QIDQ2434565FDOQ2434565

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

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

zbMATH Keywords

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

Cites Work

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

Cited In (3)

• Formal Dependability Modeling and Analysis: A Survey
• The formalization of discrete Fourier transform in HOL
• Formal verification of tail distribution bounds in the HOL theorem prover

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)