Liya Liu,
Osman Hasan,
and Sofiène Tahar.
Formal Reasoning About Finite-State Discrete-Time Markov Chains in HOL.
Journal of Computer Science and Technology,
28(2):217-231,
March 2013.
ISSN: 1860-4749.
Keyword(s): probability,
verification.
Abstract: |
Markov chains are extensively used in modeling different aspects of engineering and scientific systems, such as performance of algorithms and reliability of systems. Different techniques have been developed for analyzing Markovian models, for example, Markov Chain Monte Carlo based simulation, Markov Analyzer, and more recently probabilistic model-checking. However, these techniques either do not guarantee accurate analysis or are not scalable. Higher-order-logic theorem proving is a formal method that has the ability to overcome the above mentioned limitations. However, it is not mature enough to handle all sorts of Markovian models. In this paper, we propose a formalization of Discrete-Time Markov Chain (DTMC) that facilitates formal reasoning about time-homogeneous finite-state discrete-time Markov chain. In particular, we provide a formal verification on some of its important properties, such as joint probabilities, Chapman-Kolmogorov equation, reversibility property, using higher-order logic. To demonstrate the usefulness of our work, we analyze two applications: a simplified binary communication channel and the Automatic Mail Quality Measurement protocol. |
@article{liuFormalReasoningFiniteState2013,
title = {Formal {{Reasoning About Finite}}-{{State Discrete}}-{{Time Markov Chains}} in {{HOL}}},
author = {Liu, Liya and Hasan, Osman and Tahar, Sofi{\`e}ne},
year = {2013},
month = mar,
volume = {28},
pages = {217--231},
issn = {1860-4749},
doi = {10.1007/s11390-013-1324-6},
abstract = {Markov chains are extensively used in modeling different aspects of engineering and scientific systems, such as performance of algorithms and reliability of systems. Different techniques have been developed for analyzing Markovian models, for example, Markov Chain Monte Carlo based simulation, Markov Analyzer, and more recently probabilistic model-checking. However, these techniques either do not guarantee accurate analysis or are not scalable. Higher-order-logic theorem proving is a formal method that has the ability to overcome the above mentioned limitations. However, it is not mature enough to handle all sorts of Markovian models. In this paper, we propose a formalization of Discrete-Time Markov Chain (DTMC) that facilitates formal reasoning about time-homogeneous finite-state discrete-time Markov chain. In particular, we provide a formal verification on some of its important properties, such as joint probabilities, Chapman-Kolmogorov equation, reversibility property, using higher-order logic. To demonstrate the usefulness of our work, we analyze two applications: a simplified binary communication channel and the Automatic Mail Quality Measurement protocol.},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4367-Liu et al (2013) - Formal Reasoning About Finite-State Discrete-Time Markov Chains in HOL.pdf},
journal = {Journal of Computer Science and Technology},
keywords = {probability,verification},
number = {2}
}
Lee Pike,
Nis Wegmann,
Sebastian Niller,
and Alwyn Goodloe.
Copilot: Monitoring Embedded Systems.
Innovations in Systems and Software Engineering,
9(4):235-255,
December 2013.
ISSN: 1614-5046, 1614-5054.
Keyword(s): Haskell,
streams,
verification.
@article{pikeCopilotMonitoringEmbedded2013,
title = {Copilot: Monitoring Embedded Systems},
author = {Pike, Lee and Wegmann, Nis and Niller, Sebastian and Goodloe, Alwyn},
year = {2013},
month = dec,
volume = {9},
pages = {235--255},
issn = {1614-5046, 1614-5054},
doi = {10.1007/s11334-013-0223-x},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4376-Pike et al (2013) - Copilot.pdf},
journal = {Innovations in Systems and Software Engineering},
keywords = {Haskell,streams,verification},
number = {4}
}