# Reasoning about Quantum Information: An Overview of Quantum Dynamic Logic
## 4 Application to Quantum Communication Protocols  
As an example to illustrate the usefulness of our formalism, we look at two basic examples of such protocols, Quantum Teleportation and Quantum Secret Sharing. For our analysis of these protocols we follow the work in [3]; after that, it will be easy to see how our formal tools can be used to analyze a wide range of other protocols for quantum communication. **Quantum Teleportation. ** To start with the standard teleportation scenario, we are working in a 3-qubit space \(\Sigma_{1}\otimes\Sigma_{2}\otimes\Sigma_{3}\) and consider a system consisting of three components hence \(N=\{1,2,3\}\). In addition, we assume that there are two classical agents, [PERSON] and [PERSON]. [PERSON] and [PERSON] are assumed to be separated in space, and each holds one qubit of an \"entangled EPR pair\", i.e., a pair of qubits \(2,3\) prepared in the Bell state \(\frac{|00\rangle+|11\rangle}{\sqrt{2}}\) denoted in our formalism as \(\beta_{00}^{2,3}\). [PERSON] also holds, in addition to her part of the EPR pair, a qubit 1, in an unknown 1-local state. [PERSON] now wants to \"teleport\" this unknown state of her qubit 1 to [PERSON]; i.e., she will perform a program that will output a state satisfying \(id_{13}\), the identity map. In order to do this, [PERSON] first entangles qubit 1 with her part (qubit 2) of the EPR pair. She does this by performing a series of \(I\)-local actions: she applies a \(CNOT_{1,2}\) logical gate on the two qubits followed by a Hadamard transformation \(H_{1}\) on the first component. Next, [PERSON] measures her qubits in the standard basis, thus destroying the entanglement of the EPR pair that she shared with [PERSON]. As a result, [PERSON]'s qubit 3 will collapse to a state \(q_{3}\). Moreover, the result that [PERSON] obtains from the two measurements indicate the actions that [PERSON] has to perform in order to transfer his qubit from its state \(q_{3}\) into the same state as [PERSON]'s original qubit, i.e., the state \(id_{13}(q_{1})\) (which corresponds to the qubit [PERSON] had before the protocol). Note that it is enough for [PERSON] to communicate to [PERSON] the result of her measurement, i.e., send him two classical bits \((x,y)\in\{0,1\}\times\{0,1\}\), encoding the result \(x_{1}\) of the first measurement and the result \(y_{2}\) of the second measurement. This tells [PERSON] that he will have to apply \(y\) times the \(X\)-gate followed by \(x\) times the \(Z\) gate if he wants to force his qubit \(q_{3}\) into the state \(id_{13}(q_{1})\). The above description of the \"abstract teleportation protocol\", as one finds it in most textbooks, can be encoded into our dynamic quantum logic \(QDL\). To do so, we have to capture the passing of the first two qubits through some quantum gates, measuring them in the standard basis, then perform some correction on the third qubit, i.e., another quantum gate which depends on the result of the previous measurement outcome. Encoded as the quantum program, we obtain:  
\[\pi=\bigcup_{x,y\in\{0,1\}}\mathsf{CNOT}_{12};H_{1};(x_{1}\wedge y_{2})?;X_{3 }^{y};Z_{3}^{x}\]  
The correctness of the teleportation-protocol specified in our logic can be stated via the following logical formula:  
\[\vdash(q_{1}\wedge\beta_{00}^{2,3})\Rightarrow[\pi]q_{3}\]  
This formula expresses the fact that after the protocol, the local state of qubit 3 is the same as the initial local state of qubit 1. Given the appropriate dynamic quantum logic, one can easily proof the correctness of this protocol, and indeed, such a proof has been provided in [3]. **Quantum Secret Sharing. ** In [3], we provided the correctness of the protocol of quantum secret sharing. This protocol refers to a scenario in which we split quantum information into a number \(m\) of'shares' to be distributed among \(m\) agents in such a way that the original information, i.e., the'secret', can only be recovered when one pools together the information in all the \(m\) shares. Consider the scenario where we work with three shares.