模型檢測是一種主要用于驗證有限狀態(tài)系統(tǒng)的動態(tài)性質(zhì)的算法技術(shù)。經(jīng)過35年以上的發(fā)展，已經(jīng)成為一種重要的硬件和軟件系統(tǒng)驗證技術(shù)，并在信息與通信技術(shù)（ICT）行業(yè)中得到了許多成功的應(yīng)用。模型檢測的特殊吸引力主要得益于以下兩個特征：
�r完全自動的；
�r當性質(zhì)不滿足時提供反例，因此在調(diào)試中作用顯著。
由于計算和通信系統(tǒng)中存在各種隨機現(xiàn)象，模型檢測已被系統(tǒng)地擴展用于驗證概率系統(tǒng)，例如馬爾可夫鏈和馬爾可夫決策過程。
隨著量子計算和量子通信的出現(xiàn)，特別是其在過去幾年的快速發(fā)展，人們自然期望進一步擴展模型檢測技術(shù)以驗證量子系統(tǒng)。事實上，從將概率模型檢測直接應(yīng)用于量子系統(tǒng)（特別是量子通信協(xié)議）開始，對模型檢測量子系統(tǒng)的研究已經(jīng)進行了10多年。在處理越來越一般的量子系統(tǒng)時，人們逐漸認識到，模型檢測量子系統(tǒng)需要某些與經(jīng)典系統(tǒng)（包括概率系統(tǒng)）從根本上不同的原理。在近期的研究中，模型檢測量子系統(tǒng)的一些基本原理得到了發(fā)展，但相關(guān)研究成果分散在各種會議和期刊論文中。
本書試圖系統(tǒng)地闡述到寫作時間為止提出的模型檢測量子系統(tǒng)的原理以及基于這些原理的算法。本書末尾簡要討論了一些潛在的應(yīng)用和未來研究的主題。希望本書可以作為研究人員踏入這一新領(lǐng)域時的入門指南，并為該領(lǐng)域的進一步發(fā)展奠定基礎(chǔ)。
本書還計劃作為研究生的教學(xué)用書，因此其內(nèi)容組織基于一定的教學(xué)目標。鑒于量子計算和信息的學(xué)習(xí)者可能具備計算機科學(xué)或物理學(xué)背景，在章節(jié)的安排上，第2章和第3章為預(yù)備章節(jié)，其中第2章為物理學(xué)背景的學(xué)生簡要介紹模型檢測，第3章為計算機科學(xué)背景的學(xué)生簡要介紹量子理論。之后，從簡單的模型和檢測性質(zhì)到更復(fù)雜的模型和檢測性質(zhì)，逐步介紹量子系統(tǒng)的模型檢測技術(shù)。
致謝
本書的材料主要來自作者及合作者的一系列論文。在此感謝俞能昆博士、李楊佳博士、應(yīng)圣鋼博士和官極博士，與他們的合作愉快且富有成效。沒有他們的貢獻，這本書是不可能完成的。
本書中的工作得到了中國國家重點研發(fā)計劃（批準號：2018YFA0306701）、澳大利亞研究委員會（批準號：DP160101652和DP180100691）、中國國家自然科學(xué)基金（批準號：61832015）和中國科學(xué)院前沿科學(xué)重點研究計劃的支持。謹此致謝。