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.
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.
The development of quantum communication protocols sparked the interest in quantum extensions of process calculi and behavioural equivalences, but defining a bisimilarity that matches the observational properties of a quantum-capable system is a surprisingly difficult task. The two proposals explicitly addressing this issue, qCCS and lqCCS, do not define an algorithmic verification scheme: the bisimilarity of two processes is proven by comparing their behaviour under all input states. We introduce a new semantic model based on effects, i.e. probabilistic predicates on quantum states that represent their observable properties. We define and investigate the properties of effect distributions and effect labelled transition systems (eLTSs), generalizing probability distributions and probabilistic labelled transition systems (pLTSs), respectively. As a proof of concept, we provide an eLTS-based semantics for a minimal quantum process algebra, which we prove sound and complete with respect to the observable probabilistic behaviour of quantum processes. To the best of our knowledge, ours is the first algorithmically verifiable proposal that abides to the properties of quantum theory.
Reliable verification techniques for quantum communication protocols are of paramount importance, given their high implementation cost and critical contexts of application. Extensions of process calculi have been proposed, together with various notions of behavioural equivalence. However, their standard probabilistic models turn out to introduce some non-deterministic capabilities not aligned with the observational properties of physical quantum systems, leading to bisimilarity notions that distinguish physically equivalent processes. Nonetheless, non-deterministic features are fundamental to account for inputs, environments and adversarial behaviour. To address this issue, we propose lqCCS, a process calculus that integrates concurrency, non-determinism and quantum capabilities. We introduce a novel semantics in terms of distributions, where explicit physically admissible schedulers constrain probabilistic composition and forbid ill-defined non-deterministic moves, while preserving the expressivity needed to model real-world protocols. We investigate a scheduled version of saturated bisimilarity, pairing two processes if no observer can tell them apart, and we verify its adequacy by lifting a known result from quantum mechanics to lqCCS: equivalent processes acting on indistinguishable mixtures of quantum states are correctly recognized as bisimilar. Finally, we give an alternative semantics and a labelled bisimilarity based on a quantum generalization of probability distributions. This characterizes our behavioural equivalence as a congruence with respect to the parallel operator, enabling compositional reasoning without the need to explicitly check all possible contexts. We describe a rich class of lqCCS processes for which equivalence is decidable using standard techniques, and we analyse real-world quantum communication protocols.
Recent developments in the field of quantum communication demonstrate that secure communication protocols based on quantum features are already practical. Reliable verification techniques are of paramount importance for these technologies, given their high implementation cost and critical contexts of application. Extensions of process calculi such as CCS and 𝛑-calculus have been proposed in the literature, together with various notions of behavioural equivalence. However, their standard probabilistic models turn out to introduce some non-deterministic capabilities that are not aligned with the observational properties of physical quantum systems, leading to bisimilarity notions that distinguish processes that should be physically equivalent. Nonetheless, we argue that non-deterministic features are fundamental to account for inputs, environments and adversarial behaviour. To address this issue, we propose lqCCS, a process calculus that integrates concurrency, non-determinism and quantum capabilities. The calculus is enriched with a linear type system that enforces the no-cloning principle and resolves ambiguities in the visibility of ancillary qubits. We introduce a novel semantics in terms of distributions, where explicit physically admissible schedulers constrain probabilistic composition and forbid ill-defined non-deterministic moves, while preserving the expressivity needed to model real-world protocols. We investigate a scheduled version of saturated bisimilarity, deeming two lqCCS processes behaviourally equivalent if no observer can tell them apart. The adequacy of the approach is verified by lifting a known result from quantum mechanics to lqCCS, i.e., that equivalent processes acting on indistinguishable mixtures of quantum states are correctly recognized as bisimilar. Finally, we give an alternative semantics and a labelled bisimilarity based on a quantum generalization of probability distributions. This provides an equivalent characterization of our behavioural equivalence that is a congruence with respect to the parallel operator, enabling compositional reasoning without the need to explicitly check all possible contexts. We describe a rich class of lqCCS processes for which equivalence is decidable using standard techniques, and we analyse real-world quantum communication protocols.
Modeling and reasoning about concurrent quantum systems is very important both for distributed quantum computing and for quantum protocol verification. As a consequence, a general framework describing formally the communication and concurrency in complex quantum systems is necessary. For this purpose, we propose a model qCCS which is a natural quantum extension of classical value-passing CCS with the input and output of quantum states, and unitary transformations and measurements on quantum systems. The operational semantics of qCCS is given based on probabilistic labeled transition system. This semantics has many different features compared with the proposals in literature in order to describe input and output of quantum systems which are possibly correlated with other components. Based on this operational semantics, we introduce the notions of strong probabilistic bisimilarity and weak probabilistic bisimilarity between quantum processes and discuss some properties of them, such as congruence under various combinators.
Modeling and reasoning about concurrent quantum systems is very important for both distributed quantum computing and quantum protocol verification. As a consequence, a general framework formally describing communication and concurrency in complex quantum systems is necessary. For this purpose, we propose a model named qCCS. It is a natural quantum extension of classical value-passing CCS which can deal with input and output of quantum states, and unitary transformations and measurements on quantum systems. The operational semantics of qCCS is given in terms of probabilistic labeled transition system. This semantics has many different features compared with the proposals in the available literature in order to describe the input and output of quantum systems which are possibly correlated with other components. Based on this operational semantics, the notions of strong probabilistic bisimulation and weak probabilistic bisimulation between quantum processes are introduced. Furthermore, some properties of these two probabilistic bisimulations, such as congruence under various combinators, are examined.
Recent works have shown that defining a behavioural equivalence that matches the observational properties of a quantum-capable, concurrent, non-deterministic system is a surprisingly difficult task.We explore coalgebras over distributions taking weights from a generic effect algebra, which subsumes probabilities and quantum effects, a physical formalism that represents the probabilistic behaviour of an open quantum system.To abide by the properties of quantum theory, we introduce monads graded on a partial commutative monoid, intuitively allowing composition of two processes only if they use different quantum resources, as prescribed by the no-cloning theorem.We investigate the relation between an open quantum system and its probabilistic counterparts obtained when instantiating the input with a specific quantum state.We consider Aczel-Mendler and kernel bisimilarities, advocating for the latter as it characterizes quantum systems that exhibit the same probabilistic behaviour for all input states.Finally, we propose operators on quantum effect labelled transition systems, paving the way for a process calculi semantics that is parametric over the quantum input.