I. INTRODUCTION  
II. EARLY RESEARCH ON MODEL CHECKING OF QUANTUM SYSTEMS  
III. MODEL CHECKING QUANTUM AUTOMATA  
IV. MODEL CHECKING QUANTUM MARKOV CHAINS  
V. MODEL CHECKING SUPER-OPERATOR-VALUED MARKOV CHAINS  
VI. CONCLUSION