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

譯者序
前言
第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章中技術引理的證明
參考文獻