## 1 Introduction
### How Can We Specify the Desired Properties? Once the quantum protocol has been modelled as a quantum Markov chain, we need to consider how to formalize the properties we want to analyze. For classical model checking problems, properties are expressed as formulas in some given logic; the most common ones are the Computation Tree Logic (CTL) [2], the Linear-time Temporal Logic (LTL) [45], and their combination CTL* [46]. CTL is a branching time logic that focuses on the possible future behaviors of a system, given by the different successors of the current state. This means that whenever we are in a state with multiple successors, we branch our future execution by considering all possible successors, such as the branches of a tree. CTL has two kinds of formulas: state formulas and path formulas. State formulas, as the name suggests, refer to the properties that each single state satisfies: basic facts represented by atomic propositions, conjunctions and negations of states formulas, and quantified path formulas, where the quantification is given by either the universal (\(\forall\)) or the existential (\(\exists\)) quantifier on the paths, i.e., the branches of the tree. Path formulas, instead, refer to what happens in the states that are visited along a single path, with different temporal operators characterizing the behavior of the sequence of states visited by the path. LTL, as the name indicates, is a linear time logic that considers what happens along a single execution of the system, instead of considering all alternatives as in CTL. This means that along the execution, all choices about the successor states have already been resolved. Since LTL focuses on a single, whole execution at a time, it has only one kind of formulas that combine freely Boolean and temporal operators. \(\omega\)-regular properties extend LTL, by directly specifying the executions that are \"good\"; \(\omega\)-regular properties are given as the language of an automaton accepting infinite words (cf. [27]). Figure 1: A simple loop program and its model as a quantum Markov chain. Depending on the characteristics of the system, such as the presence of probabilistic choices, rewards, or time information, these logics have been extended and adapted to use specific operators to take care of such additional characteristics. For instance, the probabilistic version of CTL, PCTL [47], replaces the path quantifiers of CTL with a single probability operator that is used to compute the probability of all paths satisfying the given path formula. PLTL [48] is similar: instead of requiring all paths to satisfy the formula, it just computes their probability and then checks whether it is bounded by the given threshold. This is a reasonable choice: in the probabilistic setting, a single path can violate the given path property; however, we can ignore it as long as its probability is negligible. When moving to quantum systems, the logic also needs to be adapted. In this work, we consider the quantum extension of CTL given in [44] and of LTL as presented in [49], as well as the extension of CTL with a fidelity operator proposed in [50]. The former two logics can be considered the natural extension of PCTL and PLTL to quantum systems: instead of computing the probability of the paths, we compute the super-operator \(\mathcal{E}\) accumulated along these paths and then we compare it with the given threshold super-operator \(\mathcal{F}\). Such a comparison intuitively represents the fact that the success probability of performing \(\mathcal{E}\) is bounded by the probability of performing \(\mathcal{F}\), independently from the initial state. The idea underlying this choice is to use the logics to characterize _classical_ aspects of the quantum system, given the fact that the quantum protocols usually aim at achieving some classical tasks, such as exchanging encryption keys or flipping coins. As an example of the properties we can express in this logic, we have the formula \(\mathbb{Q}_{\geq\mathcal{E}}[\mathcal{F}\delta_{3}]\).