## 5 Model Checking LTL and \(\omega\)-Regular Properties
### The Standard Automata-Based Approach Does Not Work Directly for LQMCs  
In the remainder of this section, we present how the approach used to check Markov chains against \(\omega\)-regular properties can be extended to quantum Markov chains. The only difference between classical Markov chains and quantum Markov chains is the use of super-operators instead of probability values to decorate the transitions; this difference, however, has a considerable effect on the model checking algorithm, as pointed out in, e.g., [49; 72]. Consider the two Markov chains, enriched with a parity acceptance condition, shown in Figure 2. The parity acceptance is provided by the priorities 0 and 1 labelling the classical states \(s_{0}\), \(s_{1}\), and \(s_{2}\). As we will see more formally below, a path is accepted if the minimum priority occurring infinitely often is even. This means, for instance, that the path \(s_{0}s_{1}s_{2}s_{1}s_{2}\cdots\) is accepted, since its corresponding sequence of priorities is \(00101\cdots\) whose minimum priority occurring infinitely often is 0; on the other hand, the path \(s_{2}s_{2}\cdots\) is rejecting, since its minimum priority occurring infinitely is 1. The Markov chain on the left of Figure 2 is a classical one where transitions are governed by the two transition probabilities \(p\) and \(1-p\) with \(0<p<1\). The Markov chain on the right is a quantum one governed by the two super-operators \(\mathcal{E}_{0}\) and \(\mathcal{E}_{1}\), such that \(\mathcal{E}_{0},\mathcal{E}_{1}\
eq 0_{\mathcal{H}}\) and \(\mathcal{E}_{0}+\mathcal{E}_{1}\simeq\mathcal{I}_{\mathcal{H}}\). It is obvious that both Markov chains have the same classical state space, thus they have exactly the same underlying graph. If we would define the BSCCs just by looking at the underlying graph, they would have the same set of BSCCs, namely just the single BSCC \(\{s_{1},s_{2}\}\), and the same single transient state \(s_{0}\). However, we will see that this BSCC technique does not help in the evaluation of parity QMCs. In the classical Markov chains model, \(s_{0}\) is a transient state that will eventually reach almost surely the unique BSCC \(\{s_{1},s_{2}\}\). Thus, its priority makes no difference. Since the probability that both states in the BSCC are visited infinitely often is 1, we have that the BSCC \(\{s_{1},s_{2}\}\) is marked as accepting, since the minimum priority of its states is 0. Since the BSCC \(\{s_{1},s_{2}\}\) is accepting and all paths from \(s_{1}\) eventually enter \(\{s_{1},s_{2}\}\) almost surely, we find that the overall probability of the paths eventually becoming trapped in an accepting BSCC is 1 for all states. Consider now the quantum Markov chain on the right part of Figure 2 and assume that \(\mathcal{E}_{0}=\{\left|0\right\rangle\left\langle 0\right|\}\) and \(\mathcal{E}_{1}=\{\left|1\right\rangle\left\langle 1\right|\}\). Note that for \(i\in\{0,1\}\) it holds \(\mathcal{E}_{i}\mathcal{E}_{i}=\mathcal{E}_{i}\) and \(\mathcal{E}_{i}\mathcal{E}_{1-i}=0_{\mathcal{H}}\). It is easy to check that if we start from \(s_{0}\), the infinite path \(s_{0}s_{0}\cdots\), with the corresponding _nonzero_ super-operator \(\lim_{n\to\infty}\mathcal{E}_{1}^{n}=\{\left|1\right\rangle\left\langle 1\right|\}\), never leaves \(s_{0}\) to reach the other states \(s_{1}\) and \(s_{2}\). This means that \(s_{0}\) cannot be considered a BSCC, since \(s_{0}\) cannot reach itself almost surely, i.e., with super-operator \(\mathcal{I}_{\mathcal{H}}\). At the same time, \(s_{0}\) cannot be considered a transient state, since it will not eventually reach a BSCC almost surely. Therefore, the first problem we encounter is that a state in a QMC cannot be classified either as transient or as belonging to a BSCC, as happens for classical Markov chains.