×

Formal analysis of optical systems. (English) Zbl 1302.68245

Summary: Optical systems are becoming increasingly important by resolving many bottlenecks in today’s communication, electronics, and biomedical systems. However, given the continuous nature of optics, the inability to efficiently analyze optical system models using traditional paper-and-pencil and computer simulation approaches sets limits especially in safety-critical applications. In order to overcome these limitations, we propose to employ higher-order-logic theorem proving as a complement to computational and numerical approaches to improve optical model analysis in a comprehensive framework. The proposed framework allows formal analysis of optical systems at four abstraction levels, i.e., ray, wave, electromagnetic, and quantum.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68W30 Symbolic computation and algebraic computation
78A05 Geometric optics
78A25 Electromagnetic theory (general)
81V80 Quantum optics
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Allen, L., Angel, R., Rodney, G.A., Mangus, J.D., Shannon, R.R. , Spoelhof, Ch.P.: The Hubble Space Telescope Optical System Failure Report. Technical Report, NASA TM-103443, Washington, DC, November 1990
[2] Formal analysis of optical systems, Hardware Verification Group, Concordia University. http://hvg.ece.concordia.ca/projects/optics/ (2014). Accessed 20 Mar 2014
[3] Mathematica. http://www.wolfram.com/ (2014). Accessed 20 Mar 2014
[4] Mathlink Link. http://reference.wolfram.com/mathematica/guide/MathLinkAPI.html (2014). Accessed 20 Mar 2014
[5] Matlab–codev toolkit. http://opensource.gsfc.nasa.gov/projects/Matlab_Code_V/ (2014). Accessed 20 Mar 2014
[6] Matlab–zemax toolkit. http://opensource.gsfc.nasa.gov/projects/Matlab_Zemax/ (2014). Accessed 20 Mar 2014
[7] OpenMath Content Dictionaries. http://www.openmath.org/cdnames.html (2014). Accessed 20 Mar 2014
[8] OpenMath Content Dictionary: linalgeig1. http://www.win.tue.nl/\(\sim\)amc/oz/om/cds/linalgeig1.xml (2014). Accessed 20 Mar 2014
[9] Overview of OpenMath. http://www.openmath.org/overview/index.html (2014). Accessed 20 Mar 2014
[10] Rezonator. http://www.rezonator.orion-project.org/ (2014). Accessed 20 Mar 2014
[11] Source Code of the Phrasebook Mathematica-OpenMath. http://mathdox.org/new-web/index.html (2014). Accessed 20 Mar 2014
[12] Zemax. https://www.radiantzemax.com/ (2014). Accessed 20 Mar 2014
[13] Baaske M., Vollmer F.: Optical resonator biosensors: molecular diagnostic and nanoparticle detection on an integrated platform. Chem. Phys. Chem. 13(2), 427–436 (2012)
[14] Ballarin, C., Homann, K., Calmet, J.: Theorems and algorithms: an interface between Isabelle and Maple. In: Levelt, A.H.M. (ed.) Proceedings of the 1995 International Symposium on Symbolic and Algebraic Computation, ISSAC ’95, pp. 150–157. ACM, New York, USA (1995) · Zbl 0922.68080
[15] Born M., Wolf E.: Principles of Optics Electromagnetic: Theory of Propagation, Interference and Diffraction of Light. Cambridge University Press, Cambridge, UK (1999) · Zbl 0086.41704
[16] Buchberger B., Craciun A., Jebelean T., Kovacs L., Kutsia T., Nakagawa K., Piroi F., Popov N., Robu J., Rosenkranz M., Windsteiger W.: Theorema: towards computer-aided mathematical theory exploration. J. Appl. Logic 4(4), 470–504 (2006) · Zbl 1107.68095
[17] Caprotti, O., Cohen, A.M.: Connecting proof checkers and computer algebra using OpenMath. In: Bertot, Y., Dowek, G., Thery, L., Hirschowitz, A., Paulin, C. (eds.) Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 1690, pp. 109–112. Springer, Berlin, Heidelberg (1999)
[18] Caprotti O., Cohen A.M., Riem M.: JAVA phrasebooks for computer algebra and automated deduction. SIGSAM Bull. 34, 33–37 (2000)
[19] Chen K.J., Chen H.C., Tsai K.A., et. al.: Light-emitting devices: resonant-enhanced full-color emission of quantum-dot-based display technology using a pulsed spray method. Adv. Funct. Mater. 22(24), 5137–5137 (2012)
[20] Cheng Q., Cui T.J., Zhang C.: Waves in planar waveguide containing chiral nihility metamaterial. Opt. Commun. 274, 317–321 (2007)
[21] Dirac P.A.M.: The fundamental equations of quantum mechanics. Proc. R. Soc. A: Math. Phys. Eng. Sci. 109(752), 642–653 (1925) · JFM 51.0729.01
[22] Feynman R.: Simulating physics with computers. Int. J. Theor. Phys. 21, 467–488 (1982)
[23] Garg R.: Analytical and Computational Methods in Electromagnetics. Artech House, Norwood, MA, USA (2008) · Zbl 1209.78001
[24] Gordon M.J.C., Melham T.F.: Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge Press, Cambridge (1993) · Zbl 0779.68007
[25] Griffiths D.J.: Introduction to Electrodynamics. Pearson Prentice Hall, Upper Saddle River, NJ, USA (1999) · Zbl 0933.92028
[26] Griffiths D.J.: Introduction to Quantum Mechanics. Pearson Prentice Hall, Upper Saddle River, NJ, USA (2005)
[27] Hadfield R.H.: Single-Photon Detectors for Optical Quantum Information Applications. Nat. Photonics 3, 696–705 (2009)
[28] Hales, T.C.: Introduction to the flyspeck project. In: Mathematics, Algorithms, Proofs, volume 05021 of Dagstuhl Seminar Proceedings (2005)
[29] Harrison J.: HOL light: a tutorial introduction. In: Formal Methods in Computer-Aided Design, volume 1166 of LNCS, pp. 265–269. Springer (1996)
[30] Harrison, J.: Theorem Proving with the Real Numbers (Distinguished dissertations). Springer, Verlag (1998) · Zbl 0932.68099
[31] Harrison, J.: A HOL theory of Euclidean space. In: Theorem Proving in Higher Order Logics, volume 3603 of LNCS, pp. 114–129. Springer (2005) · Zbl 1152.68520
[32] Harrison, J.: Formalizing basic complex analysis. In: From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, volume 10(23) of Studies in Logic, Grammar and Rhetoric, pp. 151–165. University of Białystok (2007)
[33] Harrison J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Cambridge, UK (2009) · Zbl 1178.03001
[34] Harrison, J.: HOL light: an overview. In: Theorem Proving in Higher Order Logics, volume 5674 of Lecture Notes in Computer Science, pp. 60–66. Springer (2009) · Zbl 1252.68255
[35] Harrison J., Théry L.: A skeptic’s approach to combining HOL and maple. J. Autom. Reason. 21, 279–294 (1998) · Zbl 0916.68142
[36] Hasan, O., Afshar, S.KH., Tahar, S.: Formal analysis of optical waveguides in Hol. In: Theorem Proving in Higher Order Logics, volume 5674 of LNCS, pp. 228–243. Springer (2009) · Zbl 1252.68256
[37] Hayes P.R., O’Keefe M.T., Woodward P.R., Gopinath A.: Higher-order-compact time domain numerical simulation of optical waveguides. Opt. Quantum Electron. 31(9-10), 813–826 (1999)
[38] Heinbockel J.H.: Numerical Methods For Scientific Computing. Trafford, Victoria, BC, Canada (2004)
[39] Hölzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, Ch., Pichardie, D. (eds.) Interactive theorem proving. Lecture Notes in Computer Science, vol. 7998, pp. 279–294. Springer, Berlin, Heidelberg (2013) · Zbl 1317.68213
[40] Johnson S.G., Joannopoulos J.D.: Block-iterative frequency domain methods for Maxwell’s equations in a planewave basis. Opt. Expr. 8(3), 173–190 (2001)
[41] Clarke E.M. Jr., Grumberg O., Peled D.A.: Model Checking. The MIT Press, Cambridge, MA, USA (1999)
[42] Afshar S.K., Aravantinos V.: A HOL-Light library for vectors of complex numbers. http://hvg.ece.concordia.ca/code/hol-light/complex-vectors (2014). Accessed 20 Mar 2014
[43] Kaliszyk, C., Wiedijk, F.: Certified computer algebra on top of an interactive theorem prover. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Towards Mechanized Mathematical Assistants. Lecture Notes in Computer Science, vol. 4573, pp. 94–105. Springer, Berlin, Heidelberg (2007) · Zbl 1202.68382
[44] Karimi M., Abedi K., Zavvari M.: Resonant cavity enhanced quantum ring photodetector at 20 {\(\mu\)}m wavelength. Opt. Quantum Electron. 45(12), 1249–1258 (2013)
[45] Kogelnik H., Li T.: Laser beams and resonators. Appl. Opt. 5(10), 1550–1567 (1966)
[46] LASCAD. http://www.las-cad.com/ (2014). Accessed 20 Mar 2014
[47] Leonhardt U.: Quantum physics of simple optical instruments. Rep. Progr. Phys. 66(7), 1207 (2003)
[48] Liu Y., Sarris C.D.: Fast time-domain simulation of optical waveguide structures with a multilevel dynamically adaptive mesh refinement FDTD approach. J. Lightwave Technol. 24(8), 3235–3247 (2006)
[49] Lounis B., Orrit M.: Single-photon sources. Rep. Progr. Phys. 68(5), 1129–1179 (2005)
[50] Mahmoud, M.Y., Aravantinos, V., Tahar, S.: Formalization of infinite dimension linear spaces with application to quantum theory. In: NASA Formal Methods, volume 7871 of LNCS, pp. 413–427. Springer (2013)
[51] Malak, M., Pavy, N., Marty, F., Peter, Y., Liu, A.Q., Bourouina, T.: Stable, high-Q Fabry–Perot resonators with long cavity based on curved, all-silicon, high reflectance mirrors. In: IEEE International Conference on Micro Electro Mechanical Systems, pp. 720–723 (2011)
[52] Mandel L., Wolf E.: Optical Coherence and Quantum Optics. Cambridge University Press, Cambridge, UK (1995)
[53] Mathscheme. http://www.cas.mcmaster.ca/research/mathscheme/ (2014). Accessed 20 Mar 2014
[54] MATLAB. http://www.mathworks.com/products/matlab/ (2014). Accessed 20 Mar 2014
[55] Mookherjea S.: Analysis of optical pulse propagation with two-by-two (ABCD) matrices. Phys. Rev. E 64(016611), 1–10 (2001)
[56] MuPAD. http://www.mathworks.com/discovery/mupad.html (2014). Accessed 20 Mar 2014
[57] Nakazawa M., Kubota H., Sahara A., Tamura K.: Time-domain ABCD matrix formalism for laser mode-locking and optical pulse transmission. IEEE J. Quantum Electron. 34(7), 1075–1081 (1998)
[58] Naqvi, A.: Comments on waves in planar waveguide containing chiral nihility metamaterial. Opt. Commun. 284:215–216, Elsevier (2011)
[59] Institute of Quantum Optics at Leibniz University of Hannover. General directives for safety in the institute of quantum optics. http://www.iqo.uni-hannover.de/fileadmin/institut/pdf/job%20security/3._Sicherheitmerkblatt06012014_engl.pdf (2014). Accessed 20 Mar 2014
[60] Pereira A., Ostermann F., Cavalcanti C.: On the use of a virtual Mach–Zehnder interferometer in the teaching of quantum mechanics. Phys. Educ. 44(3), 281 (2009)
[61] Pollock C.R.: Fundamentals of Optoelectronics. Tom Casson, Chicago, USA (1995)
[62] Prieto H., Dalmas S., Papegay Y.: Mathematica as an OpenMath application. SIGSAM Bull. 34, 22–26 (2000)
[63] Ralph T.C., Gilchrist A., Milburn G.J., Munro W.J., Glancy S.: Quantum computation with optical coherent states. Phys. Rev. 68, 042319 (2003)
[64] Saadany B., Malak M., Kubota M., Marty F.M., Mita Y., Khalil D., Bourouina T.: Free-space tunable and drop optical filters using vertical Bragg mirrors on silicon. IEEE J. Sel. Topics Quantum Electron. 12(6), 1480–1488 (2006)
[65] Saleh B.E.A., Teich M.C.: Fundamentals of Photonics. John Wiley & Sons, Inc., New York, USA (1991)
[66] Siddique, U., Aravantinos, V., Tahar, S.: A new approach for the verification of optical systems. In: Optical System Alignment, Tolerancing, and Verification VII, volume 8844 of SPIE, pp. 88440G–88440G–14 (2013)
[67] Siddique, U., Aravantinos, V., Tahar, S.: Formal stability analysis of optical resonators. In: NASA Formal Methods, volume 7871 of LNCS, pp. 368–382 (2013) · Zbl 1396.68114
[68] Siddique, U., Aravantinos, V., Tahar, S.: On the formal analysis of geometrical optics in HOL. In: Automated Deduction in Geometry, volume 7993 of LNCS, pp. 161–180 (2013) · Zbl 1396.68114
[69] Siegman A.E.: Lasers. University Science Books, Sausalito, CA, USA (1986)
[70] Optica Software. http://www.opticasoftware.com/ (2014). Accessed 20 Mar 2014
[71] Song W.Z., Zhang X.M., Liu A.Q., Lim C.S., Yap P.H., Hosseini Habib M.M.: Refractive index measurement of single living cells using on-chip Fabry–Perot cavity. Appl. Phys. Lett. 89(20), 203901 (2006)
[72] Su B., Xue J., Sun L., Zhao H., Pei X.: Generalised ABCD matrix treatment for laser resonators and beam propagation. Opt. Laser Technol. 43(7), 1318–1320 (2011)
[73] Sylvester J.J.: The Collected Mathematical Papers of James Joseph Sylvester. vol. 4. Cambridge University Press, Cambridge, UK (1912) · JFM 43.0026.01
[74] Synopsys-CODE-V. http://optics.synopsys.com/codev/index.html (2014). Accessed 20 Mar 2014
[75] White A.G., Jennewein T., Barbieri M.: Single-photon device requirements for operating linear optics quantum computing outside the post-selection basis. J. Modern Opt. 58, 276–287 (2011) · Zbl 1220.81057
[76] Tan M.P., Kasten A.M., Sulkin J.D., Choquette K.D.: Planar photonic crystal vertical-cavity surface-emitting lasers. IEEE J. Sel. Topics Quantum Electron. 19(4), 4900107–4900107 (2013)
[77] Tan S.M.: A computational toolbox for quantum and atomic optics. J. Opt. B: Quantum Semiclass. Opt. 1, 424–432 (1999)
[78] Ünlü, M.S., Strite, S.: Resonant cavity enhanced photonic devices. J. Appl. Phys. 78(2), 607–639 (1995)
[79] Wiedijk F.: A synthesis of the procedural and declarative styles of interactive theorem proving. Log. Methods Comput. Sci. 8(1), 1–26 (2012) · Zbl 1238.68147
[80] Wilson, W.C., Atkinson, G.M.: MOEMS modeling using the geometrical matrix toolbox. Technical report, NASA, Langley Research Center (2005)
[81] Yin, L., Hong, W.: Domain decomposition method: a direct solution of Maxwell equations. In: Antennas and Propagation Society International Symposium, IEEE, vol.2, pp. 1290–1293 (1999)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.