模型檢測量子系統：原理與算法 Model Checking Quantum Systems: Principles and Algorithms

應明生（Mingsheng Ying），“長江學者獎勵計劃”特聘教授，中青年有突出貢獻專家。清華大學計算機科學與技術系智能技術與系統國家重點實驗室教授，中國科學院軟件研究所研究員、學術副所長。悉尼科技大學傑出教授，量子計算與智能系統中心研究主管。曾獲中國青年科技獎，教育部自然科學一等獎，中國計算機學會王選獎一等獎。 應教授的研究領域包括量子計算、程序設計語言的語義學以及人工智能中的邏輯。他為量子程序建立了包括部分正確性與完全正確性的Floyd-Hoare型邏輯，特別是證明瞭其（相對）完備性。他將高級量子控制結構引入量子語言中，以更加嚴格、完整和系統的形式推出了量子case結構、量子遞歸結構、二次量子化、量子程序疊加等一系列概念。 此外，他還是《Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrent Programs》（Springer，2001）一書的作者。

譯者序
前言
第1章引言
1.1 第二次量子革命需要新的驗證技術
1.2 經典系統的模型檢測技術
1.3 模型檢測量子系統的困難
1.4 模型檢測量子系統的研究現狀
1.5 本書結構
第2章模型檢測基礎
2.1 系統建模
2.2 時序邏輯
2.2.1 線性時序邏輯
2.2.2 計算樹邏輯
2.3 模型檢測算法
2.3.1 線性時序邏輯模型檢測
2.3.2 計算樹邏輯模型檢測
2.4 模型檢測概率系統
2.4.1 馬爾可夫鍊和馬爾可夫決策過程
2.4.2 概率時序邏輯
2.4.3 概率模型檢測算法
2.5 文獻註記
第3章量子理論基礎
3.1 量子系統的狀態空間
3.1.1 希爾伯特空間
3.1.2 子空間
3.1.3 量子力學的基本假設I
3.2 量子系統的動態過程
3.2.1 線性算子
3.2.2 酉算子
3.2.3 量子力學的基本假設II
3.3 量子測量
3.3.1 量子力學的基本假設III
3.3.2 投影測量
3.4 量子系統的複合
3.4.1 張量積
3.4.2 量子力學的基本假設IV
3.5 混合態
3.5.1 密度算子
3.5.2 混合態的演化和測量
3.5.3 約化密度算子
3.6 量子操作
3.6.1 量子力學基本假設II的一個推廣
3.6.2 量子操作的表示
3.7 文獻註記
第4章模型檢測量子自動機
4.1 量子自動機
4.2 Birkhoff-von Neumann量子邏輯
4.3 量子系統的線性時間性質
4.3.1 基本定義
4.3.2 安全性質
4.3.3 不變性
4.3.4 存活性質
4.3.5 持續性質
4.4 量子自動機的可達性
4.4.1 量子系統的(元)命題邏輯
4.4.2 量子自動機可達性的滿足
4.5 量子自動機不變性的檢測算法
4.6 量子自動機可達性的檢測算法
4.6.1 檢測A|=If的最簡單情形
4.6.2 檢測A|=If的一般情形
4.6.3 檢測A|=Gf以及A=Uf
4.7 量子自動機可達性檢測的不可判定性
4.7.1 A|=Gf、A|=Uf和A|=If的不可判定性
4.7.2 A|=Ff的不可判定性
4.8 文獻註記
第5章模型檢測量子馬爾可夫鏈
5.1 量子馬爾可夫鏈
5.2 量子圖論
5.2.1 鄰接性和可達性
5.2.2 底部強連通分量
5.3 狀態希爾伯特空間的分解
5.3.1 瞬態子空間
5.3.2 底部強連通分量分解
5.3.3 週期性分解
5.4 量子馬爾可夫鏈的可達性分析
5.4.1 可達性概率
5.4.2 重複可達性概率
5.4.3 持續性概率
5.5 檢測量子馬爾可夫決策過程
5.5.1 不變子空間和可達性概率
5.5.2 經典MDP、POMDP和qMDP的比較
5.5.3 有限邊界下的可達性
5.5.4 無限邊界下的可達性
5.6 文獻註記
第6章模型檢測超算子值馬爾可夫鏈
6.1 超算子值馬爾可夫鏈
6.2 超算子值馬爾可夫鏈上的正算子值測度
6.3 正算子值時序邏輯
6.3.1 量子計算樹邏輯
6.3.2 線性時序邏輯
6.4 檢測超算子值馬爾可夫鏈的算法
6.4.1 模型檢測量子計算樹邏輯公式
6.4.2 模型檢測線性時序邏輯性質
6.5 文獻註記
第7章總結與展望
7.1 狀態空間爆炸
7.2 應用
7.2.1 量子電路的驗證與測試
7.2.2 量子密碼協議的驗證與分析
7.2.3 量子程序的驗證與分析
7.3 工具：量子系統的模型檢測器
7.4 從模型檢測量子系統到量子模型檢測
附錄A 第4章中技術引理的證明
附錄B 第5章中技術引理的證明
附錄C 第6章中技術引理的證明
參考文獻