前面說了謂詞邏輯。實際上謂詞邏輯還需要了解的有謂詞邏輯的語義推導和謂詞邏輯的完備性。不過這一塊的概念和思想都很複雜和繁冗，本系列略去。
基于模型是和基于證明相對的。前面我們一直在使用證明，好像看起來還不錯。不過在基于證明的進行中，系統描述是一組（适當的邏輯中的）公式Γ，而規範是另一個公式φ。驗證方法是試圖找到Γ├φ的證明。這需要指導和專業知識。
在基于模型的進行中，系統由适當邏輯的模型M表示。規範仍然由φ表示。驗證方法是計算M是否滿足φ，即M ╞ φ。這是自動的。是以基于模型的方法更簡單。
模型檢測基于時态邏輯 temporal logic。命題邏輯和謂詞邏輯中的公式真假是固定的，但是時态邏輯模型包含若幹狀态，具有動态真的性質，即公式可以随系統的狀态演化而改變其真值。
模型檢測中，模型M是遷移系統（下面會解釋這個概念），性質φ是時态邏輯公式。這樣驗證過程是：
1.使用模型檢測器的描述語言模組化，得到模型M；
2.用模型檢測器的規範語言對性質編碼，得到時态邏輯公式φ；
3.輸入M和φ，運作模型檢測器。
如果M ╞ φ，機器回答yes，否則no并輸出行為軌迹。
時态邏輯主要有兩類：線性時間邏輯LTL把時間看成是路徑的集合，路徑即時間瞬時的一個序列；分支時間邏輯CTL把時間表示為樹，以目前時間為根向未來分叉，使得未來的不确定性變得明确。
時态邏輯公式的真值依賴于模型内部的時間點。
現在說一下遷移系統的概念。遷移系統M = (S, →,L)是一個狀态集合S，帶有遷移關系→（S上的二進制關系），使得每個s ∈S有某個s’ ∈S，滿足s →s’，以及一個标記函數L：S →P（Atoms）。遷移系統簡稱模型。P（Atoms）表示Atoms的幂集，即原子描述集。L可以看作是對所有原子命題的一個真值指派。由于不止一個狀态，這種指派依賴于系統所處的狀态s：L(s)包含了狀态s下為真的所有原子。
說了這麼多，模型檢測要幹嘛呢？模型檢測就是對問題M ,s╞ φ是否成立進行計算的過程，其中：M 是所考慮系統的一個适當模型;s 是該模型的一個狀态;╞是滿足關系; φ是一個LTL或CTL公式。
這裡的研究工具是線性時态邏輯LTL。LTL帶有允許我們訓示未來的連接配接詞。它将時間模組化成狀态的序列，無限延伸到未來。該序列稱為計算路徑（或路徑）。由于未來的不确定性，我們要考慮若幹可能的路徑。
設立一個原子公式的集合Atoms。原子公式可能形如p,q,r，也可能是p1,p2,p3等。每個原子代表一個可能成立的原子事實。
LTL公式表達為 φ :: =┬|┴|p|(┐φ)|(φ∧φ)|(φ∨φ)|(φ→φ)|(Xφ)|(Fφ)|(Gφ)|(φUφ)|(φWφ)|(φRφ)
上面，p是Atoms中的原子；┬和┴是LTL公式，也是Atoms原子。φ 是LTL公式，是以┐φ也是。X是下一個狀态neXt; F是某未來狀态Future; G是所有未來狀态Globally; U是直到Until；R是釋放Rlease；W是弱直到Weak-until。
這就是線性時态邏輯文法。下面都是LTL執行個體：(((Fp) ∧(Gp)) →(pWr))， (F(p →(Gr)) ∨((┐q)Up))， (pW(qWr))， ((G(Fp)) →(F(q ∨s)))。LTL也有文法樹，下面是(F(p →(Gr)) ∨((┐q)Up))的文法樹：
一進制連接配接詞┐和時态連接配接詞X，F，G具有最高優先級，然後是U，R，W；接下來是∨和∧，最低的是→。這樣，上面幾個例子可以化簡為：Fp ∧Gp →pWr，F(p →Gr) ∨┐qUp，pW(qWr)，GFp →F(q ∨s)。
可以用有向圖來表示一個遷移系統：
S={s0,s1,s2}
→={s0 → s1, s0 → s2 , s1→s0, s1→s2,s2 → s2}
L(s0)={p,q},L(s1)={q,r},L(s2)={r}
模型M = (S, →,L)的一條路徑是S中狀态的無限序列s1,s2,s3,…,對于每個i ≥1，有si →si+1。該路徑記為s1 → s2 →…。路徑π1= s1 → s2 →…表示一個可能的未來。π 的上标表示起點的下标。
将遷移系統展開為一個無限計算樹很有用。這樣，模型M的執行路徑被明确表示出來：
設M = (S, →,L)是一個模型，π 是其中的一條路徑。π 是否滿足一個LTL公式，由滿足關系╞定義如下（裡面涉及到不能推導的符号，是以我隻能在PPT中做好截圖過來了）
通過這個滿足關系表可以立即明白XGFUWR各字母的意思了吧。
φUψ表示φ一直成立直到ψ成立。ψ成立後φ怎麼樣了？這裡展現不出來的。例如：
s代表“我吸煙”，t代表“我22歲”。則sUt：我吸煙一直到了22歲。不能表示22歲以後不吸煙。如果要這樣需要這樣表示sU(t ∧ G ┐ s)。
W和U類似。不過φWψ不要求ψ在某處會成立，而是φ可以一直成立下去。
φRψ等價于┐(┐φU┐ψ)，約等價于ψWφ，不過R可以取到i。
設M = (S, →,L)是一個模型，s∈S，且φ是一個LTL公式。如果對M 的每條始于s的執行路徑π，都有π╞ φ，則記為M，s ╞ φ。