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.
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.
Abstract Markov decision process (MDP) offers a general framework for modelling sequential decision making where outcomes are random. In particular, it serves as a mathematical framework for reinforcement learning. This paper introduces an extension of MDP, namely quantum MDP (qMDP), that can serve as a mathematical model of decision making about quantum systems. We develop dynamic programming algorithms for policy evaluation and finding optimal policies for qMDPs in the case of finite-horizon. The results obtained in this paper provide some useful mathematical tools for reinforcement learning techniques applied to the quantum world.
Abstract. In this paper, the aim is to develop a quantum counterpart to classical Markov decision processes (MDPs). First, we provide a very general formulation of quantum MDPs with state and action spaces in the quantum domain, quantum transitions, and cost functions. Once we formulate the quantum MDP (q-MDP), our focus shifts to establishing the verification theorem that proves the sufficiency of Markovian quantum control policies and provides a dynamic programming principle. Subsequently, a comparison is drawn between our q-MDP model and previously established quantum MDP models (referred to as QOMDPs) found in the literature. Furthermore, approximations of q-MDPs are obtained via finite-action models, which can be formulated as QOMDPs. Finally, classes of open-loop and classical-state-preserving closed-loop policies for q-MDPs are introduced, along with structural results for these policies. In summary, we present a novel quantum MDP model aiming to introduce a new framework, algorithms, and future research avenues. We hope that our approach will pave the way for a new research direction in discrete-time quantum control.
In this paper, we aim to develop a quantum counterpart to classical Markov decision processes (MDPs), referred to as q-MDPs. We first present a comprehensive formulation of quantum MDPs with state and action spaces in the quantum domain, quantum transitions, and cost functions. The focus then shifts to establishing a verification theorem for Markovian quantum control policies. Subsequently, we introduce classes of open-loop and classical-state-preserving closed-loop policies and present their structural results. Finally, we develop algorithms for computing optimal policies and value functions for both open-loop and classical-state-preserving closed-loop policies using the duality between dynamic programming and semi-definite programming formulations.
This paper introduces a novel approach to quantum state evolution by leveraging temporal logic formalisms. The core idea is to directly represent and reason about quantum state transitions, incorporating the inherent uncertainties of non-deterministic branching and measurement outcomes. We propose a new temporal logic variant, Temporal Probabilistic Logic (TPL), where quantum state transitions are defined as logical rules and measurement collapses are modeled as probabilistic branches within the temporal reasoning process. This purely logical framework contrasts with traditional numerical simulation methods used in quantum control theory, offering potential advantages in automated proof of correctness, algorithm design, and optimization. TPL allows for the formal specification of quantum protocols and the verification of their behavior without relying on computationally intensive simulations. The paper outlines the key components of TPL, including its syntax, semantics, and operational rules, and explores its application to a simplified quantum algorithm. The presented framework provides a foundation for developing a more robust and verifiable approach to quantum computation.