## 5 Model Checking LTL and \(\omega\)-Regular Properties
### Parity Automata and Parity Quantum Markov Chains  
We shortly recall a well-known mechanism to decide whether a word is included in a given \(\omega\)-regular language. Recall that \(\mathcal{W}\) is called \(\omega\)-regular if it is the language of some nondeterministic Buchi automaton (cf. [27] (Theorem 4.32)) and that nondeterministic Buchi automata are equivalent to parity automata (cf. [63; 64; 65]). A parity automaton is defined formally as follows. **Definition 7**. : _A (deterministic) parity automaton (PA) is a tuple \(\mathfrak{A}=(A,\overline{a},AP,t,\mathsf{pri})\), where_  
* _A is a finite set of_ automaton states_;_
* \(\overline{a}\in A\) _is the_ initial state_;_
* _AP is a finite set of_ atomic propositions_;_
* \(t\colon A\times 2^{AP}\to A\) _is a_ transition function_; and_
* \(\mathsf{pri}\colon A\to\mathbb{N}\) _is a_ priority function_._  
A _path_ of \(\mathfrak{A}\) is an infinite sequence \(\sigma=a_{0}L_{0}a_{1}L_{1}\cdots\in(A\times 2^{AP})^{\omega}\), such that \(a_{0}=\overline{a}\) and for all \(i\geq 0\), \(a_{i+1}=t(a_{i},L_{i})\). We extend the priority function to paths by setting \(\mathsf{pri}(\sigma)=\lim\inf_{i\to\infty}\mathsf{pri}(a_{i})\). We use \(\mathsf{Path}^{\mathfrak{A}}\) to denote the set of all paths of \(\mathfrak{A}\). The _language_ of \(\mathfrak{A}\) is defined as  
\[\mathcal{L}(\mathfrak{A})=\{\,L_{0}L_{1}\cdots\in(2^{AP})^{\omega}\mid\exists \sigma=a_{0}L_{0}a_{1}L_{1}\cdots\in\mathsf{Path}^{\mathfrak{A}}:\mathsf{pri} (\sigma)\text{ is even }\}.\]  
As we have enriched QMCs with labels, obtaining LQMCs (cf. Definition 2), we also decorate QMCs with parity conditions, so to obtain parity QMCs; these will be useful to represent the result of the product of an LQMC and a PA, that we will present later. **Definition 8**. : _A parity quantum Markov chain (PQMC) is a tuple \(\mathfrak{M}=(S,\mathbf{Q},\mathsf{pri})\), where \((S,\mathbf{Q})\) is a QMC and \(\mathsf{pri}\colon S\to\mathbb{N}\) is a priority function._  
As we have done for LQMCs, we extend in the natural way the notion of paths, measures, etc. to PQMCs and we set \(\mathsf{pri}(s_{0}s_{1}s_{2}\cdots)=\lim\inf_{i\to\infty}\mathsf{pri}(s_{i})\). We define the _value_ of a PQMC \(\mathfrak{M}\) in \(s\in S\) as  
\[\mathsf{val}_{s}^{\mathfrak{M}}=Q_{s}^{\mathfrak{M}}(\{\,\sigma\in\mathsf{ Path}^{\mathfrak{M}}\mid\mathsf{pri}(\sigma)\text{ is even }\}).\]  
Parity QMCs can be obtained by combining together an LQMC and a PA; in practice, the PA just follows the evolution of the LQMC by synchronizing on the labels of the classical states that are visited by the LQMC. **Definition 9**. : _The product of an LQMC \(\mathfrak{M}=(S,\mathbf{Q},\mathbf{AP},L)\) and a PA \(\mathfrak{A}=(A,\overline{a},AP,t,\mathsf{pri})\) with the same set of atomic propositions \(\mathit{AP}\) is the PQMC \(\mathfrak{M}\otimes\mathfrak{A}=(S^{\prime},\mathbf{Q}^{\prime},\mathsf{pri} ^{\prime})\) where_  
* \(S^{\prime}=S\times A\)_;_
* \(\mathbf{Q}^{\prime}((s,a),(s^{\prime},a^{\prime}))=\mathbf{Q}(s,s^{\prime})\) _if_ \(a^{\prime}=t(a,L(s))\)_, and_ \(\mathbf{Q}^{\prime}((s,a),(s^{\prime},a^{\prime}))=0_{\mathcal{H}}\) _otherwise; and_
* \(\mathsf{pri}^{\prime}((s,a))=\mathsf{pri}(a)\)_._  
An important property that is used in the model checking problem of an LQMC \(\mathfrak{M}=(S,\mathbf{Q},\mathit{AP},L)\) against an \(\omega\)-regular property \(\mathcal{W}\) recognized by \(\mathfrak{A}=(A,\overline{a},\mathit{AP},t,\mathsf{pri})\) is that the value of \(\mathfrak{M}\otimes\mathfrak{A}=(S^{\prime},\mathbf{Q}^{\prime},\mathsf{pri }^{\prime})\) is trace equivalent to the super-operator corresponding to \(\mathcal{W}\) in \(\mathfrak{M}\).