鏈接：https://pan.baidu.com/s/1zDO0KajKZdZTj7zd-tBPGQ?pwd=707g?

提取碼：707g

本書系統(tǒng)且全面地梳理了模型檢測量子系統(tǒng)的原理以及基于這些原理的算法，涵蓋作者相關(guān)論文中的重要研究成果。本書講解如何應(yīng)用模型檢測技術(shù)來驗證量子工程系統(tǒng)的正確性、安全性和可靠性，包含步驟詳盡的算法以及豐富的示例和練習(xí)。書中首先介紹模型檢測和量子理論的基礎(chǔ)知識，然后討論量子自動機、量子馬爾可夫鏈和量子馬爾可夫決策過程的可達性問題，介紹求解這些問題所需的數(shù)學(xué)工具和算法，之后介紹一系列用于檢測超算子值馬爾可夫鏈的計算樹邏輯或線性時序邏輯的算法，后指明該領(lǐng)域的發(fā)展方向。

作者簡介

應(yīng)明生
清華大學(xué)計算機科學(xué)與技術(shù)系智能技術(shù)與系統(tǒng)國家重點實驗室教授，清華大學(xué)量子軟件研究中心主任。中國科學(xué)院軟件研究所研究員、學(xué)術(shù)副所長。悉尼科技大學(xué)量子軟件與信息中心杰出教授。曾獲中國青年科技獎、教育部自然科學(xué)一等獎、中國計算機學(xué)會王選獎一等獎。
他的研究領(lǐng)域包括量子計算、程序設(shè)計語言的語義學(xué)以及人工智能中的邏輯。他為量子程序建立了包括部分正確性與完全正確性的Floyd-Hoare型邏輯，特別是證明了其（相對）完備性。他將高級量子控制結(jié)構(gòu)引入量子語言中，以更加嚴格、完整和系統(tǒng)的形式推出了量子case結(jié)構(gòu)、量子遞歸結(jié)構(gòu)、二次量子化、量子程序疊加等一系列概念。
他著有Foundations of Quantum Programming（2016）和Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrent Programs（2001）。此外，他目前還擔任ACM Transactions on Quantum Computing的（聯(lián)合）主編。
馮元
悉尼科技大學(xué)量子軟件與信息中心教授。曾任清華大學(xué)計算機系副研究員。他的研究興趣包括量子系統(tǒng)的形式化驗證、量子程序理論、量子信息與計算以及概率系統(tǒng)。已在國際重要期刊和主流會議上發(fā)表論文70余篇。曾獲得澳大利亞研究理事會（ARC）未來研究基金（2010）。

目錄

譯者序
前言

第1章引言1
1.1第二次量子革命需要新的
驗證技術(shù)2
1.2經(jīng)典系統(tǒng)的模型檢測技術(shù)2
1.3模型檢測量子系統(tǒng)的困難3
1.4模型檢測量子系統(tǒng)的研究
現(xiàn)狀3
1.5本書結(jié)構(gòu)5
第2章模型檢測基礎(chǔ)7
2.1系統(tǒng)建模8
2.2時序邏輯10
2.2.1線性時序邏輯10
2.2.2計算樹邏輯13
2.3模型檢測算法16
2.3.1線性時序邏輯模型檢測
16
2.3.2計算樹邏輯模型檢測23
2.4模型檢測概率系統(tǒng)25
2.4.1馬爾可夫鏈和馬爾可夫
決策過程25
2.4.2概率時序邏輯26
2.4.3概率模型檢測算法27
2.5文獻注記30
第3章量子理論基礎(chǔ)31
3.1量子系統(tǒng)的狀態(tài)空間32
3.1.1希爾伯特空間32
3.1.2子空間35
3.1.3量子力學(xué)的基本假設(shè)I
36
3.2量子系統(tǒng)的動態(tài)過程36
3.2.1線性算子37
3.2.2酉算子39
3.2.3量子力學(xué)的基本假設(shè)II
40
3.3量子測量41
3.3.1量子力學(xué)的基本假設(shè)III
41
3.3.2投影測量42
3.4量子系統(tǒng)的復(fù)合44
3.4.1張量積44
3.4.2量子力學(xué)的基本假設(shè)IV
45
3.5混合態(tài)46
3.5.1密度算子46
3.5.2混合態(tài)的演化和測量47
3.5.3約化密度算子47
3.6量子操作48
3.6.1量子力學(xué)基本假設(shè)II的
一個推廣48
3.6.2量子操作的表示50
3.7文獻注記51
第4章模型檢測量子自動機53
4.1量子自動機54
4.2Birkhoffvon Neumann量子
邏輯56
4.3量子系統(tǒng)的線性時間性質(zhì)61
4.3.1基本定義61
4.3.2安全性質(zhì)62
4.3.3不變性63
4.3.4存活性質(zhì)66
4.3.5持續(xù)性質(zhì)67
4.4量子自動機的可達性70
4.4.1量子系統(tǒng)的(元)命題
邏輯71
4.4.2量子自動機可達性的
滿足72
4.5量子自動機不變性的檢測
算法74
4.6量子自動機可達性的檢測
算法77
4.6.1檢測

查看全部↓