A Scheme of Model Verification of the Concurrent Discrete Wavelet Transform (DWT) for Image Compression

Authors: Kamrul Hasan Talukder, Koichi Harada

Abstract:

The scientific community has invested a great deal of effort in the fields of discrete wavelet transform in the last few decades. Discrete wavelet transform (DWT) associated with the vector quantization has been proved to be a very useful tool for the compression of image. However, the DWT is very computationally intensive process requiring innovative and computationally efficient method to obtain the image compression. The concurrent transformation of the image can be an important solution to this problem. This paper proposes a model of concurrent DWT for image compression. Additionally, the formal verification of the model has also been performed. Here the Symbolic Model Verifier (SMV) has been used as the formal verification tool. The system has been modeled in SMV and some properties have been verified formally.

Keywords: Computation Tree Logic, Discrete WaveletTransform, Formal Verification, Image Compression, Symbolic Model Verifier.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1061128

References:

[1] Jayant, N. and Noll, P., "Digital Coding of Waveforms: Principles and Applications to Speech and Video", NJ: Prentice-Hall, 1984.
[2] Polikar, R. B. "Wavelet Tutorial Part I, II, III, IV", http://users.rowan.edu/~polikar/WAVELETS/WTtutorial.html, 2003.
[3] David Salomon, "Data Compression: the Complete Reference", 2nd Ed. Springer, 2002.
[4] Michael B.Martin, "Application of Wavelets to image Compression", M.S. Thesis, Blacksburg Virigina, 1999.
[5] Jayant, N., Johnston, J., and Safranek, R., "Signal compression based on models of human perception", in Proc. IEEE, Vol. 81, October 1993, pp. 1385-1422.
[6] Rao, K. R. and Yip, P., "Discrete Cosine Transform: Algorithms, Advantages and Applications", San Diego, CA: Academic, 1990.
[7] Gortler. S., Schröder, P., Cohen, M., and Hanrahan, P., "Wavelet Radiosity", in Proc. SIGGRAPH, 1993, pp. 221-230.
[8] Berman, D., Bartell, J. and Salesin, D., "Multiresolution Painting and Compositing", in Proc. SIGGRAPH, 1994, pp. 85-90.
[9] Finkelstein. A. and Salesin, D., "Multiresolution Curves", in Proc. SIGGRAPH, 1994, pp. 261-268.
[10] Eck, M., DeRose, T., Duchamp, T., Hoppe, H., Lounsberry, M. and Stuetzle, W., "Multiresolution Analysis of Arbitrary Meshes", in Proc. SIGGRAPH, 1995, pp. 173-182.
[11] Lippert, L. and Gross, M., "Fast Wavelet Based Volume Rendering by Accumulation of Transparent Texture Maps", in Proc. EUROGRAPHICS, 1995, pp. 431-443.
[12] Jacobs, C., Finkelstein, A. and Salesin, D., "Fast Multiresolution Image Querying", in Proc. SIGGRAPH, 1995, pp. 277-286.
[13] Myers, Glenford J. "The Art of Software Testing", John Wiley and Sons. ISBN 0-471-04328-1, 1979.
[14] Edmund M. Clakre, Jr. Oma FrumBerg and Doron A. Paled, "Model Checking", The MIT Press, Second Printing, 2000.
[15] Kamrul Hasan Talukder and Koichi Harada, "Development and Performance Analysis of an Adaptive and Scalable Image Compression Scheme with Wavelets", Published in the Proc. of ICICT, BUET, Dhaka, Bangladesh, ISBN: 984-32-3394-8, March 2007, pp. 250-253.
[16] Eric J. Stollnitz, Tony D. Derose and David H. Salesin, "Wavelets for Computer Graphics", Morgan Kaufmann Publishers, Inc., San Francisco. 1996.
[17] Robert L. Cook and Tony DeRose, "Wavelet Noise", ACM Transactions on Graphics, Volume 24, Number 3, Proc. of ACM SIGGRAPH 2005, July 2005, pp. 803-811.
[18] Vetterli, M. and Kovacevic, J., "Wavelets and Subband Coding", Englewood Cliffs, NJ, Prentice Hall, 1995, http://cm.belllabs. com/who/jelena/Book/home.html
[19] G. Beylkin, R. Coifman, and V. Rokhlin, "Fast wavelet transforms and numerical algorithms", I. Communications on Pure and Applied Mathematics, 44(2), March 1991, pp. 141-183.
[20] Colm Mulcahy, "Image compression using the Haar Wavelet transforms", Spelman Science and Math Journal, Vol 1, No 1, April 1997, pp. 22-31.
[21] Fred B. Schneider, "On Concurrent Programming" Inside Risks 94, CACM 41, 4, Apr 1998.
[22] Michael Huth, "Logic in Computer Science: tool based modeling and reasoning about systems", Proceedings of the International Conference on Frontiers in Education 2000, Kansas City, October 2000.
[23] Cadence Berkeley Laboratories, Free download from the website: http://www.kenmcmil.com/smv.html, Califonia, USA. SMV Model Checker, 1999.