Verifying Quantum Protocols via Quantum Probabilities

The development of Quantum Communication Protocols sparked the interest in quantum extensions of process calculi. However, existing semantic models, typically based on probability distributions and probabilistic transition systems, often fail to adequately capture the nuances of Quantum Mechanics. They can spuriously distinguish between systems that quantum theory deems identical, and allow for physically unfeasible non-deterministic capabilities. Furthermore, their reliance on concrete quantum states makes automated verification computationally intractable due to the infinite, continuous nature of the state space. To overcome these challenges, this thesis proposes to model quantum protocols in a novel manner, by leveraging both the mathematical language of Quantum Theory and the verification techniques of Computer Science. The main objective is to develop a verification framework that is both physically sound and amenable to symbolic, tractable analysis. This is achieved through the development of two novel models of quantum concurrent systems. The first major contribution is a new semantic model that respects quantum indistinguishability by construction. Quantum theory teaches us that probabilistic mixtures of quantum states should not be modelled as probability distributions. We thus introduce Density Distributions, where processes are weighted by density operators rather than scalar probabilities. We define an operational semantics based on these distributions and introduce Quantum Labelled Bisimilarity, the first behavioural equivalence to be a congruence under physically admissible scheduling policies. We show that our equivalence coincides with a purely observational, context-based, saturated bisimilarity, thus proving its adequacy in terms of discriminating power. The second core contribution is an elementary framework for the symbolic verification of quantum protocols. To abstract away from concrete quantum inputs, we develop a mathematical theory of Conditional Quantum Effects, a novel generalization of quantum effects capable of representing conditional probabilities arising from quantum measurements. Building on this foundation, we define Effect-weighted Labelled Transition Systems (eLTSs), an input-independent model for concurrent quantum systems. We propose a "Heisenberg-style" symbolic semantics that maps any quantum protocol to a single eLTS. We prove that symbolic bisimilarity on these eLTSs is fully abstract with respect to ground probabilistic bisimilarity: two symbolic systems are equivalent if and only if they yield equivalent pLTSs under all possible quantum inputs.