## 5 Model Checking LTL and \(\omega\)-Regular Properties
### Computing PQMC Values  
As we have seen in Section 5.3, it is not enough to compute the BSCCs by looking only at the classical states of the product PQMC. The solution adopted by [49] is to encode the behavior of \(\mathfrak{M}\) into a single super-operator acting on the _extended_ Hilbert space \(\mathcal{H}_{c}\otimes\mathcal{H}\) representing both the classical states and the super-operators decorating the transitions. This is obtained by taking the tensor product of the classical state space and the quantum one; then the notion of BSCC _subspaces_ for super-operators, as defined in [73], is used in the computation of the PQMC values. The intuition underlying this extended construction is to keep track of the classical states reached step by step in the \(\mathcal{H}_{c}\) part of \(\mathcal{H}_{c}\otimes\mathcal{H}\), and  
Figure 3: Parity construction for the QMC from Figure 1 and the LTL formula \((\
eg\ell_{2})\ \mathbf{U}\ \ell_{3}\). to accumulate the effects of the super-operators decorating the taken transitions on the \(\mathcal{H}\) part of \(\mathcal{H}_{c}\otimes\mathcal{H}\). This allows us to overcome the problem of the BSCC decomposition of the underlying graph of the given PQMC: as we have seen in Section 5.3, by performing a transition we might change the underlying graph, since some transition might be disabled as effect of the composition of super-operators; this does not happen in the classical and probabilistic setting, where the underlying graph is immutable. Let \(\mathcal{E}\) be a super-operator acting on \(\mathcal{H}\); given a subspace \(X\) of \(\mathcal{H}\), we call \(X\):  
* _invariant_ for \(\mathcal{E}\) if \(\mathcal{E}(X)\subseteq X\);
* a _BSCC_ of \(\mathcal{E}\) if \(\mathcal{R}(\left|\psi\right\rangle\left\langle\psi\right|)=X\) holds for each pure state \(\left|\psi\right\rangle\in X\), where \(\mathcal{R}(\rho)=\bigvee_{i=0}^{\infty}\operatorname{supp}(\mathcal{E}^{i}( \rho))\) is the _reachable subspace_ of \(\mathcal{E}\) starting in \(\rho\in\mathcal{D}(\mathcal{H})\);
* _transient_ if \(\lim_{k\to\infty}\operatorname{tr}(P_{X}\mathcal{E}^{k}(\rho))=0\) for each \(\rho\in\mathcal{D}(\mathcal{H})\), where \(P_{X}\) is the projection onto \(X\). Intuitively, we have that the probability of remaining forever in a transient subspace \(X\) tends to \(0\), as happens for the transient states in a classical Markov chain. Similarly, it is not possible to leave a BSCC \(X\), and eventually all elements of \(X\) are visited again and again, as happens for states in the BSCCs of a classical Markov chain. We are now ready to present how to combine together the classical part and the quantum part of a PQMC. Let \(\mathfrak{M}=(S,\mathbf{Q},\mathsf{pri})\) be a PQMC on \(\mathcal{H}\); for each \(s,t\in S\), let \(\mathcal{E}^{s,t}=\{\,E_{j}^{s,t}\mid j\in J^{s,t}\,\}\) be the set of Kraus operators with \(J^{s,t}\) as set of indexes for the super-operator \(\mathcal{E}^{s,t}=\mathbf{Q}(s,t)\). Following [72], let \(\mathcal{E}_{\mathfrak{M}}=\{\,|t\rangle\,\langle s|\otimes E_{j}^{s,t}\mid\,s,t\in S,j\in J^{s,t}\,\}\) be the super-operator acting on the extended Hilbert space \(\mathcal{H}_{c}\otimes\mathcal{H}\), where \(\mathcal{H}_{c}\) is the \(|S|\)-dimensional Hilbert space with orthonormal basis \(\{\,|s\rangle\mid s\in S\,\}\). For each \(s\in S\), let \(O^{s}=\{\,(t,j)\mid t\in S,j\in J^{s,t}\,\}\) and \(M^{s}=\{\,E_{j}^{s,t}\mid\,(t,j)\in O^{s}\,\}\). To see how \(\mathcal{E}_{\mathfrak{M}}\) encodes the behavior of \(\mathfrak{M}\), consider the following steps, which exactly capture the intended meaning of \(\mathfrak{M}\). 1. A projective measurement \(M=\{\,|s\rangle\,\langle s|\mid s\in S\,\}\) is performed on the classical system \(\mathcal{H}_{c}\) to determine the current classical state. 2. If the measurement outcome of \(M\) is \(s\), then the quantum measurement \(M^{s}\) is performed on the quantum system \(\mathcal{H}\). 3. If the observed outcome of \(M^{s}\) is \((t,i)\), then the classical state is set to be \(\left|t\right\rangle\left\langle t\right|\).