Liu, Liya, Hasan, Osman and Tahar, Sofiène (2013) Formal Reasoning About Finite-State Discrete-Time Markov Chains in HOL. Journal of Computer Science and Technology, 28 (2). pp. 217-231. ISSN 1000-9000
Preview |
Text (application/pdf)
384kBJCST-2013.pdf - Accepted Version |
Official URL: http://dx.doi.org/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.
| Divisions: | Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering |
|---|---|
| Item Type: | Article |
| Refereed: | Yes |
| Authors: | Liu, Liya and Hasan, Osman and Tahar, Sofiène |
| Journal or Publication: | Journal of Computer Science and Technology |
| Date: | 2013 |
| Digital Object Identifier (DOI): | 10.1007/s11390-013-1324-6 |
| Keywords: | discrete-time Markov chain; higher-order logic; probability theory; theorem prover |
| ID Code: | 977339 |
| Deposited By: | Danielle Dennie |
| Deposited On: | 11 Jun 2013 19:56 |
| Last Modified: | 18 Jan 2018 17:44 |
References:
[1] Bhattacharya R N, Waymire E C. Stochastic Processes with Applications (1st edition). Wiley-Interscience, 1990.[2] MacKay D J C. Introduction to Monte Carlo methods. In Proc. the NATO Advanced Study Institute on Learning in Graphical Models, Jordan M I (ed.), Kluwer Academic Publishers, 1998, pp.175-204.
[3] Steward W J. Introduction to the Numerical Solution of Markov Chain. Princeton University Press, 1994.
[4] Haas P J. Stochastic Petri Nets: Modelling, Stability, Simulation. Springer, 2002.
[5] Rutten J, Kwaiatkowska M, Normal G, Parker D. Mathematical techniques for analyzing concurrent and probabilisitc systems. In CRM Monograph Series, Vol.23, American Mathematical Society, 2004.
[6] Baier C, Katoen J. Principles of Model Checking Representation and Mind Series). MIT Press, 2008.
[7] Gordon M J C. Mechanizing programming logics in higher-order logic. In Current Trends in Hardware Verication and Automated Theorem Proving, Springer, 1989, pp.387-439.
[8] Liu L, Hasan O, Tahar S. Formalization of nite-state discrete-time Markov chains in HOL. In Proc. the 9th Int. Conf. Automated Technology for Veri¯cation and Analysis, Oct. 2011, pp.90-104.
[9] Knottenbelt W J. Generalised Markovian analysis of timed transition systems [Master's Thesis]. Department of computer Science, University of Cape Town, South Africa, 1996.
[10] Jonassen H, Tessmer M D, HannumWH. Task Analysis Methods for Instructional Design. Lawrence Erlbaum, 1999.
[11] Sczittnick M. MACOM | A tool for evaluating communication systems. In Proc. the 7th Int. Conf. Modelling Tech. Liya Liu et al.: Formal Reasoning About Finite-State DTMC in HOL 231 and Tools for Comput. Performance Evaluation, May 1994, pp.7-10.
[12] Dingle N J, Harrison P G, Knottenbelt W J. HYDRA Hypergraph-based distributed response-time analyser. In Proc. Int. Conf. Parallel and Distributed Processing Technique and Applications, June 2003, pp.215-219.
[13] Ciardo G, Muppala J K, Trivedi K S. SPNP: Stochastic Petrinet package. In Proc. the 3rd Workshop on Petri Nets and Performance Models, Dec. 1989, pp.142-151.
[14] Sen K, Viswanathan M, Agha G. VESTA: A statistical Model-checker and analyzer for probabilistic systems. In Proc. the 2nd International Conference on the Quantitative Evaluation of Systems, Sept. 2005, pp.251-252.
[15] Baier C, Haverkort B, Hermanns H et al. Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering, 2003, 29(4): 524-541.
[16] Nedzusiak A. ¾-¯elds and probability. Journal of Formalized Mathematics, 1989, 1, pp.1-6.
[17] Bialas J. The ¾-additive measure theory. Journal of Formalized Mathematics, 1990, 2, pp.1-7.
[18] Hurd J. Formal veri¯cation of probabilistic algorithms [Ph.D. Thesis]. University of Cambridge, UK, 2002.
[19] Hasan O. Formal probabilistic analysis using theorem proving [Ph.D. Thesis]. Concordia University, Canada, 2008.
[20] Hasan O, Abbasi N, Akbarpour B, Tahar S, Akbarpour R.
Formal reasoning about expectation properties for continuous random variables. In Proc. Formal Methods 2009, Nov. 2009, pp.435-450.
[21] Mhamdi T, Hasan O, Tahar S. Formalization of entropy measures in HOL. In Proc. the 2nd Interactive Theorem Proving, Aug. 2011, pp.233-248.
[22] HÄolzl J, Heller A. Three chapters of measure theory in Isabelle/HOL. In Proc. the 2nd Interactive Theorem Proving, Aug. 2011, pp.135-151.
[23] Paulson L C. Isabelle: A Generic Theorem Prover, Springer, 1994.
[24] Gordon M J C, Melham T F. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, 1993.
[25] Milner R. A theory of type polymorphism in programming. J. Computer and System Sciences, 1977, 17(3): 348-375.
[26] Harrison J. Theorem Proving with the Real Numbers. Springer, 1998.
[27] Hasan O, Tahar S. Reasoning about conditional probabilities in a higher-order-logic theorem prover. Journal of Applied Logic, 2011, 9(1): 23-40.
[28] Norris J R. Markov Cains. Cambridge University Press, 1999.
[29] Prabhu N U. Stochastic Processes: Basic Theory and Its Applications. World Scienti¯c Publisher, 2007.
[30] Trivedi K S. Probability and Statistics with Reliability, Queuing, and Computer Science Applications (2nd edition). John Wiley & Sons, 2001.
[31] ISO/IEC 18000-7 | Information Technology | Radio frequency identification for item management | Part 7: Parameters for active air interface communications at 433 MHz, 2008.
[32] Nokovic B, Sekerinski E. Analysis of interrogator-tag communication protocols. Technical Report, McMaster University, 2010.
Repository Staff Only: item control page
Download Statistics
Download Statistics