Model Checking Quantum Systems: Principles and Algorithms

Half Title page
Title page
Copyright page
Contents
Preface
Acknowledgements
1 Introduction
	1.1 Second Quantum Revolution Requires New Verification Techniques
	1.2 Model-Checking Techniques for Classical Systems
	1.3 Difficulty in Model Checking Quantum Systems
	1.4 Current Research on Model Checking of Quantum Systems
	1.5 Structure of the Book
2 Basics of Model Checking
	2.1 Modelling Systems
	2.2 Temporal Logics
		2.2.1 Linear Temporal Logic
		2.2.2 Computation Tree Logic
	2.3 Model-Checking Algorithms
		2.3.1 LTL Model Checking
		2.3.2 CTL Model Checking
	2.4 Model Checking Probabilistic Systems
		2.4.1 Markov Chains and Markov Decision Processes
		2.4.2 Probabilistic Temporal Logics
		2.4.3 Probabilistic Model-Checking Algorithms
	2.5 Bibliographic Remarks
3 Basics of Quantum Theory
	3.1 State Spaces of Quantum Systems
		3.1.1 Hilbert Spaces
		3.1.2 Subspaces
		3.1.3 Postulate of Quantum Mechanics I
	3.2 Dynamics of Quantum Systems
		3.2.1 Linear Operators
		3.2.2 Unitary Operators
		3.2.3 Postulate of Quantum Mechanics II
	3.3 Quantum Measurements
		3.3.1 Postulate of Quantum Mechanics III
		3.3.2 Projective Measurements
	3.4 Composition of Quantum Systems
		3.4.1 Tensor Products
		3.4.2 Postulate of Quantum Mechanics IV
	3.5 Mixed States
		3.5.1 Density Operators
		3.5.2 Evolution of and Measurement on Mixed States
		3.5.3 Reduced Density Operators
	3.6 Quantum Operations
		3.6.1 A Generalisation of Postulate of Quantum Mechanics II
		3.6.2 Representations of Quantum Operations
	3.7 Bibliographic Remarks
4 Model Checking Quantum Automata
	4.1 Quantum Automata
	4.2 Birkhoff-von Neumann Quantum Logic
	4.3 Linear-Time Properties of Quantum Systems
		4.3.1 Basic Definitions
		4.3.2 Safety Properties
		4.3.3 Invariants
		4.3.4 Liveness Properties
		4.3.5 Persistence Properties
	4.4 Reachability of Quantum Automata
		4.4.1 A (Meta-)Propositional Logic for Quantum Systems
		4.4.2 Satisfaction of Reachability by Quantum Automata
	4.5 Algorithm for Checking Invariants of Quantum Automata
	4.6 Algorithms for Checking Reachability of Quantum Automata
		4.6.1 Checking A ⊨ I f for the Simplest Case
		4.6.2 Checking A ⊨ I f for the General Case
		4.6.3 Checking A ⊨ G f and A ⊨ U f
	4.7 Undecidability of Checking Reachability of Quantum Automata
		4.7.1 Undecidability of A ⊨ G f, A ⊨ U f and A ⊨ I f
		4.7.2 Undecidability of A ⊨ F f
	4.8 Final Remark
	4.9 Bibliographic Remarks
5 Model Checking Quantum Markov Chains
	5.1 Quantum Markov Chains
	5.2 Quantum Graph Theory
		5.2.1 Adjacency and Reachability
		5.2.2 Bottom Strongly Connected Components
	5.3 Decomposition of the State Hilbert Space
		5.3.1 Transient Subspaces
		5.3.2 BSCC Decomposition
		5.3.3 Periodic Decomposition
	5.4 Reachability Analysis of Quantum Markov Chains
		5.4.1 Reachability Probability
		5.4.2 Repeated Reachability Probability
		5.4.3 Persistence Probability
	5.5 Checking Quantum Markov Decision Processes
		5.5.1 Invariant Subspaces and Reachability Probability
		5.5.2 Comparison of Classical MDPs, POMDPs and qMDPs
		5.5.3 Reachability in the Finite Horizon
		5.5.4 Reachability in the Infinite Horizon
	5.6 Final Remarks
	5.7 Bibliographic Remarks
6 Model Checking Super-Operator-Valued Markov Chains
	6.1 Super-Operator-Valued Markov Chains
	6.2 Positive Operator–Valued Measures on SVMCs
	6.3 Positive Operator–Valued Temporal Logic
		6.3.1 Quantum Computation Tree Logic
		6.3.2 Linear Temporal Logic
	6.4 Algorithms for Checking Super-Operator-Valued Markov Chains
		6.4.1 Model Checking QCTL Formulas
		6.4.2 Model Checking LTL Properties
	6.5 Bibliographic Remarks
7 Conclusions and Prospects
	7.1 State Space Explosion
	7.2 Applications
		7.2.1 Verification and Testing of Quantum Circuits
		7.2.2 Verification and Analysis of Quantum Cryptographic Protocols
		7.2.3 Verification and Analysis of Quantum Programs
	7.3 Tools: Model Checkers for Quantum Systems
	7.4 From Model Checking Quantum Systems to Quantum Model Checking
Appendix 1 Proofs of Technical Lemmas in Chapter 4
	A1.1 Proof of Lemma 4.36
	A1.2 Proof of Lemma 4.39
	A1.3 Skolem’s Problem for Linear Recurrence Sequences
	A1.4 Skolem’s Problem in Matrix Form
	A1.5 Constructing Quantum Automata from Minsky Machines
		A1.5.1 Encoding Classical States into Quantum States
		A1.5.2 Simulating Classical Transitions by Unitary Operators
		A1.5.3 Construction of V and W
Appendix 2 Proofs of Technical Lemmas in Chapter 5
	A2.1 Proof of Lemma 5.25 (ii)
	A2.2 Proof of Lemma 5.30
	A2.3 Proof of Lemma 5.34
	A2.4 Proof of Lemma 5.58
Appendix 3 Proofs of Technical Lemmas in Chapter 6
	A3.1 Proof of Theorem 6.21 (iii)
	A3.2 Proof of Lemma 6.31
	A3.3 Proof of Lemma 6.32
	A3.4 Proof of Lemma 6.33
	A3.5 Proof of Lemma 6.34
	A3.6 Proof of Lemma 6.35
References
Index