An effective, accessible abstraction hierarchy has made using and programming computers possible for people across all disciplines. Establishing such a hierarchy for quantum programming is an outstanding challenge, especially due to a proliferation of different conventions and the rapid pace of innovation. One critical portion of the hierarchy is the abstract machine, the layer that separates a programmer's mental model of the hardware from its physical realization. Drawing on historical parallels in classical computing, we explain why having the “right” quantum abstract machine (QAM) is essential for making progress in the field and propose a novel framework for evaluating QAMs based on a set of desirable criteria. These criteria capture aspects of a QAM such as universality, compactness, expressiveness, and composability, which aid in the representation of quantum programs. By defining this framework we take steps toward defining an optimal QAM. We further apply our framework to survey the landscape of existing proposals, draw comparisons, and assess them based on our criteria. While these proposals share many common strengths, we find that each falls short of our ideal. Our framework and our findings set a direction for subsequent efforts to define a future QAM that is both straightforward to map to a variety of quantum computers, and provides a stable abstraction for quantum software development.
An effective, accessible abstraction hierarchy has made using and programming computers possible for people across all disciplines. Establishing such a hierarchy for quantum programming is an outstanding challenge, especially due to a proliferation of different conventions and the rapid pace of innovation. One critical portion of the hierarchy is the abstract machine, the layer that separates a programmer's mental model of the hardware from its physical realization. Drawing on historical parallels in classical computing, we explain why having the "right" quantum abstract machine (QAM) is essential for making progress in the field and propose a novel framework for evaluating QAMs based on a set of desirable criteria. These criteria capture aspects of a QAM such as universality, compactness, expressiveness, and composability, which aid in the representation of quantum programs. By defining this framework we take steps toward defining an optimal QAM. We further apply our framework to survey the landscape of existing proposals, draw comparisons, and assess them based on our criteria. While these proposals share many common strengths, we find that each falls short of our ideal. Our framework and our findings set a direction for subsequent efforts to define a future QAM that is both straightforward to map to a variety of quantum computers, and provides a stable abstraction for quantum software development.
We describe model-checking techniques for protocols arising in quantum information theory and quantum cryptography. We discuss the theory and implementation of a practical model checker, QMC, for quantum protocols. In our framework, we assume that the quantum operations performed in a protocol are restricted to those within the stabilizer formalism; while this particular set of operations is not universal for quantum computation, it allows us to develop models of several useful protocols as well as of systems involving both classical and quantum information processing. We discuss the modeling language of QMC, the logic used for verification, and the verification algorithms that have been implemented in the tool. We demonstrate our techniques with applications to a number of case studies, including quantum teleportation and the BB84 quantum coin-flipping protocol. 11.1 Introduction Model-checking is a method of computer-aided verification used widely in both academia and industry for the analysis of software and communication systems. The method essentially consists of three phases: (1) modeling the system of interest at a suitable level of abstraction, usually by describing it in a formal specification language; (2) specifying the properties that the system must satisfy – these properties are typically expressed with reference to the system model, using a logic designed specially for this purpose ( e.g. , linear or branching time temporal logic); and (3) supplying the model and the properties to a model-checking tool, which automatically constructs the state space of the model and checks whether or not the given properties are satisfied (and if not, usually providing a counterexample).
We establish fundamental and general techniques for formal verification of quantum protocols. Quantum protocols are novel communication schemes involving the use of quantum-mechanical phenomena for representation, storage and transmission of data. As opposed to quantum computers, quantum communication systems can and have been implemented using present-day technology; therefore, the ability to model and analyse such systems rigorously is of primary importance. While current analyses of quantum protocols use a traditional mathematical approach and require considerable understanding of the underlying physics, we argue that automated verification techniques provide an elegant alternative. We demonstrate these techniques through the use of PRISM, a probabilistic model-checking tool. Our approach is conceptually simpler than existing proofs, and allows us to disambiguate protocol definitions and assess their properties. It also facilitates detailed analyses of actual implemented systems. We illustrate our techniques by modelling a selection of quantum protocols (namely superdense coding, quantum teleportation, and quantum error correction) and verifying their basic correctness properties. Our results provide a foundation for further work on modelling and analysing larger systems such as those used for quantum cryptography, in which basic protocols are used as components.
We are currently in the midst of a second quantum revolution: transition from quantum theory to quantum engineering (e.g. quantum computing, communication, sensing). The main purpose of quantum theory is to find fundamental rules governing the existing physical systems. In contrast, quantum engineering aims at designing and implementing new systems (machines, devices, etc.) to achieve some desirable tasks, based on quantum theory. From experience in today's engineering, it is not always easy for a human designer to completely understand the behaviours of the system that she/he is designing, and an error in her/his design may cause serious problems and even disasters. Consequently, theories and methodologies for verification of correctness, safety and reliability of complex engineering systems have been systematically studied in various engineering fields. In particular, computer scientists have developed techniques to verify the correctness of both hardware and software as well as the security of communication protocols. Human intuition is poorly adapted to the quantum world compared to the classical world, which implies that human engineers will make many more mistakes in designing and implementing complex quantum systems such as quantum computer hardware and software and communication protocols. Even worse, because of the essential differences between the classical and quantum worlds, verification techniques for classical systems cannot be directly used for quantum systems. Novel verification techniques will be indispensable for the coming era of quantum engineering and technology. Model-checking is an effective technique to check whether a system satisfies a desired property. The properties that are checked are usually specified in a temporal logic; typical properties are deadlock freedom, invariants, safety, and request–response properties. The systems being checked are mathematically modelled as e.g. (finite-state) automata, transition systems, Markov chains and Markov decision processes [1]. In the last three decades, model-checking has become one of the dominant techniques for verification of computer hardware and software, and has proved mature as witnessed by a large number of successful industrial applications. Techniques of model-checking were even applied in systems biology recently. With the emergence of quantum engineering and quantum technology, a question then naturally arises: is it possible to apply model-checking techniques in verifying the correctness and safety of quantum engineering systems, and how can this be done? Unfortunately, due to some essential differences between classical and quantum systems, it seems unlikely that the classical model-checking techniques can be directly applied to quantum systems. Basically, to make model-checking techniques effective for quantum systems, the following three problems must be systematically addressed: System modelling and property specification: Behaviours of quantum systems cannot be described using classical modelling methods and, consequently, the properties of the quantum systems to be checked cannot be formalized by classical specification languages. As a result, novel conceptual frameworks must be proposed to properly model and consider quantum systems, including formal models and formal descriptions of temporal properties of quantum systems. Quantum measurements: Model-checking is usually applied to check the long-term behaviours of systems. However, to check whether a quantum system satisfies a certain property at a time point, one has to perform a quantum measurement on the system, which can change the state of the system. This makes studying the long-term behaviours of quantum systems much harder than with classical systems. Algorithms: Classical model-checking algorithms normally assume the state spaces to be finite or countably infinite. However, state spaces of quantum systems are inherently continuous. To develop algorithms for model-checking quantum systems, deep mathematical properties of the systems have to be exploited, so that a finite (or countably infinite) number of representative elements in the state spaces will suffice. Note that the state space of any quantum system has a natural linear algebraic structure. A well developed algorithm for verifying quantum systems should make clever use of this structure. Despite the difficulties discussed above, a few model-checking techniques for quantum systems have been developed in the last 10 years. The earliest work mainly targeted checking quantum communication protocols: Taking the probabilism arising from quantum measurements into account, the probabilistic model-checker PRISM was used in [2] to verify the correctness of quantum protocols, including superdense coding, quantum teleportation and quantum error correction. A branching-time temporal extension of exogenous quantum propositional logic was introduced and then the model-checking problem for this logic was studied in [3], with verification of the correctness of quantum key distribution BB84 as an application. A linear temporal extension of exogenous quantum propositional logic was then defined and the corresponding model-checking problem was investigated in [4]. Model-checking techniques were developed in [5] for quantum communication protocols modelled in process algebra CQP (communicating quantum processes) [6]. A model-checker for quantum communication protocols was also developed in [7], where only the protocols that can be modelled as quantum circuits expressible in the stabilizer formalism were considered. This technique was further extended beyond stabilizer states and used to check equivalence of quantum protocols. A research line pursued by the authors and their collaborators is to develop model-checking techniques that can be used not only for quantum communication protocols but also for general quantum systems, including physical systems and quantum programs. Quantum automata were adopted in [8,9] as the model of the systems: Definition 1(Quantum automata [10]). A quantum automaton is a 4-tuple |
A=(H,Act,{Uα:α∈Act},H0)|, where: 1) |
H| is a finite-dimensional Hilbert space, called the state space; 2) |
Act| is a finite set of action names; 3) for each action name |
α∈Act|, Uα is a unitary operator on |
H|; 4) |
H0⊆H| is the subspace of initial states. A quantum automaton behaves as follows: it starts from some initial state in |
H0|, and at each step it performs a unitary transformation Uα for some |
α∈Act|. An algorithm for checking certain linear-time properties (e.g. invariants and safety properties) was proposed in [8], where, following Birkhoff–von Neumann quantum logic, closed subspaces of the state Hilbert space are used as the atomic propositions about the state of the system, and the checked linear-time properties are defined as infinite sequences of sets of atomic propositions. Furthermore, the decidability or undecidability of several reachability problems for quantum automata were established in [9]. The model-checking problem for a larger class of quantum systems than quantum automata, namely quantum Markov chains, was studied in [11]. Note that continuous-time quantum Markov processes have been studied intensively in mathematical physics. Discrete-time quantum Markov chains were recently introduced as a semantic model for quantum programs. Definition 2 (Quantum Markov chains [11]). A quantum Markov chain is a triple |
(H,E,H0)|, where |
H| and |
H0| are the same as in Definition 1, and |
E| is a super-operator on |
H|. A quantum Markov chain starts in an initial state in |
H0|, and at each step it performs the (same) quantum operation modelled by the super-operator |
E|. Note that the (discrete-time) dynamics of closed quantum systems is usually depicted by unitary operators, and the behaviours of open quantum systems are described by super-operators. Obviously, the notion of quantum automata can be generalized by replacing unitary operators Uα in Definition 1 by super-operators |
Eα|. Furthermore, quantum Markov decision processes [12] can be defined by introducing decision strategies into such generalized quantum automata. Several algorithms for checking the reachability of quantum Markov chains and quantum Markov decision processes have been developed. As in checking classical Markov chains and Markov decision processes, graph reachability is a key to these algorithms. However, classical graph theory is not suited to our purpose; instead, a new theory of quantum graphs (i.e. graphs in a Hilbert space with an adjacency relation induced by a super-operator) was developed and, in particular, an algorithm for the BSCC (bottom strongly connected components) decomposition of the state Hilbert spaces was found in [11]. Another decomposition technique, namely periodic decomposition, for quantum Markov chains has recently been proposed. The notion of the super-operator-valued Markov chain is introduced in [13] as a higher-level model of quantum programs and quantum cryptographic protocols. Definition 3 (Super-operator-valued Markov chains [13]). A labelled super-operator-valued Markov chain over a set AP of predefined atomic propositions is a 5-tuple |
(S,s0,H,Q,L)|, where: 1) S is a finite set of classical states with s0 ∈ S being the initial state; 2) |
H| is a finite-dimensional Hilbert space, called the quantum state space; 3) |
Q:S×S→SOH| is a transition super-operator function, where |
SOH| denotes the set of trace-nonincreasing super-operators on |
H| and, for each s ∈ S, ∑t ∈ SQ(s, t) is trace-preserving; and 4) L: S → 2AP is a labelling function. A super-operator-valued Markov chain has two state spaces, a classical one and a quantum one, which are connected through the transition super-operator function. It behaves in a similar manner to classical Markov chains. It starts from the classical initial state s0 but with the quantum initial state unspecified (it can be taken arbitrarily). Then at each step, given the current classical state s and quantum state ρ, it proceeds to a classical state t with probability tr[Q(s, t)(ρ)], and the accompanying quantum state evolves into Q(s, t)(ρ)/tr[Q(s, t)(ρ)] provided that tr[Q(s, t)(ρ)] ≠ 0. The normalization requirement that ∑t ∈ SQ(s, t) is trace-preserving guarantees that the probabilities of going from s to some classical state sum up to 1. As the atomic propositions are taken to be classical (they apply only to classical states), this Markov chain model is suitable for verification of quantum systems against classical properties, such as running time, termination, reachability, etc. One distinct feature of this model, however, is that it allows us to check the properties of the system once and for all; i.e. the verified results apply to all initial quantum states. For example, the model-checking algorithm for the reachability problem essentially calculates a positive operator Π, accounting for all (classical) paths satisfying the concerned property. Then the reachability probability when the Markov chain starts in the initial quantum state ρ is simply tr(Πρ). A corresponding computation tree logic (CTL) for super-operator-valued Markov chains was defined, and algorithms for checking such properties were developed in [13]. A tool implementation of these algorithms has been provided [14] based on a probabilistic model-checker. Algorithms for model-checking ω-regular properties, a general class of properties subsuming linear temporal logic (LTL) formulas, against super-operator-valued Markov chains have been proposed [15], thus allowing analysis of a wide range of properties such as repeated reachability, reachability in a restricted order, and nested Until properties. Furthermore, the reachability problem of a recursive extension of super-operator-valued Markov chains was studied in [16], with the application of analysing quantum programs with procedure calls. As reviewed in previous sections, several theoretical frameworks and algorithms of quantum model-checking have been developed. Certainly, however, quantum model-checking is still at a very early stage of its development; in particular, its applications are only at the level of toy examples. We envisage that, in the future, quantum model-checking techniques can be applied to the following areas: Checking physical systems: Physicists have already considered the algorithmic checking problem of certain properties of quantum systems, e.g. quantum measurement occurrence [17] and reachability of quantum states [18]. Quantum model-checking can offer a systematic view of this line of research. Verification of quantum circuits: Verification of circuits has been one of the major application areas of classical model-checking. But model-checking applied to verification of quantum circuits is an area to be systematically exploited. Analysis and verification of quantum programs: Another important application area of classical model-checking is analysis and verification of programs. Several techniques for analysis and verification of quantum programs have been reported in the last few years [19,20]. However, model-checking techniques specifically designed for quantum programs are still missing. Verification of security of quantum communication protocols: Applications of model-checking mentioned in the section entitled ‘Early research on model-checking of quantum systems' focus on verification of the correctness of quantum communication protocols. However, verification of the security of quantum protocols is much more difficult, and model-checking applied to it is an interesting topic for future research.
This paper applies to quantum systems a modelling for the logic of knowledge, originally developed for reasoning about distributed systems, but since then applied to game theory, computer security and artificial intelligence. A formal model of quantum message passing systems is developed and the question of how one might define the semantics of a modal operator for knowledge in this model is considered. It is argued that there are at least two plausible semantics, depending on whether the agents are permitted to make use of their quantum state in determining what they know, and on whether one is dealing with single instances of quantum systems, or ensembles. The framework is illustrated using a number of examples from the quantum computing literature, including protocols for quantum key distribution and teleportation. 1