|  Bhattacharya R N, Waymire E C. Stochastic Processes withApplications (1st edition). Wiley-Interscience, 1990. MacKay D J C. Introduction to Monte Carlo methods. InProc. the NATO Advanced Study Institute on Learning inGraphical Models, Jordan M I (ed.), Kluwer Academic Pub-lishers, 1998, pp.175-204. Steward W J. Introduction to the Numerical Solution ofMarkov Chain. Princeton University Press, 1994. Haas P J. Stochastic Petri Nets: Modelling, Stability, Simu-lation. Springer, 2002. Rutten J, Kwaiatkowska M, Normal G, Parker D. Mathemati-cal techniques for analyzing concurrent and probabilisitcsystems. In CRM Monograph Series, Vol.23, AmericanMathematical Society, 2004. Baier C, Katoen J. Principles of Model Checking (Represen-tation and Mind Series). MIT Press, 2008. Gordon M J C. Mechanizing programming logics in higher-order logic. In Current Trends in Hardware Verification andAutomated Theorem Proving, Springer, 1989, pp.387-439. Liu L, Hasan O, Tahar S. Formalization of finite-statediscrete-time Markov chains in HOL. In Proc. the 9th Int.Conf. Automated Technology for Verification and Analysis,Oct. 2011, pp.90-104. Knottenbelt W J. Generalised Markovian analysis of timedtransition systems [Master's Thesis]. Department of Com-puter Science, University of Cape Town, South Africa, 1996. Jonassen H, Tessmer M D, HannumWH. Task Analysis Met-hods for Instructional Design. Lawrence Erlbaum, 1999. Sczittnick M. MACOM——A tool for evaluating communica-tion systems. In Proc. the 7th Int. Conf. Modelling Tech. and Tools for Comput. Performance Evaluation, May 1994,pp.7-10. Dingle N J, Harrison P G, Knottenbelt W J. HYDRA ——Hypergraph-based distributed response-time analyser. InProc. Int. Conf. Parallel and Distributed Processing Tech-nique and Applications, June 2003, pp.215-219. Ciardo G, Muppala J K, Trivedi K S. SPNP: Stochastic Petrinet package. In Proc. the 3rd Workshop on Petri Nets andPerformance Models, Dec. 1989, pp.142-151. Sen K, Viswanathan M, Agha G. VESTA: A statistical model-checker and analyzer for probabilistic systems. In Proc. the2nd International Conference on the Quantitative Evaluationof Systems, Sept. 2005, pp.251-252. Baier C, Haverkort B, Hermanns H et al. Model-checkingalgorithms for continuous-time Markov chains. IEEE Trans-actions on Software Engineering, 2003, 29(4): 524-541. Nedzusiak A. σ-fields and probability. Journal of FormalizedMathematics, 1989, 1, pp.1-6. Bialas J. The σ-additive measure theory. Journal of Formali-zed Mathematics, 1990, 2, pp.1-7. Hurd J. Formal verification of probabilistic algorithms [Ph.D.Thesis]. University of Cambridge, UK, 2002. Hasan O. Formal probabilistic analysis using theorem proving[Ph.D. Thesis]. Concordia University, Canada, 2008. Hasan O, Abbasi N, Akbarpour B, Tahar S, Akbarpour R.Formal reasoning about expectation properties for continu-ous random variables. In Proc. Formal Methods 2009, Nov.2009, pp.435-450. Mhamdi T, Hasan O, Tahar S. Formalization of entropy mea-sures in HOL. In Proc. the 2nd Interactive Theorem Proving,Aug. 2011, pp.233-248. H?olzl J, Heller A. Three chapters of measure theory in Is-abelle/HOL. In Proc. the 2nd Interactive Theorem Proving,Aug. 2011, pp.135-151. Paulson L C. Isabelle: A Generic Theorem Prover, Springer,1994. Gordon M J C, Melham T F. Introduction to HOL: A Theo-rem Proving Environment for Higher-Order Logic. Cam-bridge University Press, 1993. Milner R. A theory of type polymorphism in programming.J. Computer and System Sciences, 1977, 17(3): 348-375. Harrison J. Theorem Proving with the Real Numbers.Springer, 1998. Hasan O, Tahar S. Reasoning about conditional probabilitiesin a higher-order-logic theorem prover. Journal of AppliedLogic, 2011, 9(1): 23-40. Norris J R. Markov Cains. Cambridge University Press, 1999. Prabhu N U. Stochastic Processes: Basic Theory and Its Ap-plications. World Scientific Publisher, 2007. Trivedi K S. Probability and Statistics with Reliability, Queu-ing, and Computer Science Applications (2nd edition). JohnWiley & Sons, 2001. ISO/IEC 18000-7——Information Technology——Radio fre-quency identification for item management——Part 7: Pa-rameters for active air interface communications at 433 MHz,2008. Nokovic B, Sekerinski E. Analysis of interrogator-tag commu-nication protocols. Technical Report, McMaster University,2010.