## 5 Model Checking LTL and \(\omega\)-Regular Properties
### The Standard Automata-Based Approach Does Not Work Directly for LQMCs
In addition to this problem with the classification of \(s_{0}\), we also have a second problem, namely, that the infinite path \((s_{0})^{\alpha}\) has minimum priority 0, so it must be taken into account when computing the super-operator corresponding to the accepting paths. This means that it does not suffice to look only at the states as performed for classical parity Markov chains, but we need to consider all possible paths. Consider now the state \(s_{1}\): we have only two infinite paths occurring with nonzero super-operator, namely \((s_{1})^{\alpha}\) with associated super-operator \(\{\left|1\right\rangle\left\langle 1\right|\}\) and priority 0, and \((s_{1}s_{2})^{\alpha}\) with associated super-operator \(\{\left|0\right\rangle\left\langle 0\right|\}\) and priority 0. Thus, the super-operator corresponding to the accepting paths in state \(s_{1}\) is \(\{\left|0\right\rangle\left\langle 0\right|\}+\{\left|1\right\rangle\left\langle 1 \right|\}\eqsim\mathcal{I}_{\mathcal{H}}\). The situation for \(s_{2}\) is however different: we still have only two paths, namely \((s_{2}s_{1})^{\alpha}\) with associated super-operator \(\{\left|0\right\rangle\left\langle 0\right|\}\) and priority 0, and \((s_{2})^{\alpha}\) having super-operator \(\{\left|1\right\rangle\left\langle 1\right|\}\) and priority 1. Thus, the value in \(s_{2}\) is \(\{\left|0\right\rangle\left\langle 0\right|\}\), that is different from \(\mathcal{I}_{\mathcal{H}}\) in \(s_{1}\). Therefore, we have a third problem, namely, we cannot associate the same value to all states in a BSCC, as we can do for classical Markov chains, but each state must be evaluated individually. Let us reason more about what happens along the path \(s_{2}s_{2}s_{1}s_{1}s_{1}\cdots\): its corresponding super-operator is \(0_{\mathcal{H}}\), as effect of the composition of the two orthogonal super-operators \(\mathcal{E}_{1}=\{\left|1\right\rangle\left\langle 1\right|\}\) and \(\mathcal{E}_{0}=\{\left|0\right\rangle\left\langle 0\right|\}\) in the first two transitions \(s_{2}\xrightarrow{\mathcal{E}_{1}}s_{2}\) and \(s_{2}\xrightarrow{\mathcal{E}_{0}}s_{1}\), respec  
Figure 2: Example showing that BSCC decomposition for the underlying graph does not work for model checking parity QMCs. tively. In practice, it is as the first transition from \(s_{2}\) to \(s_{2}\), decorated with \(\mathcal{E}_{1}\), \"disables\" the second transition from \(s_{2}\) to \(s_{1}\), decorated with \(\mathcal{E}_{0}\). In other words, it is like we are missing the Markovian property that allows us to forget about the past, namely that the transitions we can perform depend only on the current state, not on how we reached it. Therefore, we cannot assume that the underlying graph is immutable, since the previous transitions we performed to reach the current state might change the available edges in the underlying graph. This means that we cannot just use the standard BSCC decomposition algorithms on the underlying graph to solve the LTL and \(\omega\)-regular model checking problem for LQMCs: neither are BSCCs reached with certainty, nor do all states of a BSCC have the same value. In addition, the value of a state in a BSCC can be different from both \(0_{\mathcal{H}}\) and \(\mathcal{I}_{\mathcal{H}}\). In order to overcome these problems, in [49] we proposed an alternative approach: instead of relying on the graph structure of the product \(\mathfrak{M}\otimes\mathfrak{A}\), we transformed it into a single super-operator and we considered the BSCC decomposition of the classical-quantum Hilbert space induced by this super-operator, i.e., the tensor product of the classical state space with the quantum one. By operating on this larger Hilbert space, we have the information we need to solve the model checking problem for \(\omega\)-regular properties for labelled quantum Markov chains.