## 1 Introduction
### The Successful Story of Model Checking  
Since the seminal works of [PERSON] and [PERSON] [2] and [PERSON] and [PERSON] [3], model checking has gained a wide popularity in the formal verification community and in industry. This is mainly motivated by the fact that once the model checker gives green light to a system, we can be sure that the system that has been fed into the model checker fulfills all checked properties. On the other hand, if the model checker gives red light to some property, it is usually able to provide a counterexample witnessing why the specific property is violated; such a counterexample can be used by the developer to more easily trace the source of the bug and fix it. Model checking has been used in a variety of scenarios, from hardware [4; 5; 6; 7; 8] to software [9; 10; 11; 12; 13], from communication [14; 15; 16; 17] and security protocols [18] to pacemakers [19], from airplane and train control [20; 21] to satellites and spacecrafts [22; 23; 24; 25], just to cite a few examples; more applications of model checking can be found in literature and in several books summarizing the techniques and the results achieved by the researchers, see, e.g., [26; 27; 28; 29; 30; 31; 32; 33]. We can identify a few core aspects from these applications, which should be considered when choosing the model checking technique that best fits our needs. * The system can have a probabilistic behavior, as a result of internal random choices (such as the sampling of nonces in a security protocol) or of external uncertainty (the message is sent on a noisy channel that may alter it). * The system can have a nondeterministic behavior, as the result of multiple components running in parallel and interacting with each other in no predefined order. * The system needs to take care of the amount of time available for reacting to input or for completing its tasks: a collision avoidance system installed on an airplane needs to warn the pilot as soon as possible about the risk of the collision; it is certain that it needs to do so within the time limits imposed by the aviation authorities. Depending on the presence or the absence of these and other aspects, different models and model checking algorithms have been developed specifically for them. Given the successful application of model checking in several fields, researchers working on quantum systems considered the application of model checking techniques to verify the quantum protocols they were proposing. One of the obstacles in the manual verification of a quantum system is the fact that quantum mechanics is not really intuitive, since there are quantum phenomena for which researchers have no first-hand experience. Entanglement and superposition of the states, for instance, are not something that a person can encounter in daily life; probabilistic choices, instead, are at hand by just flipping a coin or rolling a dice. As a result, it is more likely for quantum designers to unintentionally introduce bugs in a protocol than for protocol designers working with classical systems, where they need to take care of nondeterministic and probabilistic aspects that can be experienced in our macro-scale world. Having erroneous protocols can have a large impact on the usability and reliability of quantum systems, in particular when their usage will become more practical by the advancements in the realization of quantum computers. Researchers working on quantum systems have already proposed quantum protocols, such as quantum coin-flipping [34; 35], quantum key distribution [34; 35; 36], and super-dense coding [37], that are at the core of quantum cryptography. Quantum cryptography can be considered a reasonable replacement for classical cryptography, in case the bases of the latter are mined by the achievements in quantum computation.