I Markov Processes.- 1.1 Classical Mechanics.- 1.2 Movement of a Particle with Noise.- 1.3 Transition Probability and the Markov Property.- 1.4 Diffusion Equations.- 1.5 Brownian Motions.- 1.6 The Ito formula.- Appendix. Monotone Lemmas.- II Time Reversal and Duality.- 2.1 Time Reversal of Markov Processes and Duality.- 2.2 Space-Time Markov Processes and Space-Time Duality.- 2.3 Time Reversal and Schroedinger's Representation.- III Non-Relativistic Quantum Theory.- 3.1 Non-Relativistic Equation of Motion.- 3.2 Stationary States and Eigenvalue Problem.- 3.3 Time Reversal of Diffusion Processes.- 3.4 Duality Relation of Diffusion Processes.- 3.5 Equation of Motion in General Cases.- 3.6 Principle of Superposition of Markov Processes.- 3.7 Non-Relativistic Schroedinger Equation.- 3.8 State Preparations and Measurements.- 3.9 Diffusion or Schroedinger Equations ?.- 3.10 The First Technical Convention.- IV Stationary Schroedinger Processes.- 4.1 Stationary States.- 4.2 One-Dimensional Harmonic Oscillator.- 4.3 An Example in Two-Dimension.- 4.4 Superposition of Eigenfunctions.- 4.5 Further Excited States.- 4.6 Hydrogen Atom.- V Construction of the Schroedinger Processes.- 5.1 The Feynman-Kac Formula.- 5.2 Solving the Equation of Motion.- 5.3 Transformation by Multiplicative Functionals.- 5.4 Renormalization.- 5.5 A Variational Method.- 5.6 The Maruyama-Girsanov Formula.- 5.7 A Lagrangian Formulation.- 5.8 The Second Technical Convention.- VI Markov Processes with Jumps.- 6.1 Poisson and Compound Poisson Processes.- 6.2 Poisson Random measures and Point Processes.- 6.3 Stochastic Integrals with Poisson Point Processes.- 6.4 Levy Processes.- 6.5 Stable Processes.- 6.6 Bochner's Subordination.- 6.7 Duality of Subordinate Semi-Groups.- 6.8 Harmonic Transformation of Subordinate Semi-Groups.- 6.9 Duality of Fractional Powers of Time-Dependent Operators.- VII Relativistic Quantum Particles.- 7.1 A Relativistic Schroedinger Equation for a Spinless Paticle.- 7.2 Equation of Motion for Relativistic Quantum Particles.- 7.3 Stationary States of the Relativistic Schroedinger Equation.- 7.4 Stochastic Processes for Relativistic Spinless Particles.- 7.5 Non-Relativistic Limit.- 7.6 A Diffusion Approximation.- VIII Stochastic Differential Equations of Pure-Jumps.- 8.1 Markov Processes with the Generators of Fractional Power.- 8.2 Stochastic Differential Equations of Pure-Jumps.- 8.3 The Case with no Potential Term.- 8.4 To Solve the Stochastic Differential Equations of Pure-Jumps.- 8.5 To Construct Pure-Jump Markov Processes.- 8.6 A Remark on the Integrability Condition.- IX Variational Principle for Relativistic Quantum Particles.- 9.1 Absolute Continuity.- 9.2 Pure-Jump Markov Processes.- 9.3 A Multiplicative Functional.- 9.4 Renormalization and Variational Principle.- X Time Dependent Subordination and Markov Processes with Jumps.- 10.1 Time-Inhomogeneous Subordination.- 10.2 Lemmas.- 10.3 Stochastic Differential Equation with Jumps.- 10.4 A Formula of Feynman-Kac Type.- 10.5 Markov Processes with Jumps.- Appendix. Integration by Parts Formulae.- XI Concave Majorants of Levy Processes and the Light Cone.- 14.1 The Vertex Process of a Levy Process.- 14.2 Propositions on Random walks.- 14.3 Proof of Propositions on Random Walks.- 14.4 Proof of the main Theorems.- 14.5 Examples.- 14.6 The light Cone.- XII The Locality in Quantum Physics.- 12.1 Historical Overview.- 12.2 Hidden-Variable Theories.- 12.3 Locality of Hidden-Variable Theories.- 12.4 Spin-Correlation of Three Particles.- 12.5 Gudder's Hidden-Variable Theory.- 12.6 Spin-Correlations in Gudder's Theory.- 12.7 Some Remarks.- XIII Micro Statistical Theory.- 13.1 The Source of the Noise.- 13.2 Large Deviations of the Renormalized Processes.- 13.3 The Propagation of Chaos.- 13.4 Micro Statistical Mechanics.- 13.5 Propagation of Chaos of Pure-Jump Processes.- 13.6 Superposition of Movements.- 12.7 A Remark on the Gibbs Distribution.- XIV Processes on Open Time Intervals.- 14.1 Diffusion Processes on Open Time Intervals.- 14.2 Time-Reversed Schroedinger Processes.- 14.3 A Theorem of Jeulin-Yor.- 14.4 Reflecting Brownian Motion.- 14.5 Two-Sided Skorokhod Type Problem.- 14.6 Skorokhod Problem with Singular Drift.- 14.7 The Minimum and Maximum Solutions.- 14.8 The Uniqueness and Non-Uniqueness of Solutions.- 14.9 An Application: The Origin of Universes.- XV Creation and Killing of Particles.- 15.1 Non-Linear Differential Equations.- 15.2 Branching Markov Processes.- 15.3 The Expected Number of Particles.- 15.4 Killing.- XVI The lto Calculus.- 16.1 The Ito Integral.- 16.2 Martingales.- 16.3 The Ito Integral with Local Martingales.- 16.4 Ito's formula.- 16.5 Stochastic Differential Equations.- 16.6 Stochastic Differential Calculus.- References.
This is the first of a series of papers dealing with many-particle systems from a unified, nonperturbative point of view. It contains derivations and discussions of various field-theoretical techniques which will be applied in subsequent papers. In a short introduction the general method of approach is summarized, and its relationship to other field-theoretic problems indicated. In the second section the macroscopic properties of the spectra of many-particle systems are described. Asymptotic evaluations are performed which characterize these macroscopic features in terms of intensive parameters, and the relationship of these parameters to thermodynamics is discussed. The special characteristics of the ground state are shown to follow as a limiting case of the asymptotic evaluations. The third section is devoted to the time-dependent field correlation functions, or Green's functions, which describe the microscopic behavior of a multiparticle system. These functions are defined, and related to intensive macroscopic variables when the energy and number of particles are large. Spectral representations and other properties of various one-particle Green's functions are derived. In the fourth section the treatment of non-equilibrium processes is considered. As a particular example, the electromagnetic properties of a system are expressed in terms of the special two-particle Green's function which describes current correlation. The discussion yields specifically a fluctuation-dissipation theorem, a sum rule for conductivity, and certain dispersion relations. The fifth section deals with the differential equations which determine the Green's functions. The boundary conditions that characterize the Green's function equations are exhibited without reference to adiabatic decoupling. A method for solving the equations approximately, by treating the correlations among successively larger numbers of particles, is considered. The first approximation in this sequence is shown to yield a generalized Hartree-like equation. A related, but rigorous, identity for the single-particle Green's function is then derived. A second approximation, which takes certain two-particle correlations into account, is shown to produce various additional effects: The interaction between particles is altered in a manner characterized by the intensive macroscopic parameters, and the modification and spread of the energy-momentum relation come into play. In the final section compact formal expressions for the Green's functions and other physical quantities are derived. Alternative equations and systematic approximations for the Green's functions are obtained.
It is widely known that the commutative probability theory based on Kolmogorov's measure theoretic axioms and the quantum probability theory based on von Neumann's postulates were both created at about the same time in the 1930s (see, e.g., Kolmogorov [Kol50] and von Neumann [vNeu55] for the origins of these 2 very different but parallel lines of theory). Following Kolmogorov's original work, theory of the classical Markov processes has been the subject of intensive research for the last few decades. The classical theory, its applications, and their connections to other areas of research have been systematically developed by many prominent probabilists as illuminated by their widely referenced monographs such as those of Dynkin [Dyn62], Blumenthal and Getoor [BG68], Ethier and Kurtz [EK85], Renuv and Yor [RY99], and others. On the other hand, development of a complete theory of quantum stochastics such as quantum Markov processes has been progressing at a much slower pace in comparison with that of its classical counterpart. This is perhaps because development of a theory of quantum stochastics and quantum Markov processes requires an unusually large number of tools from operator theory and perhaps also because the probabilistic and analytical tools for understanding sample path behaviors of quantum stochastic processes have yet to be developed. The main goal of this monograph is to give a systematic exploration of relevant topics in quantum Markov processes in hopes of stimulating further research along this line and of stimulating interest in the classical stochastics community for research in its quantum counterpart. This monograph is written largely based on the current account of relevant research results by widely surveying relevant results contributed by many prominent researchers in quantum probability, quantum noise, quantum stochastic calculus, stochastic quantum differential equations, quantum Markov semigroups, strong quantum Markov processes, and large time asymptotic behaviors of quantum Markov semigroups through a systematic and self-contained introduction/presentation of these very interesting topics in an attempt to illuminate the rigor and beauty of quantum stochastics and quantum Markov processes.
After a qualitative discussion of the advantages of the density matrix and of the different ways to introduce it (the statistical, quantum mechanical and operational methods of approach), § 2 deals with the general properties of the density matrix, including a discussion of pure cases and mixtures. A brief discussion is given of Green function techniques and of the relation between Green functions and correlation functions. A discussion of recent developments in the evaluation of partition functions concludes the first part of this article dealing with the theory of density matrix techniques. Sections 5 to 9 discuss applications. The first application is the quantum-chemical one to many-body systems in their ground state, that is, systems at absolute zero, and it is shown how the density matrix fits into the Hartree-Fock and Thomas-Fermi schemes. A brief discussion is given of the theory of diamagnetism. This is followed by a discussion of non-equilibrium processes and of Kubo's approach to transport theory. After that the polarization of beams of electrons or of photons is discussed and it is indicated how density matrix techniques can be used to treat scattering processes. Section 9 concludes this part of the paper by a brief account of density matrix theory applications to resonance and relaxation phenomena. Finally, the theory of measurement in quantum mechanics is considered.
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.