Formal reasoning about finite-state discrete-time Markov chains in HOL
DOI10.1007/S11390-013-1324-6zbMATH Open1280.68124OpenAlexW2016818970MaRDI QIDQ2434565FDOQ2434565
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
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
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 (7)
- Formal dependability modeling and analysis: a survey
- Formalization of finite-state discrete-time Markov chains in HOL
- The formalization of discrete Fourier transform in HOL
- Formal verification of tail distribution bounds in the HOL theorem prover
- Markov chains and Markov decision processes in Isabelle/HOL
- Formal reasoning about classified Markov chains in HOL
- Characterization and computation of infinite-horizon specifications over Markov processes
Uses Software
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)
