# Reasoning about Quantum Information: An Overview of Quantum Dynamic Logic
## 2 The Logic of Quantum Actions
### Semantics of \(Lqa\)
If \(W=\bigcup P\) is the corresponding subspace of \(\mathcal{H}\), then the quantum test is the map induced on states by the projector \(Proj_{W}\) onto the subspace \(W\), which is given by:  
\[P\overline{x}:=\overline{Proj_{W}(x)}\in\Sigma,\text{ if }\overline{x}\
ot\in P ^{\perp}(\text{i.e., if }Proj_{W}(x)\
eq 0)\]\[P?(\overline{x}):=\text{undefined},\text{ otherwise}.\]  
We use the notation \(\stackrel{{ P? }}{{\rightarrow}}\subseteq\Sigma\times\Sigma\) to denote the binary relation corresponding to the partial map \(P?\) that is given by:  
\[s\stackrel{{ P?}}{{\rightarrow}}t\text{ if and only if }P?(s)=t\]  
In our semantics, we work with a family of such binary relations \(\{\stackrel{{ P? }}{{\rightarrow}}\}_{P\in\mathcal{L}}\) indexed by the testable properties \(P\in\mathcal{L}\) expressing the state transitions that a successful test of a physical property induces. More specifically, the action of a quantum test \(s\stackrel{{ P? }}{{\rightarrow}}t\) represents the _successful test_ of a testable property \(P\) on an input state \(s\). A \"successful test\" indicates that if the state is such that \(P\) happens to be successfully tested, then the answer of the binary measurement of \(P\) will be \"yes\", and as a result, the output state \(t\) of the system will satisfy property \(P\). **Unitary Evolutions. ** A _unitary transformation_ (or 'quantum evolution') is a linear map \(U\) on \(\mathcal{H}\) such that \(U\circ U^{\ddagger}=U^{\ddagger}\circ U=id\) (where \(id\) is the identity on \(\mathcal{H}\) and \(U^{\ddagger}\) is the adjoint of \(U\)). Unitary evolutions preserve inner products. For every such unitary transformation \(U\) on \(\mathcal{H}\), we consider the corresponding binary relation on the state space \(U\subseteq\Sigma\times\Sigma\) given by  
\[s\stackrel{{ UI}}{{\rightarrow}}t\text{ if and only if }U(x)=y\text{ for some non-zero vectors }x\in s\text{ and }y\in t\]  
In our semantics, we work with a family of such binary relations \(\{\stackrel{{ U}}{{\rightarrow}}\}_{U\in\mathcal{U}}\) indexed by the unitary quantum logical gates \(U\) to express the state transitions that are due to unitary evolutions that let the system evolve in a specific way. The binary relations labeled by the successful tests of testable properties or by unitary evolutions are all state transition relations, expressing how the action of performing a test or letting the system evolve via a logical gate changes the state of a physical system. **Semantic Interpretation of \(\boldsymbol{LQA}\). ** As standard in logic, we define a quantum-dynamic _model_ as a pair \((\boldsymbol{\Sigma},\|\bullet\|)\), consisting of a quantum frame (transition system) \(\boldsymbol{\Sigma}\), together with a valuation \(\|\bullet\|:\Omega\rightarrow\mathcal{P}(\Sigma)\), assigning to every atomic sentence \(p\in\Omega\) some proposition \(\|p\|\subseteq\Sigma\). As standard, we can recursively extend the valuation to an _interpretation_ function, that maps each well-formed sentence \(\varphi\) to a proposition \(\|\varphi\|\subseteq\Sigma\), and it also maps each program \(\pi\) to a binary relation \(\stackrel{{\pi}}{{\rightarrow}}\subseteq\Sigma\times\Sigma\) on states. The definition of the interpretation map is provided by induction in terms of its compositional clauses for well-formed sentences:  
\[s\in\|\
eg\varphi\|\text{ iff }s\
ot\in\|\varphi\|\]  
\[s\in\|\varphi\wedge\psi\|\text{ iff }s\in\|\varphi\|\text{ and }s\in\|\psi\|\]  
\[s\in[\pi]\varphi\text{ iff }t\in\|\varphi\|\text{ whenever }s\stackrel{{\pi}}{{ \rightarrow}}t\]  
As usual, we will sometimes use the _satisfaction relation_\(s\models\varphi\) as an alternative notation for \(s\in\|\varphi\|\).