八卦一下模型驗證 三

2021-04-18 08:49:01 字數 2846 閱讀 2917

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原則佔了上風,以**v為代表的ctl模型驗證軟體佔統治地位。不過風水輪流轉,後來大家又發現ltl寫的系統描述更容易理解,再加上ltl模型驗證的演算法有長足進步,cadence』s **v和spin這類用ltl的驗證軟體開始崛起。

八卦一下模型驗證 三

csdn的大大們啊,求求你們了啊。修復這坨不能自動上傳的錯誤啊。好像已經三個月了啊。圖多的時候發文章真地很痛苦啊。orz orz orz 準備八卦edmund等人演算法時才想起,人1986年成名作是討論用ctl computational tree logic 作規範語言的模型驗證演算法,而第一篇八...

八卦一下g9的八卦

八卦一下g9的八卦 早就想八卦一下g9老大 的技術八卦 了。國內技術社群能把技術和八卦整合得如此天衣無縫的,就我所知,僅此一家,別無分號。有時我就想不通乙個問題,為什麼這哥們文章中的八卦總是那麼源源不絕,信手拈來呢?我暗地裡琢磨這老大肯定私下有乙個小本本,上面的名人技術八卦按字母索引按年代索引按語言...

八卦一下g9的八卦

八卦一下g9的八卦 早就想八卦一下g9老大 的技術八卦 了。國內技術社群能把技術和八卦整合得如此天衣無縫的,就我所知,僅此一家,別無分號。有時我就想不通乙個問題,為什麼這哥們文章中的八卦總是那麼源源不絕,信手拈來呢?我暗地裡琢磨這老大肯定私下有乙個小本本,上面的名人技術八卦按字母索引按年代索引按語言...