-
Quantum Heat Engines and the Generalized Uncertainty Principle
Authors:
Gardo Blado,
Jonathan Nguyen,
Giovani Renteria,
Skylar Gay,
Bryce Mortimer
Abstract:
We study the effects of the generalized uncertainty principle (GUP) on the efficiency of quantum heat engines based on a particle in an infinite square well using the partition function approach. In particular, we study the Carnot and Otto heat engines. For the system we used, the GUP-corrected efficiencies turned out to be lower than efficiencies without the GUP effects. However, as expected, GUP…
▽ More
We study the effects of the generalized uncertainty principle (GUP) on the efficiency of quantum heat engines based on a particle in an infinite square well using the partition function approach. In particular, we study the Carnot and Otto heat engines. For the system we used, the GUP-corrected efficiencies turned out to be lower than efficiencies without the GUP effects. However, as expected, GUP effects increase as the temperature of the cold heat bath decreases and as the width of the potential well decreases.
△ Less
Submitted 19 January, 2023;
originally announced January 2023.
-
Application of Quantum Process Calculus to Higher Dimensional Quantum Protocols
Authors:
Simon J. Gay,
Ittoop Vergheese Puthoor
Abstract:
We describe the use of quantum process calculus to describe and analyze quantum communication protocols, following the successful field of formal methods from classical computer science. We have extended the quantum process calculus to describe d-dimensional quantum systems, which has not been done before. We summarise the necessary theory in the generalisation of quantum gates and Bell states and…
▽ More
We describe the use of quantum process calculus to describe and analyze quantum communication protocols, following the successful field of formal methods from classical computer science. We have extended the quantum process calculus to describe d-dimensional quantum systems, which has not been done before. We summarise the necessary theory in the generalisation of quantum gates and Bell states and use the theory to apply the quantum process calculus CQP to quantum protocols, namely qudit teleportation and superdense coding.
△ Less
Submitted 31 July, 2014; v1 submitted 12 March, 2013;
originally announced March 2013.
-
Analysis of a Quantum Error Correcting Code using Quantum Process Calculus
Authors:
Timothy A. S. Davidson,
Simon J. Gay,
Rajagopal Nagarajan,
Ittoop Vergheese Puthoor
Abstract:
We describe the use of quantum process calculus to describe and analyze quantum communication protocols, following the successful field of formal methods from classical computer science. The key idea is to define two systems, one modelling a protocol and one expressing a specification, and prove that they are behaviourally equivalent. We summarize the necessary theory in the process calculus CQP,…
▽ More
We describe the use of quantum process calculus to describe and analyze quantum communication protocols, following the successful field of formal methods from classical computer science. The key idea is to define two systems, one modelling a protocol and one expressing a specification, and prove that they are behaviourally equivalent. We summarize the necessary theory in the process calculus CQP, including the crucial result that equivalence is a congruence, meaning that it is preserved by embedding in any context. We illustrate the approach by analyzing two versions of a quantum error correction system.
△ Less
Submitted 1 October, 2012;
originally announced October 2012.
-
Stabilizer States as a Basis for Density Matrices
Authors:
Simon J. Gay
Abstract:
We show that the space of density matrices for n-qubit states, considered as a (2^n)^2 dimensional real vector space, has a basis consisting of density matrices of stabilizer states. We describe an application of this result to automated verification of quantum protocols.
We show that the space of density matrices for n-qubit states, considered as a (2^n)^2 dimensional real vector space, has a basis consisting of density matrices of stabilizer states. We describe an application of this result to automated verification of quantum protocols.
△ Less
Submitted 9 December, 2011;
originally announced December 2011.
-
Formal Analysis of Quantum Systems using Process Calculus
Authors:
Timothy A. S. Davidson,
Simon J. Gay,
Rajagopal Nagarajan
Abstract:
Quantum communication and cryptographic protocols are well on the way to becoming an important practical technology. Although a large amount of successful research has been done on proving their correctness, most of this work does not make use of familiar techniques from formal methods, such as formal logics for specification, formal modelling languages, separation of levels of abstraction, and co…
▽ More
Quantum communication and cryptographic protocols are well on the way to becoming an important practical technology. Although a large amount of successful research has been done on proving their correctness, most of this work does not make use of familiar techniques from formal methods, such as formal logics for specification, formal modelling languages, separation of levels of abstraction, and compositional analysis. We argue that these techniques will be necessary for the analysis of large-scale systems that combine quantum and classical components, and summarize the results of initial investigation using behavioural equivalence in process calculus. This paper is a summary of Simon Gay's invited talk at ICE'11.
△ Less
Submitted 1 August, 2011;
originally announced August 2011.
-
QMC: A Model Checker for Quantum Systems
Authors:
Simon Gay,
Rajagopal Nagarajan,
Nikolaos Papanikolaou
Abstract:
We introduce a model-checking tool intended specially for the analysis of quantum information protocols. The tool incorporates an efficient representation of a certain class of quantum circuits, namely those expressible in the so-called stabiliser formalism. Models of protocols are described using a simple, imperative style simulation language which includes commands for the unitary operators in…
▽ More
We introduce a model-checking tool intended specially for the analysis of quantum information protocols. The tool incorporates an efficient representation of a certain class of quantum circuits, namely those expressible in the so-called stabiliser formalism. Models of protocols are described using a simple, imperative style simulation language which includes commands for the unitary operators in the Clifford group as well as classical integer and boolean variables. Formulas for verification are expressed using a subset of quantum computational tree logic (QCTL). The model-checking procedure treats quantum measurements as the source of non-determinism, leading to multiple protocol runs, one for each outcome. Verification is performed for each run.
△ Less
Submitted 21 April, 2008; v1 submitted 27 April, 2007;
originally announced April 2007.
-
Probabilistic Model--Checking of Quantum Protocols
Authors:
Simon Gay,
Rajagopal Nagarajan,
Nikolaos Papanikolaou
Abstract:
We establish fundamental and general techniques for formal verification of quantum protocols. Quantum protocols are novel communication schemes involving the use of quantum-mechanical phenomena for representation, storage and transmission of data. As opposed to quantum computers, quantum communication systems can and have been implemented using present-day technology; therefore, the ability to m…
▽ More
We establish fundamental and general techniques for formal verification of quantum protocols. Quantum protocols are novel communication schemes involving the use of quantum-mechanical phenomena for representation, storage and transmission of data. As opposed to quantum computers, quantum communication systems can and have been implemented using present-day technology; therefore, the ability to model and analyse such systems rigorously is of primary importance.
While current analyses of quantum protocols use a traditional mathematical approach and require considerable understanding of the underlying physics, we argue that automated verification techniques provide an elegant alternative. We demonstrate these techniques through the use of PRISM, a probabilistic model-checking tool. Our approach is conceptually simpler than existing proofs, and allows us to disambiguate protocol definitions and assess their properties. It also facilitates detailed analyses of actual implemented systems. We illustrate our techniques by modelling a selection of quantum protocols (namely superdense coding, quantum teleportation, and quantum error correction) and verifying their basic correctness properties. Our results provide a foundation for further work on modelling and analysing larger systems such as those used for quantum cryptography, in which basic protocols are used as components.
△ Less
Submitted 5 October, 2005; v1 submitted 1 April, 2005;
originally announced April 2005.
-
An Automated Analysis of the Security of Quantum Key Distribution
Authors:
Rajagopal Nagarajan,
Nikolaos Papanikolaou,
Garry Bowen,
Simon Gay
Abstract:
This paper discusses the use of computer-aided verification as a practical means for analysing quantum information systems; specifically, the BB84 protocol for quantum key distribution is examined using this method. This protocol has been shown to be unconditionally secure against all attacks in an information-theoretic setting, but the relevant security proof requires a thorough understanding o…
▽ More
This paper discusses the use of computer-aided verification as a practical means for analysing quantum information systems; specifically, the BB84 protocol for quantum key distribution is examined using this method. This protocol has been shown to be unconditionally secure against all attacks in an information-theoretic setting, but the relevant security proof requires a thorough understanding of the formalism of quantum mechanics and is not easily adaptable to practical scenarios. Our approach is based on probabilistic model-checking; we have used the PRISM model-checker to show that, as the number of qubits transmitted in BB84 is increased, the equivocation of the eavesdropper with respect to the channel decreases exponentially. We have also shown that the probability of detecting the presence of an eavesdropper increases exponentially with the number of qubits. The results presented here are a testament to the effectiveness of the model-checking approach for systems where analytical solutions may not be possible or plausible.
△ Less
Submitted 9 February, 2005;
originally announced February 2005.
-
Communicating Quantum Processes
Authors:
Simon Gay,
Rajagopal Nagarajan
Abstract:
We define a language CQP (Communicating Quantum Processes) for modelling systems which combine quantum and classical communication and computation. CQP combines the communication primitives of the pi-calculus with primitives for measurement and transformation of quantum state; in particular, quantum bits (qubits) can be transmitted from process to process along communication channels. CQP has a…
▽ More
We define a language CQP (Communicating Quantum Processes) for modelling systems which combine quantum and classical communication and computation. CQP combines the communication primitives of the pi-calculus with primitives for measurement and transformation of quantum state; in particular, quantum bits (qubits) can be transmitted from process to process along communication channels. CQP has a static type system which classifies channels, distinguishes between quantum and classical data, and controls the use of quantum state. We formally define the syntax, operational semantics and type system of CQP, prove that the semantics preserves typing, and prove that typing guarantees that each qubit is owned by a unique process within a system. We illustrate CQP by defining models of several quantum communication systems, and outline our plans for using CQP as the foundation for formal analysis and verification of combined quantum and classical systems.
△ Less
Submitted 9 September, 2004;
originally announced September 2004.
-
Formal Verification of Quantum Protocols
Authors:
Rajagopal Nagarajan,
Simon Gay
Abstract:
We propose to analyse quantum protocols by applying formal verification techniques developed in classical computing for the analysis of communicating concurrent systems. One area of successful application of these techniques is that of classical security protocols, exemplified by Lowe's discovery and fix of a flaw in the well-known Needham-Schroeder authentication protocol. Secure quantum crypto…
▽ More
We propose to analyse quantum protocols by applying formal verification techniques developed in classical computing for the analysis of communicating concurrent systems. One area of successful application of these techniques is that of classical security protocols, exemplified by Lowe's discovery and fix of a flaw in the well-known Needham-Schroeder authentication protocol. Secure quantum cryptographic protocols are also notoriously difficult to design. Quantum cryptography is therefore an interesting target for formal verification, and provides our first example; we expect the approach to be transferable to more general quantum information processing scenarios. The example we use is the quantum key distribution protocol proposed by Bennett and Brassard, commonly referred to as BB84. We present a model of the protocol in the process calculus CCS and the results of some initial analyses using the Concurrency Workbench of the New Century (CWB-NC).
△ Less
Submitted 18 March, 2002;
originally announced March 2002.
