Anzeige
Erschienen in:
2015 | OriginalPaper | Buchkapitel
On the Formal Verification of Optical Quantum Gates in HOL
verfasst von : Mohamed Yousri Mahmoud, Prakash Panangaden, Sofiène Tahar
Erschienen in: Formal Methods for Industrial Critical Systems
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Quantum computers are expected to handle hard computational problems and provide unbreakable security protocols. Among different quantum computer implementations, those based on quantum optics and nuclear magnetic resonance show good advancement in building large scale machines. However, the involvement of optical and nuclear techniques makes their development very critical. This motivates us to apply formal techniques, in particular theorem proving, in quantum circuits analysis. In this work, we present the formalization of multi-inputs/multi-outputs quantum gates (technically called multi-modes optical circuits). This requires the implementation of tensor product over complex-valued functions. Firstly, we build a formal model of single optical beams and then extend it to cover circuits of multi optical beams, with the help of the developed tensor product algebra. As an application, we formally verify the behavior of the optical quantum CNOT gate and Mach-Zehnder interferometer.