[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.