## 5 Model Checking LTL and \(\omega\)-Regular Properties
### Computing PQMC Values
The super-operator \(\mathcal{E}_{\mathfrak{M}}\) enjoys a couple of nice properties: starting from a product initial state, the classical and quantum systems remain separable (disentangled) along the whole execution (cf. [49] (Lemma 11)); moreover, each fixed point state \(\sigma\) of \(\mathcal{E}_{\mathfrak{M}}\), i.e., \(\mathcal{E}_{\mathfrak{M}}(\sigma)=\sigma\), has the form \(\sigma=\sum_{s\in S}\left|s\right\rangle\left\langle s\right|\otimes\sigma_{s}\). According to [73], we find that any BSCC of \(\mathcal{E}_{\mathfrak{M}}\) can be spanned by pure states of the form \(\left|s\right\rangle\left|\eta\right\rangle\) where \(s\in S\) and \(\left|\eta\right\rangle\in\mathcal{H}\). We are now ready to collect all BSCCs of \(\mathcal{E}_{\mathfrak{M}}\) and classify them according to their acceptance condition. Given a BSCC \(B\) of \(\mathcal{E}_{\mathfrak{M}}\), let  
\[C(B)=\{\,s\in S\mid\left|s\right\rangle\left|\eta\right\rangle\in B\text{ for some }\left|\eta\right\rangle\in\mathcal{H}\,\}\]  
be the set of classical states supported in \(B\). Note that it is possible to have \(C(B)\cap C(B^{\prime})\
eq\emptyset\) for two different BSCCs \(B\) and \(B^{\prime}\); this happens when there are two states \(\left|s\right\rangle\left|\eta\right\rangle\in B\) and \(\left|s^{\prime}\right\rangle\left|\eta^{\prime}\right\rangle\in B^{\prime}\) with \(s=s^{\prime}\). However, this is not a real problem: as shown by [49] (Lemma 12), two BSCCs are orthogonal as long as they differ on at least one classical state. Given the set of all BSCCs of \(\mathcal{E}_{\mathfrak{M}}\), we can organize it with respect to the minimal priority assigned to the classical states in each BSCC. For a priority \(k\in\mathbb{N}\), let \(\mathcal{BSCC}_{=k}\) be the span of all BSCCs of \(\mathcal{E}_{\mathfrak{M}}\) whose minimal priority is \(k\), that is,  
\[\mathcal{BSCC}_{=k}=\bigvee\{\,B\text{ is a BSCC of }\mathcal{E}_{\mathfrak{M}}\mid \min\{\,\mathsf{pri}(s)\mid s\in C(B)\,\}=k\,\}.\]  
Similarly, let \(\mathcal{BSCC}_{<k}\) and \(\mathcal{BSCC}_{>k}\) be the spans of all BSCCs with the minimal priority being less than and larger than \(k\), respectively. Since \(\mathcal{BSCC}_{=k}\), \(\mathcal{BSCC}_{<k}\), and \(\mathcal{BSCC}_{>k}\) have different sets of classical states, they are pairwise orthogonal by [49] (Lemma 12). This implies, by [73], that \(\mathcal{H}_{c}\otimes\mathcal{H}\) can be decomposed _uniquely_ into  
\[\mathcal{H}_{c}\otimes\mathcal{H}=T\oplus\mathcal{BSCC}_{-k}\oplus\mathcal{BSCC }_{<k}\oplus\mathcal{BSCC}_{>k},\]  
where \(T\) is the maximum transient subspace of \(\mathcal{E}_{\mathfrak{M}}\). An important result (cf. [49] (Lemma 13)) is that the BSCCs in \(\mathcal{BSCC}_{=k}\), \(\mathcal{BSCC}_{<k}\), and \(\mathcal{BSCC}_{>k}\) do not interfere with each other: let \(\operatorname{tr}(R_{t}^{k}(\rho))\) denote the probability that \(k\) is the lowest priority occurring infinitely often from the initial state \(\ket{t}\bra{t}\otimes\rho\). Then, we have that:  
* if \(\operatorname{supp}(\ket{t}\bra{t}\otimes\rho)\subseteq\mathcal{BSCC}_{-k}\), then \(\operatorname{tr}(R_{t}^{k}(\rho))=\operatorname{tr}(\rho)\);
* if \(\operatorname{supp}(\ket{t}\bra{t}\otimes\rho)\subseteq\mathcal{BSCC}_{<k}\), then \(\operatorname{tr}(R_{t}^{k}(\rho))=0\); and
* if \(\operatorname{supp}(\ket{t}\bra{t}\otimes\rho)\subseteq\mathcal{BSCC}_{>k}\), then \(\operatorname{tr}(R_{t}^{k}(\rho))=0\),  
that is, once we enter \(\mathcal{BSCC}_{=k}\) with probability \(\operatorname{tr}(\rho)\), we will see \(k\) as the minimum priority almost surely; instead, if we enter \(\mathcal{BSCC}_{<k}\) or \(\mathcal{BSCC}_{>k}\), we will see \(k\) as minimum priority with probability \(0\). In practice, \(\mathcal{BSCC}_{=k}\) acts like the standard BSCC with minimum priority \(k\) in classical Markov chains. It now remains to collect all \(\mathcal{BSCC}_{=k}\) with even priority \(k\) to obtain the accepting BSCCs, and combine together their super-operators. This is formalized as follows. **Theorem 1** ([49] (Corollary 15)).