›› 2010, Vol. 25 ›› Issue (6): 1305-1320.doi: 10.1007/s11390-010-1103-6

• Regular Papers • Previous Articles     Next Articles

Formally Analyzing Expected Time Complexity of Algorithms Using Theorem Proving

Osman Hasan and Sofiéne Tahar, Senior Member, IEEE, Member, ACM   

  1. Department of Electrical and Computer Engineering, Concordia University, Montreal, Canada
  • Received:2009-06-20 Revised:2010-07-26 Online:2010-11-01 Published:2010-11-01
  • About author:Osman Hasan received the B.Eng. (Hons.) degree from the N-W.F.P University of Engineering and Technology, Pakistan, in 1997, and the M.Eng. and Ph.D. degrees from Concordia University, Montreal, QC, Canada, in 2001 and 2008, respectively. He served as an ASIC design Engineer from 2001 to 2003 in the industry prior to joining Concordia University in 2004 for his Ph.D. Currently, he is a research associate at the Hardware Verification Group, Concordia University. His current research interests include formal methods, higher-order-logic theorem proving and probabilistic analysis.
    Sofiéne Tahar received the Diploma degree in computer engineering from the University of Darmstadt, Germany, in 1990, and the Ph.D. degree with distinction in computer science from the University of Karlsruhe, Germany, in 1994. Currently, he is a professor and research chair in formal verification of system-on-chip at the Department of Electrical and Computer Engineering, Concordia University. His research interests are in the areas of formal hardware verification, system-on-chip verification, analog and mixed signal circuits verification, and probabilistic, statistical and reliability analysis of systems. Dr. Tahar, a professional engineer in the Province of Quebec, is the founder and director of the Hardware Verification Group at Concordia University. In 2007, he was named University Research Fellow upon receiving Concordia University’s Senior Research Award.

Probabilistic techniques are widely used in the analysis of algorithms to estimate the computational complexity of algorithms or a computational problem. Traditionally, such analyses are performed using paper-and-pencil proofs and the results are sometimes validated using simulation techniques. These techniques are informal and thus may result in an inaccurate analysis. In this paper, we propose a formal technique for analyzing the expected time complexity of algorithms using higher-order-logic theorem proving. The approach calls for mathematically modeling the algorithm along with its inputs, using indicator random variables, in higher-order logic. This model is then used to formally reason about the expected time complexity of the underlying algorithm in a theorem prover. The paper includes the higher-order-logic formalization of indicator random variables, which are fundamental to the proposed infrastructure. In order to illustrate the practical effectiveness and utilization of the proposed infrastructure, the paper also includes the analysis of algorithms for three well-known problems, i.e., the hat-check problem, the birthday paradox and the hiring problem.

[1] Knuth D E. The Art of Computer Programming. Addison-Wesley Professional, 1997.

[2] Whittle P. Probability via Expectation. Springer, 2000.

[3] Kozen D. A probabilistic PDL. Journal of Computer and System Sciences, 1985, 30(2): 162-178.

[4] Jones C. Probabilistic Non-Determinism
[Ph.D. Dissertation]. University of Edinburgh, Edinburgh, UK, 1990.

[5] Mitzenmacher M, Upfal E. Probability and Computing. Cambridge University Press, 2005.

[6] Whitney M . Exploring the birthday paradox using a Monte Carlo simulation and graphing calculators. Mathematics Teacher, 2001, 94(4): 258-262.

[7] Hastingsr K . Introduction to Probability with {M}athematica. Chapman and Hall/CRC, 2000.

[8] Devroye L. Non-Uniform Random Variate Generation. Springer-Verlag, 1986.

[9] MacKay D J C. Introduction to Monte Carlo methods. In NATO Advanced Study Institute on Learning in Graphical Models, Erice, Italy, 1998, pp.175-204.

[10] Flajolet P, Salvy B, Zimmermann P. Automatic average-case analysis of algorithms. Theoretical Computer Science, 1991, 79(1): 37-109.

[11] Adams A, Gottliebsen H, Linton S A, Martin U. Automated theorem proving in support of computer algebra: Symbolic definite integration as a case study. In Proc. Symbolic and Algebraic Computation, Vancouver, Canada, July 28-31, 1999, pp.253-260.

[12] Hall A. Realising the benefits of formal methods. J. Universal Computer Science, 2007, 13(5): 669-678.

[13] Clarke E, Grumberg O, Long D. Verification tools for finite state concurrent systems. In Proc.REX School/Symp. A Decade of Concurrency --- Reflections and Perspectives, Noordwijkerhout, The Neitherlands, Jun. 1-4, 1993, pp.124-175.

[14] Harrison J. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009.

[15] Hurd J. Formal verification of probabilistic algorithms
[Ph.D. Dissertation]. University of Cambridge, Cambridge, UK, 2002.

[16] McIver A K, Morgan C C. Abstraction, Refinement and Proof for Probabilistic Systems. Spriger, 2005.

[17] Hurd J, McIver A, Morgan C. Probabilistic guarded commands mechanized in HOL. Theoretical Computer Science, 2005, 346(1): 96-112.

[18] Cormen T H, Leiserson C E, Rivest R L, Stein C. Introduction to Algorithms. The MIT Press, 2001.

[19] Hasan O, Tahar S. Using theorem proving to verify expectation and variance for discrete random variables. Journal of Automated Reasoning, 2008, 41(3/4): 295-323.

[20] Grinstead C M, Snell J L. Introduction to Probability. American Mathematical Society, 1997.

[21] Mckinney E H. Generalized birthday problem. The American Mathematical Monthly, 1966, 73(4): 385-387.

[22] de Montmort P R. Essay dÁnalyse sur les Jeux de {H}azard. Published anonymously, 1708.

[23] Euler L. Calcul de la probabilite dans le jeu de rencontre. Memoires de lAcademie des Sciences de Berlin, 1753, (7): 255-270.

[24] P S de Laplace. Theorie Analytique des Probabilites. Published anonymously, 1812.

[25] Takacs L. The problem of coincidences. Archive for History of Exact Sciences, 1980, 3(21): 229-244.

[26] Akutsu T. On determining the congruity of point sets in higher dimensions. In Proc. International Symposium on Algorithms and Computation, Beijing, China, Aug. 25-27, 1994, pp.38-46.

[27] Flajolet P, Gardy D, Thimonier L. Birthday paradox, coupon collectors, caching algorithms and self-organizing search. Discrete Applied Mathematics, 1992, 39(3): 207-229.

[28] Gazit H, Reif J H. A randomized parallel algorithm for planar graph isomorphism. Journal of Algorithms, 1998, 28(2): 290-314.

[29] Stinson D R. Cryptography, Theory and Practice. CRC Press, 2006.

[30] Gardner M. Mathematical games. Scientific American, 1960, 202: 150-153.

[31] Freeman P R. The secretary problem and its extensions: {A} review. International Statistical Review, 1983, 51(2): 189-206.

[32] Kleinberg R. A multiple-choice secretary algorithm with applications to online auctions. In Proc. ACM-SIAM Symposium on Discrete Algorithms, Vancouver, Canada, Jan. 23-25, 2005, pp.630-631.

[33] Babaioff M, Immorlica N, Kleinberg R. Matroids, secretary problems, and online mechanisms. In Proc. ACM-SIAM Symposium on Discrete Algorithms, New Orleans, USA, Jan. 7-9, 2007, pp.434-443.

[34] Broder A Z, Kirsch A, Kumar R, Mitzenmacher M, Upfal E, Vassilvitskii S. The hiring problem and lake wobegon strategies. In Proc. ACM-SIAM Symposium on Discrete Algorithms, San Francisco, USA, Jan. 20-22, 2008, pp.1184-1193.

[35] Gordon M J C, Melham T F. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, 1993.

[36] Paulson L C. Isabelle: A Generic Theorem Prover. Springer, 1994.

[37] CoQ. http://pauillac.inria.fr/coq/, 2009.

[38] PVS. http://pvs.csl.sri.com, 2009.

[39] Nedzusiak A. σ-fields and probability. Journal of Formalized Mathematics, 1989, 1.

[40] Bialas J. The σ-additive measure theory. Journal of formalized Mathematics, 1990, 2.

[41] Hasan O, Tahar S. Formalization of the continuous probability distributions. In Proc. Int. Conf. Automated Deduction, Bremen, Germany, Jul. 17-20, 2007, pp.3-18.

[42] Hasan O, Tahar S. Performance analysis and functional verification of the stop-and-wait protocol in HOL. Journal of Automated Reasoning, 2009, 42(1): 1-33.

[43] Hasan O, Tahar S. Performance analysis of ARQ protocols using a theorem prover. In Proc. International Symposium on Performance Analysis of Systems and Software, Austin, USA, April 20-22, 2008, pp.85-94.

[44] Hasan O, Tahar S. Performance analysis of wireless systems using theorem proving. In Proc. the First International Workshop on Formal Methods for Wireless Systems, Toronto, Canada, Aug. 19-22, 2008, pp.3-18.

[45] Hasan O, Abbasi N, Tahar S. Formal probabilistic analysis of stuck-at faults in reconfigurable memory arrays. In Proc. Int. Conf. Integrated Formal Methods, Düsseldorf, Germany, Feb. 16-19, 2009, pp.277-291.

[46] Baier C, Haverkort B, Hermanns H, Katoen J P. Model checking algorithms for continuous time Markov chains. IEEE Transactions on Software Engineering, 2003, 29(4): 524-541.

[47] Rutten J, Kwaiatkowska M, Normal G, Parker D. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. Vol.23 of CRM Monograph Series, American Mathematical Society, 2004.

[48] Baier C, Katoen J P. Principles of Model Checking. MIT Press, 2008.

[49] L de Alfaro. Formal verification of probabilistic systems
[Ph.D. Dissertation]. Stanford University, Stanford, USA, 1997.

[50] Parker D. Implementation of symbolic model checking for probabilistic system
[Ph.D. Dissertation]. University of Birmingham, Birmingham, UK, 2001.

[51] Kwiatkowska M, Norman G, Parker D. Quantitative analysis with the probabilistic model checker PRISM. Electronic Notes in Theoretical Computer Science, 2005, 153(2): pp.5-31.

[52] Sen K, Viswanathan M, Agha G. VESTA: A statistical model-checker and analyzer for probabilistic systems. In Proc. IEEE International Conference on the Quantitative Evaluation of Systems, Torino, Italy, Sept. 19-22, 2005, pp.251-252.

[53] Norman G. Validation of Stochastic Systems: A Guide to Current Research, vol. 2925 of LNCS (Tutorial Volume), Chapter Analyzing Randomized Distributed Algorithms, Springer, 2004, pp.384-418.

[54] Church A. A formulation of the simple theory of types. Journal of Symbolic Logic, 1940, 5: 56-68.

[55] Milner R. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 1977, 17: 348-375.

[56] Paulson L C. ML for the Working Programmer. Cambridge University Press, 1996.

[57] Harrison J. Formalized mathematics. Technical Report 36, Turku Centre for Computer Science, Finland, 1996.

[58] Harrison J. Theorem Proving with the Real Numbers. Springer, 1998.

No related articles found!
Full text



[1] Liu Mingye; Hong Enyu;. Some Covering Problems and Their Solutions in Automatic Logic Synthesis Systems[J]. , 1986, 1(2): 83 -92 .
[2] Chen Shihua;. On the Structure of (Weak) Inverses of an (Weakly) Invertible Finite Automaton[J]. , 1986, 1(3): 92 -100 .
[3] Gao Qingshi; Zhang Xiang; Yang Shufan; Chen Shuqing;. Vector Computer 757[J]. , 1986, 1(3): 1 -14 .
[4] Chen Zhaoxiong; Gao Qingshi;. A Substitution Based Model for the Implementation of PROLOG——The Design and Implementation of LPROLOG[J]. , 1986, 1(4): 17 -26 .
[5] Huang Heyan;. A Parallel Implementation Model of HPARLOG[J]. , 1986, 1(4): 27 -38 .
[6] Min Yinghua; Han Zhide;. A Built-in Test Pattern Generator[J]. , 1986, 1(4): 62 -74 .
[7] Tang Tonggao; Zhao Zhaokeng;. Stack Method in Program Semantics[J]. , 1987, 2(1): 51 -63 .
[8] Min Yinghua;. Easy Test Generation PLAs[J]. , 1987, 2(1): 72 -80 .
[9] Zhu Hong;. Some Mathematical Properties of the Functional Programming Language FP[J]. , 1987, 2(3): 202 -216 .
[10] Li Minghui;. CAD System of Microprogrammed Digital Systems[J]. , 1987, 2(3): 226 -235 .

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
E-mail: jcst@ict.ac.cn
  Copyright ©2015 JCST, All Rights Reserved