Formal reasoning about finite-state discrete-time Markov chains in HOL. (English) Zbl 1280.68124
Summary: 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.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |
| 60J20 | Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) |
References:
| [1] | Bhattacharya R N, Waymire E C. Stochastic Processes with Applications (1st edition). Wiley-Interscience, 1990. · Zbl 0744.60032 |
| [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. · Zbl 0911.65004 |
| [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. · Zbl 1052.90001 |
| [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. · Zbl 1179.68076 |
| [7] | Gordon M J C. Mechanizing programming logics in higher-order logic. In Current Trends in Hardware Verification and Automated Theorem Proving, Springer, 1989, pp.387-439. |
| [8] | Liu L, Hasan O, Tahar S. Formalization of finite-state discrete-time Markov chains in HOL. In Proc. the 9th Int. Conf. Automated Technology for Verification and Analysis, Oct. 2011, pp.90-104. · Zbl 1348.68221 |
| [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. 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 Petri net 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. · doi:10.1109/TSE.2003.1205180 |
| [16] | Nedzusiak A. {\(\sigma\)}-fields and probability. Journal of Formalized Mathematics, 1989, 1, pp.1-6. |
| [17] | Bialas J. The {\(\sigma\)}-additive measure theory. Journal of Formalized Mathematics, 1990, 2, pp.1-7. · Zbl 0853.01008 |
| [18] | Hurd J. Formal verification of probabilistic algorithms [Ph.D. Thesis]. University of Cambridge, UK, 2002. · Zbl 1013.68193 |
| [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. · Zbl 1342.68295 |
| [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. · Zbl 1342.68287 |
| [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. · Zbl 0779.68007 |
| [25] | Milner R. A theory of type polymorphism in programming. J. Computer and System Sciences, 1977, 17(3): 348-375. · Zbl 0388.68003 · doi:10.1016/0022-0000(78)90014-4 |
| [26] | Harrison J. Theorem Proving with the Real Numbers. Springer, 1998. · Zbl 0932.68099 |
| [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. · Zbl 1216.68234 · doi:10.1016/j.jal.2011.01.001 |
| [28] | Norris J R. Markov Cains. Cambridge University Press, 1999. |
| [29] | Prabhu N U. Stochastic Processes: Basic Theory and Its Applications. World Scientific Publisher, 2007. · Zbl 1202.60003 |
| [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. |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
