
›› 2013, Vol. 28 ›› Issue (2): 217231.doi: 10.1007/s1139001313246
• Theoretical Computer Science • Next Articles
Liya Liu, Student Member, IEEE, Osman Hasan, and Sofiène Tahar, Student Member, IEEE
[1] Bhattacharya R N, Waymire E C. Stochastic Processes withApplications (1st edition). WileyInterscience, 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 Publishers, 1998, pp.175204. [3] Steward W J. Introduction to the Numerical Solution ofMarkov 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 probabilisitcsystems. In CRM Monograph Series, Vol.23, AmericanMathematical 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 higherorder logic. In Current Trends in Hardware Verification andAutomated Theorem Proving, Springer, 1989, pp.387439. [8] Liu L, Hasan O, Tahar S. Formalization of finitestatediscretetime Markov chains in HOL. In Proc. the 9th Int.Conf. Automated Technology for Verification and Analysis,Oct. 2011, pp.90104. [9] Knottenbelt W J. Generalised Markovian analysis of timedtransition 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.710. [12] Dingle N J, Harrison P G, Knottenbelt W J. HYDRA ——Hypergraphbased distributed responsetime analyser. InProc. Int. Conf. Parallel and Distributed Processing Technique and Applications, June 2003, pp.215219. [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.142151. [14] Sen K, Viswanathan M, Agha G. VESTA: A statistical modelchecker and analyzer for probabilistic systems. In Proc. the2nd International Conference on the Quantitative Evaluationof Systems, Sept. 2005, pp.251252. [15] Baier C, Haverkort B, Hermanns H et al. Modelcheckingalgorithms for continuoustime Markov chains. IEEE Transactions on Software Engineering, 2003, 29(4): 524541. [16] Nedzusiak A. σfields and probability. Journal of FormalizedMathematics, 1989, 1, pp.16. [17] Bialas J. The σadditive measure theory. Journal of Formalized Mathematics, 1990, 2, pp.17. [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 continuous random variables. In Proc. Formal Methods 2009, Nov.2009, pp.435450. [21] Mhamdi T, Hasan O, Tahar S. Formalization of entropy measures in HOL. In Proc. the 2nd Interactive Theorem Proving,Aug. 2011, pp.233248. [22] H?olzl J, Heller A. Three chapters of measure theory in Isabelle/HOL. In Proc. the 2nd Interactive Theorem Proving,Aug. 2011, pp.135151. [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 HigherOrder Logic. Cambridge University Press, 1993. [25] Milner R. A theory of type polymorphism in programming.J. Computer and System Sciences, 1977, 17(3): 348375. [26] Harrison J. Theorem Proving with the Real Numbers.Springer, 1998. [27] Hasan O, Tahar S. Reasoning about conditional probabilitiesin a higherorderlogic theorem prover. Journal of AppliedLogic, 2011, 9(1): 2340. [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. [30] Trivedi K S. Probability and Statistics with Reliability, Queuing, and Computer Science Applications (2nd edition). JohnWiley & Sons, 2001. [31] ISO/IEC 180007——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 interrogatortag communication protocols. Technical Report, McMaster University,2010. 
No related articles found! 

