## 2 Quantum Markov Chains
For the reader familiar with the probabilistic setting, it is natural to consider the set \(\mathcal{S}^{\mathcal{I}}(\mathcal{H})\) as the quantum counterpart of the probability domain \([0,1]\). This is the underlying idea of the quantum Markov chains defined in [44]. Definition 1: A _super-operator weighted Markov chain_\(\mathfrak{M}\) over a Hilbert space \(\mathcal{H}\) is a pair \(\mathfrak{M}=(S,\mathbf{Q})\), where  
* \(S\) is a finite set of _classical states;
* \(\mathbf{Q}\colon S\times S\to\mathcal{S}^{\mathcal{I}}(\mathcal{H})\) is called the _transition matrix_ where for each \(s\in S\), the super-operator \(\sum_{s^{\prime}\in S}\mathbf{Q}(s,s^{\prime})\) is trace-preserving, that is \(\sum_{s^{\prime}\in S}\mathbf{Q}(s,s^{\prime})\eqsim\mathcal{I}_{\mathcal{H}}\). We just refer to this kind of Markov chains as _quantum Markov chains_ (QMCs). Similar to the setting of classical Markov chains, to talk about the (probability) measure of different events in a quantum Markov chain, we need to introduce a measurable space and the measure we want to use. The basic events of the measurable space will be based on the notion of path. Given a QMC \(\mathfrak{M}=(S,\mathbf{Q})\), we call a finite or infinite sequence \(\sigma=s_{0}s_{1}\cdots\) of states in \(S\) a _path_ of \(\mathfrak{M}\) if, for each valid index \(i\geq 1\), we have \(\mathbf{Q}(s_{i-1},s_{i})\
eq 0_{\mathcal{H}}\). We denote by \(\operatorname{Path}^{\mathfrak{M}}_{fin}\) the set of finite paths and by \(\operatorname{Path}^{\mathfrak{M}}\) the set of infinite paths. We let \(\sigma[i]\) denote the state \(s_{i}\). The basic events of our measurable space are the cylinder sets of finite paths. We define the _cylinder set_ of the finite path \(\sigma=s_{0}s_{1}\cdots s_{n}\) to be the set \(\operatorname{Cyl}(\sigma)=\{\ \sigma^{\prime}\in\operatorname{Path}^{ \mathfrak{M}}\mid\ \forall 0\leq i\leq n:\sigma[i]=\sigma^{\prime}[i]\ \}\). In practice, the cylinder set of a finite path \(\sigma\) contains all possible infinite paths that are an extension of \(\sigma\). Let \((\operatorname{Path}^{\mathfrak{M}},\Sigma)\) be a measurable space where \(\Sigma\) is the \(\sigma\)-algebra generated by all the cylinder sets \(\operatorname{Cyl}(\sigma)\) where \(\sigma\in\operatorname{Path}^{\mathfrak{M}}_{fin}\). For any \(s\in S\), we define the measure \(Q_{s}^{\mathfrak{M}}\colon\operatorname{Path}^{\mathfrak{M}}_{fin}\to \mathcal{S}(\mathcal{H})\) as follows. Given the finite path \(\sigma=s_{0}s_{1}\cdots s_{n}\),  
\[Q_{s}^{\mathfrak{M}}(s_{0}s_{1}\cdots s_{n})= \begin{cases}0_{\mathcal{H}}& \text{if $s_{0}\
eq s$;}\\ \mathcal{I}_{\mathcal{H}}&\text{if $s_{0}=s$ and $n=0$;}\\ \mathbf{Q}(s_{n-1},s_{n})\mathbf{Q}(s_{n-2},s_{n-1})\cdots\mathbf{Q}(s_{0},s_{ 1})&\text{if $s_{0}=s$ and $n>0$.}\end{cases} \]  
Then, \(Q_{s}^{\mathfrak{M}}\) induces a (super-operator valued) measure on \((\operatorname{Path}^{\mathfrak{M}},\Sigma)\), also denoted by \(Q_{s}^{\mathfrak{M}}\) for simplicity, by setting \(Q_{s}^{\mathfrak{M}}(\operatorname{Cyl}(\sigma))=Q_{s}^{\mathfrak{M}}(\sigma)\). According to [44] (Theorem 3.2), this measure is unique up to \(\approx\). In the reminder of the paper, we are interested in analyzing properties of a given QMC. We assign labels to the states of the QMC to indicate the basic properties that hold in each state, that is, we decorate each state of the QMC with the atomic propositions it satisfies. Atomic propositions represent some simple known facts we want to express about the single states of the system, such as \"the execution is terminated\", \"the measured qubits are different\", \"eavesdropping detected\", and so on. Thus, we consider an extension of QMCs in which each state obtains assigned atomic propositions by a labelling function. Definition 2: A labelled quantum Markov chain (LQMC) is a tuple \(\mathfrak{M}=(S,\mathbf{Q},AP,L)\) where \((S,\mathbf{Q})\) is a QMC and  
* _AP is a finite set of_ atomic propositions _and_
* \(L\colon S\to 2^{\mathcal{A}P}\) _is a_ labelling function.