Ardeshir-Larijani, Ebrahim (2014) Automated equivalence checking of quantum information systems. PhD thesis, University of Warwick.

Preview

PDF WRAP_THESIS_Ardeshir-Larijani_2014.pdf - Submitted Version - Requires a PDF viewer. Download (934Kb) | Preview

Request Changes to record.

Abstract

Quantum technologies have progressed beyond the laboratory setting and are beginning to make an impact on industrial development. The construction of practical, general purpose quantum computers has been challenging, to say the least. But quantum cryptographic and communication devices have been available in the commercial marketplace for a few years. Quantum networks have been built in various cities around the world, and plans are afoot to launch a dedicated satellite for quantum communication. Such new technologies demand rigorous analysis and verification before they can be trusted in safety and security-critical applications.

In this thesis we investigate the theory and practice of equivalence checking of quantum information systems. We present a tool, Quantum Equivalence Checker (QEC), which uses a concurrent language for describing quantum systems, and performs verification by checking equivalence between specification and implementation. For our process algebraic language CCSq, we define an operational semantics and a superoperator semantics. While in general, simulation of quantum systems using current computing technology is infeasible, we restrict ourselves to the stabilizer formalism, in which there are efficient simulation algorithms and representation of quantum states. By using the stabilizer representation of quantum states we introduce various algorithms for testing equality of stabilizer states.

In this thesis, we consider concurrent quantum protocols that behave functionally in the sense of computing a deterministic input-output relation for all interleavings of a concurrent system. Crucially, these input-output relations can be abstracted by superoperators, enabling us to take advantage of linearity. This allows us to analyse the behaviour of protocols with arbitrary input, by simulating their operation on a finite basis set consisting of stabilizer states. We present algorithms for the checking of functionality and equivalence of quantum protocols. Despite the limitations of the stabilizer formalism and also the range of protocols that can be analysed using equivalence checking, QEC is applied to specify and verify a variety of interesting and practical quantum protocols from quantum communication and quantum cryptography to quantum error correction and quantum fault tolerant computation, where for each protocol different sequential and concurrent model are defined in CCSq.

We also explain the implementation details of the QEC tool and report on the experimental results produced by using it on the verification of a number of case studies.

Item Type:	Thesis (PhD)
Subjects:	Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Library of Congress Subject Headings (LCSH):	Quantum systems, Quantum computers, Computer systems -- Verification
Official Date:	February 2014
Dates:	Date Event February 2014 Submitted
Institution:	University of Warwick
Theses Department:	Department of Computer Science
Thesis Type:	PhD
Publication Status:	Unpublished
Supervisor(s)/Advisor:	Nagarajan, Rajagopal ; Lazic, Ranko
Sponsors:	University of Warwick. Centre for Discrete Mathematics and its Applications ; University of Warwick. Department of Computer Science ; Engineering and Physical Sciences Research Council ; Eidgenössische Technische Hochschule Zürich
Extent:	xvii, 162 leaves : illustrations
Language:	eng

Request changes or add full text files to a record

Repository staff actions (login required)

View Item

Downloads