## 1 Introduction
### How Can We Model Formally the Given Quantum Protocol? When modelling quantum systems for model checking them, one of the main characteristics we need to take into consideration is that a quantum system is, by its own nature, continuous. The state space of a quantum system is usually represented as a finite \(d\)-dimensional Hilbert space \(\mathcal{H}_{d}\) (the vector space \(\mathbb{C}^{d}\) equipped with an inner product operation), which is a continuum. Although the Hilbert space \(\mathcal{H}_{d}\) can be finitely represented, for instance by taking \(d\) pairwise orthogonal vectors forming a basis for \(\mathcal{H}_{d}\), the states in the state space are infinitely many. However, model checking usually expects to deal with finite state spaces, even when applied to continuous systems. For example, for continuous time Markov chains, the model still has a finite state space and the continuous time is represented by exponential distributions governing the delay in taking the transition from a state to another; for timed automata, the automaton has a finite number of locations and the continuous time is represented by clocks that increase uniformly and that enable, and possibly force, to take transitions to other locations. Depending on the formula to be analyzed, the continuous behavior of the system is first made discrete by applying different discretization techniques (such as regions and zones for timed automata), and then the obtained system is checked against the given property (cf. [26; 27]). Developing similar discretization techniques for quantum systems does not seem to be an easy task. Thus, researchers started to look for models with a finite number of states still able to encode the continuous quantum states. Instead of considering all quantum states of the system to analyze, [PERSON] et al. [39; 40] restricted the state space to a set of finitely describable stabilizer states; in addition, they also considered only quantum operations of the [PERSON] group. In this way, they were able to present an efficient model checker for quantum protocols based on purely classical algorithms; it has been implemented as an automatic tool that can be used to model check quantum communication protocols [41]. This approach, while being useful, is also limited: since it is based on stabilizer states, it does not extend to more general protocols involving non-stabilizer states. Independently from [PERSON] et al., [PERSON] et al. [42; 43] adopted a similar approach for the synthesis of quantum circuits. In their work, they use a symbolic reachability analysis to formulate the problem of the quantum logic synthesis problem; in this way, they reduce the original problem to a multiple-valued logic synthesis problem, which simplifies the search space and the complexity of the synthesis problem. In [44], [PERSON] et al. overcome these limitations. The model for quantum protocols they introduced is defined on top of classical Markov chains: it keeps the classical, discrete state space of a Markov chain and replaces the probability values decorating the transitions between states with super-operators. This means that quantum states and operations are unrestricted, thus it is possible to model general quantum protocols. We will present the model proposed by [44] in more details in Section 2 but, as an example, consider the simple loop program shown in the left part of Figure 1. This program first applies at line \(\ell_{0}\) the \(\frac{1}{2}\)-amplitude damping channel \(\mathcal{A}=\left\{E_{0},E_{1}\right\}\), where \(E_{0}=\left|0\right\rangle\left\langle 0\right|+\frac{1}{\sqrt{2}}\left|1 \right\rangle\left\langle 1\right|\) and \(E_{1}=\frac{1}{\sqrt{2}}\left|0\right\rangle\left\langle 1\right|\), on the quantum system \(q\) as initialization. Then, at line \(\ell_{1}\) it measures \(q\), by means of the two-outcome projective measurement \(M=\lambda_{0}\left|0\right\rangle\left\langle 0\right|+\lambda_{1}\left|1 \right\rangle\left\langle 1\right|\).