| [1] Bhattacharya R N, Waymire E C. Stochastic Processes withApplications (1st edition). Wiley-Interscience, 1990.[2] 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.[3] Steward W J. Introduction to the Numerical Solution ofMarkov Chain. Princeton University Press, 1994.[4] Haas P J. Stochastic Petri Nets: Modelling, Stability, Simu-lation. Springer, 2002.[5] 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.[6] Baier C, Katoen J. Principles of Model Checking (Represen-tation and Mind Series). MIT Press, 2008.[7] 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.[8] 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.[9] Knottenbelt W J. Generalised Markovian analysis of timedtransition systems [Master's Thesis]. Department of Com-puter Science, University of Cape Town, South Africa, 1996.[10] Jonassen H, Tessmer M D, HannumWH. Task Analysis Met-hods for Instructional Design. Lawrence Erlbaum, 1999.[11] 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.[12] 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.[13] 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.[14] 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.[15] 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.[16] Nedzusiak A. σ-fields and probability. Journal of FormalizedMathematics, 1989, 1, pp.1-6.[17] Bialas J. The σ-additive measure theory. Journal of Formali-zed Mathematics, 1990, 2, pp.1-7.[18] Hurd J. Formal verification 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 continu-ous random variables. In Proc. Formal Methods 2009, Nov.2009, pp.435-450.[21] 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.[22] 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.[23] Paulson L C. Isabelle: A Generic Theorem Prover, Springer,1994.[24] Gordon M J C, Melham T F. Introduction to HOL: A Theo-rem Proving Environment for Higher-Order Logic. Cam-bridge 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 probabilitiesin a higher-order-logic theorem prover. Journal of AppliedLogic, 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 Ap-plications. World Scientific Publisher, 2007.[30] Trivedi K S. Probability and Statistics with Reliability, Queu-ing, and Computer Science Applications (2nd edition). JohnWiley & Sons, 2001.[31] 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.[32] Nokovic B, Sekerinski E. Analysis of interrogator-tag commu-nication protocols. Technical Report, McMaster University,2010. |