# Reasoning about Quantum Information: An Overview of Quantum Dynamic Logic
## 2 The Logic of Quantum Actions
### Semantics of \(Lqa\)
5  
Footnote 5: The _quantum_  
To capture this probabilistic ingredient, we now extend our language with a probabilistic operator \(P^{\geq r}\) to obtain the full logic \(QDL\) as follows:  
\[ \begin{array}{cccc|c|c|c}\varphi&::=&p&\mid\
eg\varphi&\mid\varphi\wedge\varphi& \mid[\pi]\varphi&\mid K_{1}\varphi\mid P^{\geq r}\varphi\\ \pi&::=&U&\mid\varphi\text{?}&\mid\pi\cup\pi&\mid\pi;\pi\end{array} \]  
The expression \(P^{\geq r}\varphi\) is here used to express the fact that testing property \(\varphi\) (on the current state of the system) will succeed with probability \(\geq r\) if we perform a binary measurement of \(\varphi\) on the system. Here, \(r\) is a rational number in the interval \([0,1]\). Having this probabilistic modality \(P^{\geq r}\) in our language does turn this logic into a probabilistic logic as explained in [7], which enhances the expressive power of the logic and makes it fit for the verification of probabilistic quantum algorithms. Note that using both the quantum and classical negation in our language, one can express different strict versions of the probabilistic modality as done in [7]:  
\[P^{\leq r}\varphi :=P^{\geq(1-r)}\sim\varphi\] \[P^{<r}\varphi :=\
eg P^{\geq r}\varphi\] \[P^{>r}\varphi :=\
eg P^{\leq r}\varphi\]  
We can further plug in the probabilistic formula inside the dynamic modality as follows  
\[[\varphi^{\geq r}]\psi :=P^{\leq r}\varphi\Rightarrow[\varphi\text{?}]\psi\]  
This construct has been used in [7] to express that \"if the test of \(\varphi\) will succeed with probability \(\geq r\), then \(\psi\) will be the case after any successful execution of the test\". **Semantics of the Probabilistic Operator. ** To calculate the probabilistic expectation values of a measurement of \(\varphi\) in quantum mechanics, we adopt the Born rule. The Born rule states that the probability that a test of property \(\varphi\) (or a projective measurement of \(\varphi\)) is successful for a system in state \(s\) represented by any of the vectors \(x\in s\) is given by  
\[<x|Proj_{\varphi}(x)>=|Proj_{\varphi}(x)|^{2},\]  
where we denoted by \(Proj_{\varphi}\) the projector onto the closed linear subspace \(\overline{\bigcup\|\varphi\|}=\bigcup\|\varphi\|^{\perp\perp}\) generated by \(\|\varphi\|\), while \(<x|y>\) is as usual the inner product of vectors \(x\) and \(y\), and \(|x|=\sqrt{<x|x>}\) is the norm of vector \(x\). The interpretation that we give to our probabilistic modality will make use of the here-stated Born rule. In standard dirac notation, we express that the expectation value is equal or bigger than \(r\) for the test of property \(\varphi\) to be successful for a system in state \(s\):  
\[s\in\|P^{\geq r}\varphi\|\text{ iff }\left|Proj_{\varphi}(x)\right|^{2}\geq r \text{ for all unit vectors }x\in s\]  
**Decidability of \(QDL\). ** The full quantum dynamic logic \(QDL\) includes the three fragments of the logic that we have explained, starting with the logic of quantum tests and adding the epistemic features and the probabilistic features. The obtained logical system \(QDL\) has been shown to be a decidable logic [7]. It is important to note that this result shows that quantum logic has a great computational advantage over its classical first-order (and higher-order) variants, which are known to be undecidable. Decidability is an important feature for a logical system to have, as it opens up the road for implementations in the area of quantum computing. We have proven the important decidability result via a translation into the first-order logic of real numbers in [7]. We refer to this paper for more details about the general proof method we constructed to show the decidability result, which extends upon an idea employed in the decidability proof in [33]. In the next section, we illustrate how the full logic \(QDL\) can now be used to specify and verify a range of specific quantum protocols.