Model Checking Quantum Systems --- A Survey <s> C. Difficulty in Model Checking Quantum Systems <s> A system of quantum reasoning for a closed system is developed by treating nonrelativistic quantum mechanics as a stochastic theory. The sample space corresponds to a decomposition, as a sum of orthogonal projectors, of the identity operator on a Hilbert space of histories. Provided a consistency condition is satisfied, the corresponding Boolean algebra of histories, called a framework, can be assigned probabilities in the usual way, and within a single framework quantum reasoning is identical to ordinary probabilistic reasoning. A refinement rule, which allows a probability distribution to be extended from one framework to a larger (refined) framework, incorporates the dynamical laws of quantum theory. Two or more frameworks which are incompatible because they possess no common refinement cannot be simultaneously employed to describe a single physical system. Logical reasoning is a special case of probabilistic reasoning in which (conditional) probabilities are 1 (true) or 0 (false). As probabilities are only meaningful relative to some framework, the same is true of the truth or falsity of a quantum description. The formalism is illustrated using simple examples, and the physical considerations which determine the choice of a framework are discussed. \textcopyright{} 1996 The American Physical Society. <s> BIB001 </s> Model Checking Quantum Systems --- A Survey <s> C. Difficulty in Model Checking Quantum Systems <s> PREFACE ACKNOWLEDGEMENTS PART 1: PROBABILITY IN CLASSICAL AND QUANTUM MECHANICS 1. Classical probability theory and stochastic processes 2. Quantum Probability PART 2: DENSITY MATRIX THEORY 3. Quantum Master Equations 4. Decoherence PART 3: STOCHASTIC PROCESSES IN HILBERT SPACE 5. Probability distributions on Hilbert space 6. Stochastic dynamics in Hilbert space 7. The stochastic simulation method 8. Applications to quantum optical systems PART 4: NON-MARKOVIAN QUANTUM PROCESSES 9. Projection operator techniques 10. Non-Markovian dynamics in physical systems PART 5: RELATIVISTIC QUANTUM PROCESSES 11. Measurements in relativistic quantum mechanics 12. Open quantum electrodynamics <s> BIB002
Unfortunately, it seems that the current model-checking techniques cannot be directly applied to quantum systems because of some essential differences between the classical world and the quantum world. To develop model-checking techniques for quantum systems, the following three problems must be systematically addressed: • System modelling and property specification: The classical system modelling method cannot be used to describe the behaviours of quantum systems, and the classical specification language is not suited to formalise the properties of quantum systems to be checked. So, we need to carefully and clearly define a conceptual framework in which we can properly reason about quantum systems, including formal models of quantum systems and formal description of temporal properties of quantum systems. • Quantum measurements: Model-checking is usually applied to check long-term behaviours of the systems. But 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 studies of the long-term behaviours of quantum systems much harder than that of classical systems BIB001 , BIB002 ,  . • Algorithms: The state spaces of the classical systems that model-checking algorithms can be applied to are usually finite or countably infinite. However, the state spaces of quantum systems are inherently continuous even when they are finite-dimensional. In order to develop algorithms for model-checking quantum systems, we have to exploit some deep mathematical properties of the systems so that it suffices to examine only a finite number of (or at most countably infinitely many) representative elements, e.g. those in an orthonormal basis, of their state spaces. Also, a linear algebraic structure always resides in the state space of a quantum system. So, an algorithm checking a quantum system should be carefully developed so that the linear algebraic structure will not be broken.