Quantum Equivalence Checker is a tool for verification of quantum communicating systems, using equivalence checking. While classical simulation and analysis of quantum systems are infeasible in genreral, we have been able to automatically verify the correctness of some important quantum protocols, from quantum communication, quantum fault tolerant computation to quantum cryptography. Here we present some details of protocols those we have been able to verify by equivalence checker .
In this protocol Alice sends two classical bits only by sending one qubit and sharing an entangled pair. There are three processes of Alice,Bob and entanglement. We have modelled this protocol by encoding classical bits into two qubits. Then we only applied equivalence checking on the standard basis.(we have altered the released version source code i.e we have only four basis states to check: (00,01,10,11).
Quantum systems in general are continuous . Discrete analysis of quantum systems, as we do in verification of them, has a longer history in QIP. A beautiful example is Stabilizer Codes. Several stabilizer codes have been developed. Here we explain the most compact codes like five qubit code, which is been implemented in the laboratory (like Five qubit code in the following). This code can protect a single qubit against a continuum of errors only by analysing a discrete subset of them. Namely, bit flip and phase flip errors. An interesting point here is that both of bit flip and phase flip protocol lie in the stabilizer formalism and therefore can be analysed in our equivalence checking system. In the following first we give implementation of phase flip error correction protocol, then we implement five qubit general error correction protocol. The specification of these protocols are similar to the Teleportation example and can be found in the file "Identity.ccs".
In these protocols Alice wants to send qubits to Bob in the presence of noises. The effect of noisy environment in bit flip codes is modelled applying X operations (flipping) on the qubits. The protocol consists of three phases: encoding, correction and recovery. The specification program is similar to teleportation, that is we want to send a qubit q and completely recover it at the end of protocol. Quantum Bit flip code is analogous to classical bit flip protocol. a more interesting example of stabilizer codes is Phase flip code which has no classical equivalent. The overall structure of this protocol is similar to the bit flip code except that errors effect is flipping the phase (Applying Pauli Z)of quantum states. To make phase flip visible, we need to change the basis of syndrome measurements from Z basis to X basis, by applying Hadamard gate. The implementation of these protocols are in the "ErrB.ccs" and "ErrZ.ccs".
The idea of combining phase flip and bit flip codes into one code first appeared in Shor's nine qubits protocol. Then it was optimized to Steane seven qubit protocol. Finally, Laflamme et.al. showed that there is a five qubit protocol which does the same job as Shor's and Steane's codes. The interesting fact about these codes is they can protect a single qubit not only from bit flip and phase flip, but also from arbitrary errors. To build a model for analysis of this protocol first we encode the qubit which we want to protect against noises with four other qubits according to the LMPZ protocol. Then we consider 16 different noises applied on a single qubit of the system, that is including no error, five Pauli X (bit flip), five Pauli Z (phase flip) and five combined bit and phase flip (XZ) error.
In fault tolerant quantum information processing often computation is carried out in blocks in which joint quantum operations are only allowed inside of a block and not between blocks. For example in the Teleportation protocol we only apply quantum operations inside Alice, EPR or Bob process. However if we were allowed to apply a CNOT operation on two qubits one from Alice and one from Bob we would end up in a simpler model for Teleportation. These are called X-teleporation and Z-Teleportation and the model is described in the examples directory. An application of this kind of Teleportation is in the implementation of remote (fault tolerant) CNOT operation. For this protocol we run a X-Teleportation and a Z-Teleportation concurrently and also with a shared entangled pair of qubit. The intended specification is to apply CNOT on a given input. Specification of this protocol is in file "Cnot.ccs" and implementation of remote CNOT can be found in the examples directory. An alternative approach for implementing remote CNOT is introduced by Gottesmann. However this method is less systematic and fault tolerant than the previously mentioned method. Nevertheless, it produces smaller number of interleavings and has been implemented in file "aremoteCnot.ccs".
This protocol is to teleport a quantum state from Alice to Bob without physically transferring qubits, using quantum entanglement. Before starting the communication between the two parties, Alice and Bob, an entangled pair is established and shared between them. Alice then entangles the input qubit with her half of the entangled qubit by applying a controlled-not gate followed by a Hadamard gate. She then measures her qubits and sends the classical outcome to the Bob. Depending on the four classical outcomes of Alice measurements, Bob applies certain X and Z operations and recovers the input state on his entangled qubit. In our concurrent language, we provide a programming interface thus we can describe the implementation of teleportation reflecting physical separation Alice and Bob . This is not possible using quantum circuit formalism. The implementation can be found in the examples directory.
This protocol was first introduced by Hillery et. al. The original problem of secret sharing involves an agent Alice sending a message to two agents Bob and Charlie, one of whom is dishonest. Alice doesn't know whic one of the agents is dishonest, so she must encode the message so that Bob and Charlie must collaborate to retrieve it. For the quantum version of this protocol the three agents need to share a maximally entangled three-qubit state, called the GHZ state, prior to the execution of the protocol: (|000> + |111>)/sqrt(2). In our implementation model we assume that Charlie will end up with the original qubit (a variation of the protocol will allow Bob to end up with it). First, Alice entangles the input qubit with her entangled qubit from the GHZ state. Then Alice measures her qubits and sends the outcome to Charlie. Bob also measures his qubit and sends the outcome to Charlie. Finally, Charlie is able to retrieve the original qubit once he has access to the bits from Alice and Bob. The security of this protocol stems from no-cloning theorem in quantum mechanics. The model for this protocol is included in the examples directory.