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