Book contents
- Frontmatter
- Contents
- Preface
- Acknowledgements
- 1 Introduction
- 2 Basics of Model Checking
- 3 Basics of Quantum Theory
- 4 Model Checking Quantum Automata
- 5 Model Checking Quantum Markov Chains
- 6 Model Checking Super-Operator-Valued Markov Chains
- 7 Conclusions and Prospects
- Appendix 1 Proofs of Technical Lemmas in Chapter 4
- Appendix 2 Proofs of Technical Lemmas in Chapter 5
- Appendix 3 Proofs of Technical Lemmas in Chapter 6
- References
- Index
5 - Model Checking Quantum Markov Chains
Published online by Cambridge University Press: 14 January 2021
Book contents
- Frontmatter
- Contents
- Preface
- Acknowledgements
- 1 Introduction
- 2 Basics of Model Checking
- 3 Basics of Quantum Theory
- 4 Model Checking Quantum Automata
- 5 Model Checking Quantum Markov Chains
- 6 Model Checking Super-Operator-Valued Markov Chains
- 7 Conclusions and Prospects
- Appendix 1 Proofs of Technical Lemmas in Chapter 4
- Appendix 2 Proofs of Technical Lemmas in Chapter 5
- Appendix 3 Proofs of Technical Lemmas in Chapter 6
- References
- Index
Summary
This chapter develops model-checking techniques for a much larger class of quantum systems modelled as quantum Markov chains or more generally, quantum Markov decision processes. The differences between quantum automata and quantum Markov systems require us to develop algorithms for the latter that are fundamentally different from those for the former.
Keywords
- Type
- Chapter
- Information
- Model Checking Quantum SystemsPrinciples and Algorithms, pp. 87 - 137Publisher: Cambridge University PressPrint publication year: 2021