csdn的大大們啊，求求你們了啊。修復這坨不能自動上傳的錯誤啊。好像已經三個月了啊。圖多的時候發文章真地很痛苦啊。orz orz orz
準備八卦edmund等人演算法時才想起，人2023年成名作是討論用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結合起來，我們就有了如下的基本操作符：
下面有一堆圖示。每幅圖都代表系統狀態的轉移。每坨節點表示系統在某一時刻的狀態。路徑表示系統狀態在不同時刻間的轉移。當前狀態是每坨狀態圖的根節點。當p在節點代表的狀態裡為真時，該節點塗成白色。如果p在節點代表的狀態裡為假，該節點塗成黑色。節點塗成灰色，表示我們不關心p的值—p可以為真也可以為假（是滴，排中律在這裡不重要。去掉排中律，我們就得到了intuitionistic logic。不過這是後話了）。
從上圖可以看出，ctl可以用來描述未來的多種可能性。系統在每一時刻都可能發展多個平行小宇宙。換句話說，在每一時刻系統的未來都可能「分叉」。所以ctl屬於分支時間邏輯（branching time logic）。因為節點可能分叉，ctl計算的結果是棵樹。這也是ctl全稱computational tree logic的由來。相比之下，ltl總是同時描述單條路徑的情況。因此，可以把ltl計算的結果是乙個集合。舉個例子。假設下圖是系統的狀態轉換。標籤a，b，c指代每坨狀態。如果狀態下有字母p，則表示p在該狀態為真。否則表示該狀態為假。
如果用ltl描述這套系統，我們只關心單個路徑。所以可能的情況無非是在最左邊的節點陷入迴圈：aw(這裡的指數符號w表示a無限重複)，要麼是從左邊開始，經過一定迴圈後，在最右邊陷入迴圈：anbcw。換句話說，我們可以判定：不管哪條路徑，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。可惜af ag p在上述系統中不成立，因為不管在哪條途徑上，我們都可以拐到節點b上，使得ag p為假。那ltl是不是ctl的超集囁？很可惜，也不是。比如ag ef p, 在ltl裡就找不到對應表達。
有不相容，便有比較。有比較，便有人要分個高下。於是長達30年的ltl vs. ctl辯論便從2023年pnuelli發表那篇時序邏輯的**時開始。flame war不是程式設計師的專利。總的來說，從邏輯的角度看。兩種語言各有長短。實際用於模型驗證時，眾多老大的意見是ltl的表達能力更強。但從計算的角度看，實現ctl模型驗證相對簡單。最後的結果是，模型驗證早期，弱即是強的kiss原則佔了上風，以smv為代表的ctl模型驗證軟體佔統治地位。不過風水輪流轉，後來大家又發現ltl寫的系統描述更容易理解，再加上ltl模型驗證的演算法有長足進步，cadence』s smv和spin這類用ltl的驗證軟體開始崛起。
八卦一下模型驗證 三
csdn的大大們啊，求求你們了啊。修復這坨不能自動上傳的錯誤啊。好像已經三個月了啊。圖多的時候發文章真地很痛苦啊。orz orz orz 準備八卦edmund等人演算法時才想起，人1986年成名作是討論用ctl computational tree logic 作規範語言的模型驗證演算法，而第一篇八...
八卦一下g9的八卦
八卦一下g9的八卦 早就想八卦一下g9老大 的技術八卦 了。國內技術社群能把技術和八卦整合得如此天衣無縫的，就我所知，僅此一家，別無分號。有時我就想不通乙個問題，為什麼這哥們文章中的八卦總是那麼源源不絕，信手拈來呢？我暗地裡琢磨這老大肯定私下有乙個小本本，上面的名人技術八卦按字母索引按年代索引按語言...
八卦一下g9的八卦
八卦一下g9的八卦 早就想八卦一下g9老大 的技術八卦 了。國內技術社群能把技術和八卦整合得如此天衣無縫的，就我所知，僅此一家，別無分號。有時我就想不通乙個問題，為什麼這哥們文章中的八卦總是那麼源源不絕，信手拈來呢？我暗地裡琢磨這老大肯定私下有乙個小本本，上面的名人技術八卦按字母索引按年代索引按語言...