## 5 Model Checking LTL and \(\omega\)-Regular Properties
### Computing PQMC Values
: _Let \(\mathfrak{M}=(S,\mathbf{Q},\mathsf{pri})\) be a PQMC. Then, for any \(s\in S\),_  
\[\operatorname{val}_{s}^{\mathfrak{M}}\eqsim\operatorname{tr}_{c}\circ\mathcal{ P}_{\text{even}}\circ\mathcal{E}_{\mathfrak{M}}^{\infty}\circ\mathcal{E}_{s}\]  
_where \(\operatorname{tr}_{c}\) is the partial trace super-operator, such that \(\operatorname{tr}_{c}(\ket{s}\bra{t}\otimes\rho)=\bra{t}s\cdot\rho\), \(\mathcal{P}_{\text{even}}=\sum_{\{k\in\mathsf{pri}(S)|k\text{ even}\}}\mathcal{P}_{=k}\) where \(\mathcal{P}_{=k}=\{P_{=k}\}\) is the projection super-operator onto \(\mathcal{BSCC}_{=k}\), \(\mathcal{E}_{\mathfrak{M}}^{\infty}=\lim_{N\to\infty}\frac{1}{N}\sum_{n=1}^{N }\mathcal{E}_{\mathfrak{M}}^{n}\), and \(\mathcal{E}_{s}(\rho)=\ket{s}\bra{s}\otimes\rho\)._  
Similarly to the QCTL case (cf. Section 3), the value \(\operatorname{val}_{s}^{\mathfrak{M}}\) is not computed exactly, but only a _trace equivalent_ super-operator is obtained. This is in line with the statement of [44] (Theorem 3.2), saying that the super-operator valued measure for a QMC (hence, for a PQMC) is well-defined only up to the trace equivalence \(\eqsim\), already at the level of the measure for the measurable space \((\mathsf{Path}^{\mathfrak{M}},\Sigma)\). This means that we are not able to compute the _exact_ super-operator corresponding to a measurable set of paths, but only a super-operator in the same \(\eqsim\)-equivalence class. This suffices for our purposes, since LTL and \(\omega\)-regular model checking for LQMCs (as well as the QCTL model checking) only look for the _probability_ of satisfying the given property, which is preserved by \(\eqsim\). As an application of the above construction, consider the right part of Figure 3, where we show the product of the QMC shown in Figure 1 and the PA \(\mathfrak{M}\) encoding the formula \((\
eg\ell_{2})\)\(\mathbf{U}\,\ell_{3}\). It is easy to observe that, for this specific case, we have only one accepting BSCC, composed only by the state \((\ell_{3}\top)\), and that the super-operator corresponding to the paths leading to it is \(\mathcal{E}_{0}\mathcal{A}\), the same as we computed in Example 1, as expected. As another application of the above construction, consider again the PQMC depicted on the right of Figure 2 where the super-operators decorating the transitions are \(\mathcal{E}_{0}=\{\ket{0}\bra{0}\}\) and \(\mathcal{E}_{1}=\{\ket{1}\bra{1}\}\). Then, the super-operator \(\mathcal{E}_{\mathfrak{M}}\) encoding \(\mathfrak{M}\) is  
\[\mathcal{E}_{\mathfrak{M}}= \{\ket{s_{1}}\bra{s_{0}}\otimes\mathcal{E}_{0}+\{\ket{s_{0}} \bra{s_{0}}\otimes\mathcal{E}_{1}\] \[+\{\ket{s_{2}}\bra{s_{1}}\otimes\mathcal{E}_{0}+\{\ket{s_{1}} \bra{s_{1}}\otimes\mathcal{E}_{1}\] \[+\{\ket{s_{1}}\bra{s_{2}}\otimes\mathcal{E}_{0}+\{\ket{s_{2}} \bra{s_{2}}\}\otimes\mathcal{E}_{1}.\]  
In practice, for each pair of states \(s\) and \(t\) for which \(\mathbf{Q}(s,t)\
eqq\mathcal{H}\), we add \(\{\ket{t}\bra{s}\}\otimes\mathbf{Q}(s,t)\), which can be intuitively interpreted as: we transition from \(s\) to \(t\) while performing \(\mathbf{Q}(s,t)\). We can now decompose \(\mathcal{E}_{\mathfrak{M}}\) into the BSCCs and the maximal transient space, obtaining that the maximal transient space of \(\mathcal{E}_{\mathfrak{M}}\) is \(T=\operatorname{span}\{\ket{s_{0}}\ket{0}\}\) and that the BSCCs are \[B_{1} =\text{span}\{\ket{s_{0}}\ket{1}\}, B_{2} =\text{span}\{\ket{s_{1}}\ket{1}\},\] \[B_{3} =\text{span}\{\ket{s_{1}}\ket{0},\ket{s_{2}}\ket{0}\}, B_{4} =\text{span}\{\ket{s_{2}}\ket{1}\}.\]  
Since the priorities range over \(\{0,1\}\), we obtain only \(\mathcal{BSCC}_{=0}=\bigvee\{B_{1},B_{2},B_{3}\}\) with even minimum priority, with corresponding projection super-operator (in Kraus notation)  
\[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}\,\}\]0  
which is also the projection super-operator \(\mathcal{P}_{cent}\) occurring in Theorem 1. Regarding the super-operator \(\mathcal{E}_{\mathfrak{M}}^{\infty}\), we first compute its components.