本站小編為你精心準備了模型檢測網絡傳播的策略參考范文，愿這些范文能點燃您思維的火花，激發您的寫作靈感。歡迎深入閱讀并收藏。

1.網絡傳播模型與干預策略問題

網絡是由大量個體通過相互作用或者聯系構成的有機整體。現實世界中存在大量這樣的網絡，比如由計算機、人或者森林構成的網絡，其中的個體狀態隨著鄰接點的影響而發生動態改變。網絡以及其中個體間的相互作用可以形式化地通過圖表示。假設G(V,E)是一個圖，頂點集1{...}nV=vv表示網絡中的個體，邊的集合E表示能夠導致傳播的個體間的連接。每個頂點iv∈v有一個與之對應的狀態()iσv，取值為“感染”（infected）或者“易感“（open）。對圖中每個頂點定義一個由鄰接點構成的集合(){|(,)}ijijρv=v∈Vvv∈E。節點iv的狀態變化由鄰接點的狀態以及iv當前的狀態決定，用傳遞函數f描述[1]。同時，采用局部更新函數g描述節點iv感染后受其自身影響所產生的狀態變化[1]。一般來說，根據節點感染后能否重新恢復成易感狀態，我們可以將其分為兩類：（1）不可恢復和（2）可恢復。以人類的某些傳染疾病例，有些疾病憑借著人自身的免疫力，經過一段時間可自愈，這就是可恢復情形。但也有部分疾病無法自愈，這就是不可恢復情形。對于不可恢復情形，具體來講，節點iv由易感狀態變為感染狀態的條件是至少需要它的鄰接點中有k個是感染的，對應的函數f定義如下：而在不可恢復情形中，由于感染的節點可以恢復，即經過一段時間（比如r）,感染節點的狀態變為易感，所以需要記錄節點感染時間長度,用infectedk表示一個節點已經被感染了k個時刻，那么初始感染的狀態即為infected1，對應的函數定義如下：以上所描述的是未采取干預策略的網絡傳播模型。為了描述干預策略對傳播模型的影響，對節點增加“保護”狀態（protected）。被保護的節點將一直保持保護狀態，因此不會被感染和用于傳播。干預策略的基本思想是通過對部分易感節點進行保護，隔離其它未保護的易感節點和感染節點，實現對網絡傳播的控制。如果干預策略能將感染節點的數量控制在給定的范圍內，則稱其是有效的。干預策略通常受到各種因素制約，例如被保護節點數量，實施節點保護的時機等。本文研究不同的網絡傳播類型，根據給定的目標和資源判斷并找出有效的保護策略。根據實施方式的不同，干預策略問題可以分為兩類：（1）靜態保護問題和（2）動態保護問題。在靜態保護問題中，對于易感節點的選擇和保護在初始時刻一次性完成，即對于給定結構的傳播模型要求在t=0時刻從易感節點中隨機選取固定數目(比如m個)的節點進行保護，使得最終感染節點的數量不超過預定的數目。另一方面在現實世界中，由于受運輸或保護資源數量等限制，無法一次性保護大量的節點，而只能通過每次保護部分節點，采取分批次方式實施保護，這就是動態保護問題，比如消防員問題。動態保護問題要求在t=0時刻，從易感節點中隨機選取數量不多于固定值d的節點進行保護，在隨后的各個時刻，即t=1，2，…，當節點的狀態完成更新后，不斷重復選擇和保護節點的過程，直到網絡中沒有新的節點被感染，使得在整個過程中感染的節點數量控制在給定數目內。與網絡傳播模型相對應，根據節點感染后能否恢復為易感染狀態,即g函數類型的不同，靜態保護和動態保護問題又都可以分為不可恢復和可恢復兩種情形。其中，可恢復情形由于g不再是單調函數，因此取決于節點被感染的速率和感染節點恢復的速率，感染節點的數量可能增加也可能減少：如果節點被感染節點的速率大于恢復速率，則感染節點的數量增加；否則，感染節點數量減少。所以這種情況下的干預策略問題更為復雜。綜上所述，可以將網絡傳播中的干預策略問題分為四類：（1）不可恢復的靜態保護問題(staticunrecoverableproblem)、（2）可恢復的靜態保護問題(staticrecoverableproblem)、（3）不可恢復的動態保護問題(dynamicunrecoverableproblem)以及（4）可恢復的動態保護問題(dynamicrecoverableproblem)。由于可恢復的動態保護問題最為復雜，接下來我們以圖1為例對其做相關說明。假設傳遞函數f中k為1，即當前易感染節點只要存在一個感染狀態的鄰接點，下一時刻它必被感染。另外設g函數中r為1，即經過一個時間感染節點恢復到易感狀態。初始網絡中只有節點0和2被感染（黑色實心圓），d為1，即每次只能保護1個易感節點。干預策略的目標是將感染節點的數量控制在2以內。可以找到這樣一種可行的干預策略：在t=0時刻，保護節點5（灰色實心圓）。t=1時刻，節點1和3根據f函數被感染，而節點2和4根據g函數恢復為易感狀態，這時感染節點的數量還是2；在t=2時刻，繼續保護節點4；在t=3時刻，節點0和2被感染，節點1和3恢復為感染狀態。此后網絡中沒有新的節點被感染，可以停止保護；在整個過程中，感染節點的數量始終不超過2，因此這是一種有效的干預策略。

2.基于模型檢測的干預策略問題分析

模型檢測作為一種成熟的自動驗證技術，已被廣泛用于計算機硬件、通信協議和航空電子等領域。其基本思想是通過對系統的狀態空間的窮舉搜索，來判斷采用時序邏輯所描述的待驗證的行為屬性是否成立，并且當屬性不成立時，提供反例說明。另一方面，對于網絡傳播中的干預策略問題,由于其本質上需要考慮所有可能的干預組合來判斷其是否有效，這與模型檢測的思想相吻合。因此可以考慮采用模型檢測方法來解決干預策略問題。基本思路是：采用狀態遷移系統來描述由于傳播造成的網絡節點的狀態變化，同時將干預策略的控制目標用時序邏輯描述，然后采用模型檢測方法判斷并找出有效的干預策略。由于模型檢測已經在實際中獲得廣泛應用，因此我們期望可以借助成功的模型檢測技術來解決網絡傳播干預策略問題。

2.1模型檢測工具實際中開發了很多模型檢測器，NuSMV和SPIN就是其中應用最為廣泛的兩種。它們代表了模型檢測的兩種不同理念，即符號化計算和顯式的狀態搜索。

2.1.1NuSMVNuSMV是一個針對有限狀態系統的符號化驗證工具,其基本思想是用二叉決策圖（BDD）表示布爾公式，進而用布爾邏輯公式表示遷移關系和狀態集合，能夠降低模型檢測所使用的存儲空間，解決狀態空間爆炸問題。NuSMV能夠驗證多種時序邏輯公式表達的性質，如CTL和LTL等，在電路設計和安全協議的驗證方面得到廣泛應用。

2.1.2SPINSPIN采用自動機表示模型，主要針對由LTL時序公式表達的屬性。它采用了on-the-fly技術，不需要構建一個完整的狀態空間，而是根據屬性動態展開搜索路徑的狀態。SPIN采用了多重優化技術，比如偏序規約以及狀態壓縮等。這些優化使SP其具有極高的檢測效率和較低的內存需求。它以進程作為建模的基本單位，模型中的多個進程之間可以交錯并發，更加適合對并發系統的驗證。

2.2干預策略問題分析采用圖對網絡傳播進行建模是一種直觀有效的方法。圖中的節點對應于網絡中的實體。圖中的邊對應網絡中的連接關系。圖中每個節點添加一個狀態，即感染狀態（infected），或者易感狀態（open）或者保護狀態（protected）。這樣通過圖就可以表示出對應網絡的整體狀態。根據傳遞函數f和局部更新函數g，不同時刻圖中節點對應的狀態會發生變化。雖然圖的拓撲結構未改變，但由于節點狀態的變化，圖的整體狀態也發生了變化。為了避免和節點的狀態混淆，在本文我們用“形態”表示圖的整體狀態。圖隨著時間的形態變化構成了網絡傳播的形態遷移系統。第1節中所提出的四類問題可以通過分析網絡傳播所對應的形態遷移系統，將干預策略目標采用對應的網絡形態來刻畫，通過檢測所期望的形態是否可以到達來判斷是否存在有效干預策略。為了驗證是否存在從某個初始形態出發能夠到達期望的形態，需要考慮所有可能的初始形態。為了利用模型檢測方法來解決這個問題，最重要的是將干預策略作用下的網絡傳播的形態遷移系統轉化為模型檢測所需要的狀態遷移系統。其基本方法是將傳播模型的初始形態定義為模型檢測中狀態遷移系統的狀態，并且進一步將傳播模型形態間的遷移通過狀態遷移表示出來;這樣就可以模擬從所有初始形態開始的形態遷移變化；然后采用時序邏輯表示出目標，從而可利用模型檢測進行分析驗證。

2.2.1網絡干預問題的形態遷移模型網絡干預問題的模型可以用Kripke結構表示。定義1：設錯誤！不能通過編輯域代碼創建對象。是一個原子命題集合。AP上的Kripke結構是一個四元組0M=(S,S,T,L)，其中：與靜態問題不同，動態保護問題中由于對節點的選取和保護與傳播過程交替進行，所以相應的Kripke結構更復雜。狀態集合0S對應于初始網絡形態，即初始感染節點的集合，所以。整個建模過程集中于遷移關系上，它不是單純與傳遞函數f和局部更新函數g有關，而是分為選取保護節點和網絡傳播兩個過程，即將選取保護節點作為遷移關系的一部分來定義。選取保護節點，即選擇不多于固定數量（比如d個）的節點進行保護

2.2.2干預策略問題的LTL描述建立了上述模型之后，需要給出干預策略問題所對應的行為屬性描述。我們用LTL屬性表示相應的四類干預策略問題。LTL是一種線性時態邏輯，用于描述與模型中所有可能的路徑集合所對應的行為屬性。LTL公式由表示時序的連接詞組成，例如F，U，G等。其中F連接詞表示“未來某個狀態”，G連接詞表示“所有未來狀態”。另外LTL還會出現一些組合連接詞，例如GF組合表示”在每一個路徑上，某個狀態能夠無限多次出現“，而FG則表示”一個特定過程最終會被永久保持“。接下來探討如何使用時序公式表示本文的四類問題。我們首先介紹文獻對于靜態保護問題的分析,然后介紹我們所提出的對于動態保護問題的分析。為了便于描述，我們用total表示當前感染節點的總數量，maxaffectedNum表示最大允許感染的節點數量。在不可恢復的靜態保護問題中，由于節點被感染后不能恢復，所以total是單調非遞減的。為了能夠找到一個使感染節點數量控制在maxaffectedNum之內的干預策略,使用LTL公式φ:F(total>maxaffectedNum);如果系統滿足φ，則對于系統中的所有路徑，最終都將達到一個使得total>maxaffectedNum成立的狀態,即對于給定的初始條件，不存在有效的干預策略。反之，則意味著存在某條滿足初始條件的路徑，并且total≤maxaffectedNum在該路徑上一直滿足，即路徑上的所有狀態都滿足total≤maxaffectedNum；在這種情況下，模型檢測器將返回相應的初始狀態)(),...,(ins=〈σvσv〉，從中可得到對應的干預策略。另一方面，在可恢復的靜態保護問題中，由于節點被感染后又會恢復到易感狀態，所以total可能不是單調非遞增的。為了達到將感染節點數量控制在maxaffectedNum之內的目的，策略制定者需要設法使感染節點的數量最終達到一種“平穩態”，即經過一段時間后，感染節點的數量總是能夠控制在maxaffectedNum之內。為此，可采用LTL公式φ'''':GF(total>maxaffectedNum)來描述。如果系統滿足φ'''',也就是說從所有初始路徑出發，total>maxaffectedNum將反復出現。反之，則表示存在某條路徑滿足FG(total≤maxaffectedNum)，即存在某條路徑，從某個時刻開始滿足“平穩態”且一直滿足total≤maxaffectedNum;相應地，從反例的初始狀態可以推出對應的有效干預策略。動態保護問題屬性描述更為復雜，這主要是因為模型中需要添加是否繼續保護易感節點的判斷。當傳播過程中感染節點的數量不再增加時，也就是說不會有新的節點被感染，此時停止保護節點，感染節點數量達到最大值，只需判斷total是否大于maxaffectedNum即可。為此，我們定義一個變量newNodeInfected作為停止保護的標識，初始為TRUE，當它變為FALSE時，停止保護節點。因此，問題的時序屬性描述為ψ:G((newNodeInfected=FALSE)→(total>maxaffectedNum))。若上述公式ψ成立，則從系統的所有路徑出發，到達停止保護狀態時，total>maxaffectedNum成立，亦即不存在有效的干預策略。反之，如果公式ψ不成立，則表示存在某條路徑，到達停止時刻時，total≤maxaffectedNum并將一直持續下去，即對于某條路徑，從停止保護時刻開始，之后所有的狀態均滿足total≤maxaffectedNum，從反例的狀態數組能夠分析出每次采取的干預策略。

對于可恢復的動態問題，由于感染的節點經過一段時間可以恢復到易感狀態，即相應的局部更新函數g不是單調函數，所以total也不一定是單調非遞減的，其值可能會時高時低，這取決于感染和恢復的速率。所以停止保護時，感染節點數量不一定對應于最大值，因此按照上述ψ中以此時的total來衡量是否大于maxaffectedNum是不恰當的，這時需要衡量模型未來時刻屬性的時序連接詞。與靜態恢復的情況類似，我們也希望達到相應的“平穩態”，因此可以采用時序邏輯公式ψ'''':G((newNodeInfected=FALSE)→GF(total>maxaffectedNum))。如果上述公式ψ''''成立，即表示在停止保護后total>maxaffectedNum不斷反復出現。反之，則表示存在某條路徑，停止保護后的某個時刻開始，之后能夠達到“平穩態”，即total≤maxaffectedNum一直持續下去，從反例中可以逐步推出對應的干預策略，即找出變為保護狀態的節點。

3.問題分析建模

在這一節我們分別針對上述四類問題，給出采用NuSMV和SPIN尋找有效的干預策略的分析模型。為了便于說明，我們將傳播模型中f函數的參數k設為1，可恢復情況下的g函數中r參數設為2。為了便于描述，下文用protectedNum表示需要保護的節點數量，maxaffectedNum表示系統允許的最大感染節點的數量，N表示節點的總數量，變量total表示任意時間被感染節點的總數量,數組s[N]表示網絡中所有個體的狀態。

3.1不可恢復的靜態保護問題NuSMV：使用NuSMV解決此類問題時,首先需要考慮的是將節點的狀態通過映射反映到采用NuSMV語言所描述的驗證模型中。這可以通過采用枚舉方式進行定義,比如將節點狀態映射到整數上，感染狀態對應于整數1，保護狀態對應于-1，易感狀態對應于0。NuSMV程序主要分為兩部分：初始化部分和遷移變化部分。初始化部分主要完成系統的初始環境賦值。遷移變化過程則是表示所有變量的狀態遷移及其變量間的相互關系。我們的初始化部分主要完成對感染節點的初始表示和保護節點的選擇。根據映射，將節點的初始狀態賦對應的值即可。然后重點是對傳播過程中節點的遷移變化進行描述。節點的狀態變化由f函數以及對應的鄰接點決定。對應的驗證模型則需要用狀態變量的變化，即用next語句表示出節點狀態的變化過程。根據我們的模型，對應于每個狀態為0的節點v，如果存在狀態為1的鄰接點，則它的狀態由0變為1，其它情況下它的狀態保持不變。SPIN：使用SPIN解決此類問題的重點是選取保護節點。選取節點進行保護可以利用一個do循環實現，每次選取一個節點進行保護；當被保護的節點數目達到protectedNum時即終止循環。這可以采用SPIN中條件結構的不確定性(non-deterministic)來實現。我們可以采用非負整數，比如2表示保護狀態。對應的程序如下所示，其中SelectNum表示當前選擇的保護節點數量。

3.2可恢復的靜態保護問題NuSMV：此類問題的NuSMV模型的建模思路與上述不可恢復問題的NuSMV模型相同。但根據局部更新函數g，感染狀態可細分為infected1，infected2，..，infectedr-1，并且在狀態infectedr-1后恢復為open狀態。在本文的實驗中，我們將r取3，并在模型中分別采用1和2表示infected1和infected2。這樣感染后的節點的下一狀態會有1-2,2->0的變遷，分別表示SPIN：此類問題建模思路類似不可恢復情形的SPIN建模，所以不再介紹。

3.3不可恢復的動態保護問題NuSMV：動態問題屬于動態規劃問題，因此驗證模型較兩類靜態保護問題復雜，并且由于NuSMV語言的特性給建立模型帶來了困擾。對于動態保護問題，采用NuSMV建立模型有如下難點：(i)如何表示可供選擇的易感節點的集合(ii)判斷何時停止選取節點進行保護(iii)如何表示選取保護節點與網絡傳播兩個過程的交替進行由于不斷有節點被感染和被選擇保護，所以易感節點的集合是動態變化的。如何表示易感節點的集合是NuSMV程序的第一個難點。為此，我們采用如下的策略：如果節點狀態為易感狀態，則返回節點標號，否則返回空集。由于NuSMV語言本身沒有設置空集概念，所以另外設值（比如-1）代替。接著使用內置union函數，將易感節點標號連接成一個集合。這樣就得到了供選擇的易感節點的集合，并且它是動態變化的。對于靜態問題，由于保護節點只是在初始時刻實施，故僅在初始化部分即可完成相應的干預策略表示。動態問題的選取節點過程則是不斷重復的，所以只能在遷移變化過程中表示。另一方面，由于NuSMV沒有隨機集合的類型，故一次選擇保護節點過程中同時選擇多個節點比較困難，所以我們分多步進行，即每步選擇一個節點進行保護，用Turnprotected表示這樣的步數。為了表示每步選取的易感節點的編號，模型定義了selector變量。selector可以是供選擇的易感節點標號集合中的一個隨機數。如果網絡中沒有新的節點被感染，這時再投入保護資源顯然是沒有意義的。為了避免保護資源的浪費，需要對停止保護的時刻進行判定。為此模型中設置一個結束保護的標識變量newNodeInfected。它初始為TRUE，只有當沒有易感節點候選或者在傳播過程沒有新的節點被感染，newNodeInfected才變為FALSE。當此變量發生變化時，我們就停止對節點的保護。next(newNodeInfected):=case(total=Turnprotected*turn&(next(affectedNum)-affectedNum=0))|(total+affectedNum=N):FALSE;TRUE:newNodeInfected;esac;動態問題的狀態遷移變化分為兩部分：選取保護節點和傳播變化過程，并且這兩個過程交替進行，我們用turn變量來表示選取節點過程執行的次數。選擇節點過程中只有當selector的值等于節點標號時，當前節點才能被變更為保護狀態。當選取節點過程中選擇的節點數量達到Turnprotected*turn或者無易感節點可被保護時，執行傳播過程。假設傳播網絡中節點0只與節點1,3相鄰，下面的程序是以節點0為例的遷移變化過程。SPIN：動態問題與靜態問題不同之處是添加了不斷重復選取節點和傳播的過程，直到不再進行保護。我們為此添加變量PreAffectednodeNum用來表示前一時刻感染節點的總數量。如果程序前后兩個時刻感染節點的總數量未發生變化即PreAffectednodeNum==AffectednodeNum，則終止。

3.4可恢復的動態保護問題NuSMV：此類問題的NuSMV模型類似不可恢復的動態保護問題的NuSMV模型，只是在一些地方有修改，比如不能繼續用感染節點數量不增加作為停止保護的條件。這是動態保護問題與靜態保護問題的最大不同點，也是設計模型的最大難點。感染節點數量不增加并不表示沒有新的節點被感染。當感染和恢復同時存在且兩者的速率相同，就會造成total不變化，但這并不意味著感染不會擴散到新節點以及之后不會造成大范圍的擴散。對此，我們的思路是比較前后兩個時刻曾經感染過的節點數量。若不相等，繼續保護節點；否則，停止保護。SPIN：結合此類問題的NuSMV建模思路即可完成對應的建模。

4.實驗結果與分析

我們選用隨機和NW小世界網絡兩種拓撲結構的網絡進行實驗。由于問題的復雜性，選用的隨機網絡規定每個節點的度不大于5。動態保護問題由于干預模型足夠復雜，限定隨機網絡中每個節點的度不大于4。小世界網絡是一類特殊的復雜網絡結構，在這種網絡中大部份的節點彼此并不相連，但絕大部份節點之間經過少數幾步就可到達。在社會關系網絡、互聯網絡、生物工程等眾多領域，小世界網絡得到了廣泛的應用。NW小世界網絡是一種改進了的小世界網絡模型，它避免了產生孤立點的可能。實驗的NW小世界網絡選取K=1，P=0.1表示構造環狀規則網絡時每個節點與它最鄰近的K個節點各連出1條邊接。P表示以概率P在隨機選取的一對節點之間加上一條邊。我們按一定規律（如節點個數增加）產生一系列系列數據并分別進行實驗。這樣就能很大程度上反映隨著節點數增加，模型檢測器所消耗的最大內存和CPU時間的一般性規律。為了提高實驗的準確性，本文對所總結的每一類問題都產生四組數據并分別實驗。鑒于篇幅原因，我們僅列出部分實驗數據。此外實驗采用2.5.4版本的NuSMV和6.2.3版本的SPIN，在Inteli52.5GHz處理器以及32位ubuntu平臺進行。

4.1隨機網絡實驗結果不可恢復的靜態保護問題：圖2為靜態不可恢復問題的實驗數據對應的趨勢圖。圖中間斷點表示NuSMV超時或者SPIN內存超出。實驗中設置系統允許的最長運行時間為2小時及最大可用內存為3G。另外圖表中出現的運行時間均為CPU時間。從實驗結果我們得到了如下的基本結論：對于不可恢復的靜態保護問題，SPIN需要的運行時間明顯小于NuSMV，使用的最大內存大于NuSMV。另外在最壞情況下，即對于給定問題不存在有效的干預策略時，SPIN需要的最大內存可能出現超出范圍的情況。比如圖2在節點數為45時，SPIN的內存可達到3G以上，無法完全搜索。對于這種情況可通過狀態壓縮技術進行處理，這時的最大內存略小于NuSMV，但運行時間則超過了NuSMV。可恢復的靜態保護問題：由于兩類靜態問題的實驗結果大致相同，所以此類問題的實驗數據及結論不再重復。不可恢復的動態保護問題：不可恢復的動態問題的實驗結果對應于圖3。存在有效的干預策略情況下，SPIN較NuSMV運行時間少，需要的最大內存較多，但運行時間和需要的最大內存波動較小；NuSMV隨著節點的增大，在運行時間和需要的最大內存上都存在較大波動，雖然有時隨著節點數的增加需要的最大內存反而減少，但是運行時間可能在最某點急劇增大。最壞情況下，SPIN內存消耗巨大，例如圖3中的節點數為20時，SPIN需要的最大內存急劇增加。可恢復的動態保護問題：表1是可恢復的動態保護問題的數據。表中“—”表示NuSMV超時或者SPIN內存超出。它的變化趨勢基本和靜態問題相同。但實驗中NuSMV出現了較多的超時現象，例如表1中NuSMV在節點數為13,14,15時均超時。

4.2小世界網絡實驗結果小世界網絡的分析問題比隨機網絡的情況更為復雜；即使是隨機連接概率較小（比如0.1）的小世界也可能具有復雜的網絡結構并且包含許多連接度較大的節點。表2是小世界網絡的靜態不可恢復問題的實驗結果。小世界問題中的運行時間和內存使用趨勢基本與隨機網絡的情況一致。但NuSMV在節點個數大于35之后，運行超時。SPIN在節點個數35之后，內存超出了范圍。小世界的其他問題雖然運行時間或內存更大，但結論和隨機網絡基本相同，所以不再重復。

4.3實驗結果分析產生上述現象的原因與兩種模型檢測器的原理有關。一方面，NuSMV采用高效的BDD結構表示狀態及遷移關系，可以極大地減少內存的使用量；另一方面，SPIN采用動態搜索的方式，只需要構造部分路徑就可以開始搜索，只有當前的路徑沒有找到反例，才需構造新的路徑，而一旦找到反例就停止搜索，這樣很大可能不需要構造整個狀態空間。據實驗觀察，NuSMV構造整個狀態空間的BDD圖所花的時間占運行時間的50%以上。為了解決時間超時或者內存超出問題，最根本的方法是采用抽象方法對網絡進行化簡。具體地，可以根據網絡的特征，將一些節點進行合并，這樣就能在一定程度上降低網絡的規模，從而提高模型檢測的效率。

5.相關工作

網絡傳播問題一直是數學、物理和計算機領域共同關注的焦點。眾多學者對控制網絡傳播做了大量的研究，其目標都是通過對部分個體進行保護而有效地控制傳播。部分工作研究在感染爆發之前如何采取防護措施，比如隨機免疫,目標免疫等。隨機免疫是完全隨機地選取網絡中的一部分節點進行免疫。很容易看出，它的效率比較低下，代價較大。目標免疫是根據網絡特性，選取少量度值較大的點進行免疫。網絡結構已知的情況下，目標免疫的效果遠遠好于隨機免疫。文獻論證了目標免疫措施能夠有效地控制有害傳播。另外，大量研究工作關注的是在感染已存在情況下所采取的干預策略。上文提到的消防員問題及其變種是這樣一類問題。很多文獻針對的是特定結構網絡的消防員問題,比如網格結構的消防員問題和樹結構的消防員問題。文獻考慮的是消防員問題的較一般情形，即每個時刻投入的消防員數量大于1。與上述眾多研究不同，本文考慮的是通過模型檢測方法找出一種有效的干預策略。我們研究的是更一般的情形，不僅網絡結構更為復雜，而且考慮了著火點和消防員數量多個的情況。不僅如此，本文還同時考慮了更為復雜的感染節點可恢復情形。狀態爆炸是限制模型檢測在實際應用中發展的一個重要問題。上述的實驗中出現的超時或者超出內存都是狀態爆炸的表現。針對大規模傳播模型，文獻提出了的兩種解決狀態爆炸的機制。第一種減少機制旨在減少不必要的狀態變化。比如感染節點之間的相互影響是不可以忽略的，可以刪除這部分狀態遷移。第二種機制針對的是有向傳播的網絡。根據距離將圖中的易感節點進行有效的等價類劃分。這樣一定程度減少了網絡中節點的個數，降低了模型的復雜度。

6.總結

通過保護個體進而破壞網絡結構的連通性是控制網絡傳播的一種的干預策略。本文在已有的靜態保護問題工作的基礎上，針對感染節點不可恢復與可恢復兩種情形總結了四類干預策略問題，并且重點分析了多次保護節點的動態保護問題。給出了這四類問題對應的形式化模型及相關的時序邏輯描述方法，通過模型檢測方法找出有效的干預策略。最后，使用NuSMV和SPIN兩種模型檢測工具對四類問題建模和驗證。實驗采用了隨機和小世界兩種網絡，依據實驗結果分析了NuSMV和SPIN兩種模型檢測器在具體問題中的優缺點。本文考慮了一種受時間和鄰接點影響的簡單的網絡傳播模型。但從實驗結果可以看出，隨著問題規模的增加，模型檢測所花的時間或內存空間較大。實驗中當節點的度或節點數增加到一定程度時，極易造成狀態的爆炸式增長，最終由于時間或者內存的限制，模型檢測器無法正常解決問題。因此，若能根據傳播網絡的結構特征，將模型檢測的對稱化簡和組合化簡思想應用到文中提到的問題上，并結合文獻中提出的兩種機制，有可能實現具有針對性的解決狀態爆炸的方法，在提高模型檢測的效率的同時也能使模型檢測應用到大規模的傳播網絡問題中。現實世界中的傳播模型摻雜著概率因素。文獻中建立了離散的郵件病毒傳播模型，其中病毒在相鄰節點之間傳播和節點被感染是有一定概率的。文獻應用概率模型檢測方法對生化網絡進行了分析。類似地，將概率模型檢測方法應用到網絡干預問題中，將是一個十分有意義的問題。

作者：余鵬魏歐 韓蘭勝牛耘單位：蘇州大學鳳凰傳媒學院