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.
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.
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.
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.
Past years have seen the development of a few proposals for quantum extensions of process calculi. The rationale is clear: with the development of quantum communication protocols, there is a need to abstract and focus on the basic features of quantum concurrent systems, like CCS and CSP have done for their classical counterparts. So far, though, no accepted standard has emerged, neither for the syntax nor for the behavioural semantics. Indeed, the various proposals do not agree on what should be the observational properties of quantum values, and as a matter of fact, the soundness of such properties has never been validated against the prescriptions of quantum theory. To this aim, we introduce a new calculus, Linear Quantum CCS (lqCCS), and investigate the features of behavioural equivalences based on barbs and contexts. Our calculus can be thought of as an asynchronous, linear version of qCCS, which is in turn based on value-passing CCS. The combination of linearity and asynchronous communication fits well with the properties of quantum systems (e.g. the no-cloning theorem), since it ensures that each qubit is sent exactly once, precisely specifying which qubits of a process interact with the context. We exploit contexts to examine how bisimilarities relate to quantum theory. We show that the observational power of general contexts is incompatible with quantum theory: roughly, they can perform non-deterministic moves depending on quantum values without measuring (hence perturbing) them. Therefore, we refine the operational semantics in order to prevent contexts from performing unfeasible non-deterministic choices. This induces a coarser bisimilarity that better fits the quantum setting: ( i ) it lifts the indistinguishability of quantum states to the distributions of processes and, despite the additional constraints, ( i i ) it preserves the expressiveness of non-deterministic choices based on classical information. To the best of our knowledge, our semantics is the first one that satisfies the two properties above.
Quantum communication is a rapidly growing area of research and development. While the successful construction of a large-scale quantum computer may be some years away, there are already commercial implementations of secure communication using quantum cryptography. The application of formal methods to classical communication and cryptographic systems has been very successful, and is now widely used in industry by organisations such as Intel, Microsoft and NASA. There is reason to believe that similar benefits can be expected for the verification of quantum systems. In this thesis, we focus on the use of process calculus, specifically Communicating Quantum Processes (CQP), for the analysis of quantum protocols. Congruence relations are an important aspect of process calculus, since they provide the foundation for equational reasoning. Previous work on congruence relations for quantum processes excluded the classical information arising from measurements, and was therefore unable to analyse many of the interesting known quantum communication protocols. Developing a congruence relation for general quantum processes is difficult because of the interaction between measurement, entanglement and parallel composition. We define a labelled transition relation for CQP in order to describe external interactions. Based on this semantics, we define a notion of observational equivalence for CQP processes, namely probabilistic branching bisimilarity. We find that this relation is not preserved by parallel composition, however we are able to gain a deeper understanding of the link between probabilistic branching and measurement. Based on this newfound understanding, we present a novel semantics for quantum processes, combining mixed quantum states with probabilistic branching. With respect to this new semantic model, we define full probabilistic branching bisimilarity and prove that it is a congruence. We use this congruence relation to discuss an axiomatic approach to the verification of quantum processes. The quantum teleportation protocol is used as a primary example throughout, and we prove that it is congruent to a quantum channel. We define a translation from CQP to the Quantum Model Checker (QMC) in order to provide automated verification techniques using CQP specifications. We prove that this translation preserves the semantics of CQP processes, thereby enabling a multifaceted approach to formal verification by enhancing the manual techniques of process calculus with the benefits of model checking.
Full formal descriptions of algorithms making use of quantum principles must take into account both quantum and classical computing components, as well as communications between these components. Moreover, to model concurrent and distributed quantum computations and quantum communication protocols, communications over quantum channels that move qubits physically from one place to another must also be taken into account. Inspired by classical process algebras, which provide a framework for modelling cooperating computations, a process algebraic notation is defined. This notation provides a homogeneous style for formal descriptions of concurrent and distributed computations comprising both quantum and classical parts. Based upon an operational semantics that makes sure that quantum objects, operations and communications operate according to the postulates of quantum mechanics, an equivalence is defined among process states considered as having the same behaviour. This equivalence is a probabilistic branching bisimulation. From this relation, an equivalence on processes is defined. However, it is not a congruence because it is not preserved by parallel composition.
Quantum cryptographic systems have been commercially available, with a striking advantage over classical systems that their security and ability to detect the presence of eavesdropping are provable based on the principles of quantum mechanics. On the other hand, quantum protocol designers may commit more faults than classical protocol designers since human intuition is poorly adapted to the quantum world. To offer formal techniques for modeling and verification of quantum protocols, several quantum extensions of process algebra have been proposed. An important issue in quantum process algebra is to discover a quantum generalization of bisimulation preserved by various process constructs, in particular, parallel composition, where one of the major differences between classical and quantum systems, namely quantum entanglement, is present. Quite a few versions of bisimulation have been defined for quantum processes in the literature, but in the best case they are only proved to be preserved by parallel composition of purely quantum processes where no classical communication is involved. Many quantum cryptographic protocols, however, employ the LOCC (Local Operations and Classical Communication) scheme, where classical communication must be explicitly specified. So, a notion of bisimulation preserved by parallel composition in the circumstance of both classical and quantum communication is crucial for process algebra approach to verification of quantum cryptographic protocols. In this article we introduce novel notions of strong bisimulation and weak bisimulation for quantum processes, and prove that they are congruent with respect to various process algebra combinators including parallel composition even when both classical and quantum communication are present. We also establish some basic algebraic laws for these bisimulations. In particular, we show the uniqueness of the solutions to recursive equations of quantum processes, which proves useful in verifying complex quantum protocols. To capture the idea that a quantum process approximately implements its specification, and provide techniques and tools for approximate reasoning, a quantified version of strong bisimulation, which defines for each pair of quantum processes a bisimulation-based distance characterizing the extent to which they are strongly bisimilar, is also introduced.