CSDN的大大們啊，求求你們了啊。修復這坨不能自動上傳圖片的錯誤啊。好像已經三個月了啊。圖多的時候發文章真地很痛苦啊。Orz Orz Orz

準備八卦 Edmund等人 算法時才想起，人 1986年成名作 是討論用CTL ( Computational Tree Logic ) 作規范語言的模型驗證算法，而 第一篇八卦 失心瘋只介紹了LTL。雖說也有算法對付Kripke結構上的LTL模型驗證，但一來該算法的復雜度為 P-SPACE ，遠不如在Kripke結構上玩兒CTL的算法復雜度來得震撼；二來經典的LTL模型驗證方法是將LTL公式轉換為 Büchi Automata 后表演自動機理論與搜索算法的花活。三來俺的初衷是介紹今年圖靈獎得主Edmund等人的工作，鋪墊半天后突然跳到跟自動機理論有關的LTL模型驗證，大有相親卻看中女方伴娘的架勢，不夠厚道。所以這次先八卦CTL。下次再談算法。其實 Büchi Automata 這類有限狀態的無窮自動機妙趣無方，足夠另開系列細細八卦。

幸好 有LTL墊底 ，CTL也不難。同LTL一樣，CTL也支持時序操作符G, F, X, U。不同的是，CTL規定，這些時序操作符前必須加上路徑量詞A或者E。路徑量詞A表示從當前狀態開始所有的路徑，路徑量詞E則表示從當前開始某些路徑。這同一階謂詞邏輯里的全稱量詞?以及存在量詞?類似。將A、E同G、F、X、U結合起來，我們就有了如下的基本操作符：

• AG(φ): 在任何路徑上，公式φ永遠為真。
• AF(φ): 在任何路徑上，公式j在某個時刻一定會為真
• AX(φ): 在任何路徑上，下一個時刻公式j為真
• A(φ U y)：在任何路徑上，公式j一直為真，直到公式y為真
• EG(φ): 至少在一條路徑上，公式φ永遠為真。
• EF(φ): 至少在一條路徑上，公式j在某個時刻一定會為真
• EX(φ): 至少在一條路徑上，下一個時刻公式j為真
• E(φ U y)：至少在一條路徑上，公式j一直為真，直到公式y為真

下面有 一堆圖示 。每幅圖都代表系統狀態的轉移。每坨節點表示系統在某一時刻的狀態。路徑表示系統狀態在不同時刻間的轉移。當前狀態是每坨狀態圖的根節點。當p在節點代表的狀態里為真時，該節點涂成白色。如果p在節點代表的狀態里為假，該節點涂成黑色。節點涂成灰色，表示我們不關心p的值—p可以為真也可以為假（是滴，排中律在這里不重要。去掉排中律，我們就得到了 Intuitionistic Logic 。不過這是后話了）。

從上圖可以看出，CTL可以用來描述未來的多種可能性。系統在每一時刻都可能發展多個平行小宇宙。換句話說，在每一時刻系統的未來都可能“分叉”。所以CTL屬于分支時間邏輯（Branching Time Logic）。因為節點可能分叉，CTL計算的結果是棵樹。這也是CTL全稱Computational Tree Logic的由來。相比之下，LTL總是同時描述單條路徑的情況。因此，可以把LTL計算的結果是一個集合。舉個例子。假設下圖是系統的狀態轉換。標簽A，B，C指代每坨狀態。如果狀態下有字母P，則表示P在該狀態為真。否則表示該狀態為假。

如果用LTL描述這套系統，我們只關心單個路徑。所以可能的情況無非是在最左邊的節點陷入循環：A ^w (這里的指數符號w表示A無限重復)，要么是從左邊開始，經過一定循環后，在最右邊陷入循環：A ⁿ BC ^w 。換句話說，我們可以判定：不管哪條路徑，p最終會永遠為真。用LTL的公式表達就是：FG p。

用CTL描述上面的系統就要復雜多了。比如在節點A，任意時刻都面臨兩個選擇：要么繼續在A循環，要么到B。所以在CTL的描述下，系統是一顆無限展開的樹。我們可以用CTL判定在任何路徑上，最終某條分支 上p在所有狀態上都為真。用公式表達就是：AF EG p.

初學CTL和LTL時，容易錯誤地以為CTL是LTL的超集 – 在LTL公式的操作符前加上路徑量詞A不就是CTL了？可惜數學就是奇妙得讓人沮喪。就用上面的系統作例子。我們找不到對應LTL描述FG p的CTL公式。給FG p加上路徑量詞，我們得到AF AG p?？上F AG p在上述系統中不成立，因為不管在哪條途徑上，我們都可以拐到節點B上，使得AG p為假。那LTL是不是CTL的超集囁？很可惜，也不是。比如AG EF p, 在LTL里就找不到對應表達。

有不兼容，便有比較。有比較，便有人要分個高下。于是長達30年的LTL vs. CTL辯論便從1977年Pnuelli發表那篇時序邏輯的論文時開始。Flame war不是程序員的專利?？偟膩碚f，從邏輯的角度看。兩種語言各有長短。實際用于模型驗證時，眾多老大的意見是LTL的表達能力更強。但從計算的角度看，實現CTL模型驗證相對簡單。最后的結果是，模型驗證早期，弱即是強的KISS原則占了上風，以SMV為代表的CTL模型驗證軟件占統治地位。不過風水輪流轉，后來大家又發現LTL寫的系統描述更容易理解，再加上LTL模型驗證的算法有長足進步，Cadence’s SMV和SPIN這類用LTL的驗證軟件開始崛起。

八卦一下模型驗證(三)