Formally Analyzing Expected Time Complexity of Algorithms Using Theorem Proving

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

• Type: Journal
• Year: 2010
• Where: JCST
• Authors: Osman Hasan, Sofiène Tahar
• Keywords: Algorithms, Expected Time Complexity, Indicator Random Variables, JCST 2010