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