Model Checking Quantum Systems --- A Survey <s> VI. CONCLUSION <s> We address the question of which quantum states can be inter-converted under the action of a time-dependent Hamiltonian. In particular, we consider the problem as applied to mixed states, and investigate the difference between pure- and mixed-state controllabilities introduced in previous work. We provide a complete characterization of the eigenvalue spectrum for which the state is controllable under the action of the symplectic group. We also address the problem of which states can be prepared if the dynamical Lie group is not sufficiently large to allow the system to be controllable. <s> BIB001 </s> Model Checking Quantum Systems --- A Survey <s> VI. CONCLUSION <s> In this work, we show that very natural, apparently simple problems in quantum measurement theory can be undecidable even if their classical analogues are decidable. Undecidability hence appears as a genuine quantum property here. Formally, an undecidable problem is a decision problem for which one cannot construct a single algorithm that will always provide a correct answer in finite time. The problem we consider is to determine whether sequentially used identical Stern-Gerlach-type measurement devices, giving rise to a tree of possible outcomes, have outcomes that never occur. Finally, we point out implications for measurement-based quantum computing and studies of quantum many-body models and suggest that a plethora of problems may indeed be undecidable. <s> BIB002
As reviewed in previous sections, several theoretical frameworks and algorithms of quantum model-checking have been developed. But certainly, 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: 1) Checking physical systems: Physicists already considered the algorithmic checking problem of certain properties of quantum systems, for example, quantum measurement occurrence BIB002 and reachability of quantum states BIB001 . Quantum model-checking can offer a systematic view of this line of research. 2) 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.