Statistical Model Checking for Entanglement Swapping in Quantum Networks

Given the fragile, stochastic and time critical nature of quantum communication systems, it is useful to analyse them with the rigour of formal methods. However, computationally expensive methods like exact probabilistic model checking do not scale with the size of the quantum network. In this work, we analyse entanglement swapping, an important primitive in quantum networks, using statistical model checking. We investigate the robustness of entanglement swapping against important parameters like longevity of quantum memory, success probability of entanglement generation and Bell State Measurements, and heterogeneity of the quantum network nodes. We demonstrate the usefulness of the approach using the MultiVeStA statistical model checker and the SeQUeNCe quantum network simulator.