Login | Register

Formal Analysis of Quantum Optics


Formal Analysis of Quantum Optics

Mahmoud, Mohamed Yousri (2015) Formal Analysis of Quantum Optics. PhD thesis, Concordia University.

[thumbnail of MAHMOUD_PhD_F2015.pdf]
Text (application/pdf)
MAHMOUD_PhD_F2015.pdf - Accepted Version


At the beginning of the last century, the theory of quantum optics arose and led to a revolution in physics, since it allowed the interpretation of many unknown phenomena and the development of numerous powerful, cutting edge engineering applications,
such as high precision laser technology. The analysis and verification of such applications and systems, however, are very complicated. Moreover, traditional analysis tools, e.g., simulation, numerical methods, computer algebra systems, and paper-and-pencil approaches are not well suited for quantum systems. In the last decade, a new emerging verification technique, called formal methods, became common among engineering domains, and has proven to be effective as an analysis tool. Formal methods
consist in the development of mathematical models of the system subject for analysis, and deriving computer-aided mathematical proofs. In this thesis, we propose a framework for the analysis of quantum optics based on formal methods, in particular theorem proving. The framework aims at implementing necessary quantum mechanics and optics concepts and theorems that facilitate the modelling of quantum optical devices and circuits, and then reason about them formally. To this end, the framework
consists of three major libraries: 1) Mathematical foundations, which mainly contain the theory of complex-valued-function linear spaces, 2) Quantum mechanics, which develops the general rules of quantum physics, and 3) Quantum Optics, which
specializes these rules for light beams and implements all related concepts, e.g., light coherence which is typically emitted by laser sources. On top of these theoretical foundations, we build a library of formal models of a number of optical devices commonly
used in quantum circuits, including, beam splitters, light displacers, and light phase shifters. Using the proposed framework, we have been able to formally verify common quantum optical computing circuits, namely the Flip gate, CNOT gate, and Mach-Zehnder interferometer.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (PhD)
Authors:Mahmoud, Mohamed Yousri
Institution:Concordia University
Degree Name:Ph. D.
Program:Electrical and Computer Engineering
Date:September 2015
Thesis Supervisor(s):Tahar, Sofiene
Keywords:Formal Methods Theorem Proving Quanrum Optics Quantum Computing
ID Code:980594
Deposited On:28 Oct 2015 12:16
Last Modified:18 Jan 2018 17:51
Related URLs:
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top