王軼 駱犀羚

1 引言

對由網(wǎng)絡(luò)結(jié)構(gòu)導(dǎo)致的社會網(wǎng)絡(luò)隨時間演變的特性進行邏輯分析是敵友邏輯（Logic of Allies and Enemies）（[10]）的主要目的。其理論基礎(chǔ)來自于社會心理學(xué)家提出的結(jié)構(gòu)平衡理論（[8,9]），而后又被推廣為使用圖論來進行刻畫（[1,5,6]）。在該理論中，社會網(wǎng)絡(luò)被處理為加標(biāo)圖：每個節(jié)點代表一個主體，每條邊代表一個連帶（tie）且標(biāo)以積極或消極符號。積極符號通常用于標(biāo)識朋友或盟友關(guān)系，而消極符號則用于敵人或?qū)κ株P(guān)系。

如果網(wǎng)絡(luò)結(jié)構(gòu)滿足特定的條件，那么這個網(wǎng)絡(luò)是平衡的。舉例來說，三個互為朋友的主體所表示的關(guān)系結(jié)構(gòu)是平衡的，而三個互相敵對的主體所代表的關(guān)系結(jié)構(gòu)被認為是不平衡的。經(jīng)典文獻（[1,5–7]）中通過圖形中的回路來定義網(wǎng)絡(luò)的結(jié)構(gòu)平衡性。如果一條回路中有偶數(shù)條消極邊，則該回路是積極的；反之如果有奇數(shù)條邊，則整條回路是消極的。例如，圖1表示具有五個主體（a,b,c,d,e）和三條回路（abc、abdec和bced）的網(wǎng)絡(luò)。因為圖中每條回路都有偶數(shù)個消極邊，所以全部回路都是積極的。這種只有積極回路的網(wǎng)絡(luò)就稱為是平衡的。結(jié)構(gòu)平衡理論認為，社會網(wǎng)絡(luò)有向平衡網(wǎng)絡(luò)演變的趨勢，雖然這一過程可能需要很長時間，并且可能由于各方面因素的影響而無法真正達到平衡。

敵友邏輯引入了一個與結(jié)構(gòu)平衡秉承相似直觀但有所不同的概念，稱為穩(wěn)定性。在敵友邏輯中，如果一對主體更愿意保持彼此現(xiàn)有的關(guān)系，那么他們當(dāng)下的關(guān)系是穩(wěn)定的。如果網(wǎng)絡(luò)中每對主體間的關(guān)系都是穩(wěn)定的，那么整個網(wǎng)絡(luò)就是穩(wěn)定的。更細致地說，如果兩個主體是朋友，并且他們的共識（即共同的朋友或敵人）多于分歧（即與其一為友而與另一為敵的那些主體），則兩者的關(guān)系是穩(wěn)定的。如果兩個主體是敵人，并且分歧多于共識，該關(guān)系也是穩(wěn)定的。此外，對于非敵非友的兩個主體，如果共識與分歧數(shù)量相等，則也具有穩(wěn)定關(guān)系。其他情況則是不穩(wěn)定的。

穩(wěn)定性概念乍看起來或許與平衡性相去甚遠，但它采用的觀點實際上源自結(jié)構(gòu)平衡理論最初的想法（[8,9]）：對第三者抱有相似態(tài)度的一對個體傾向于彼此喜歡，對第三者抱有不同態(tài)度的一對個體傾向于彼此厭惡。

文中將引入敵友邏輯的公理系統(tǒng)，它在分支時間邏輯CTL（[3]）的公理系統(tǒng)之上增加一些與網(wǎng)絡(luò)相關(guān)的公理和規(guī)則。該系統(tǒng)的可靠性和完全性也將得到證明。

敵友邏輯的模型檢測、有效性以及可滿足性檢測問題都是PSPACE完全的（[10]），其具體算法已通過Python程序?qū)崿F(xiàn)，后文將具體說明其主要功能，包括如下常用函數(shù)：

?staScore()：對于給定的網(wǎng)絡(luò)，計算其穩(wěn)定性評分

?isStable()：判斷給定網(wǎng)絡(luò)是否穩(wěn)定

?succNum()：對于給定的網(wǎng)絡(luò)，計算其后繼數(shù)目

?successors()：返回存儲給定網(wǎng)絡(luò)所有后繼的列表

?isSucc()：判斷一網(wǎng)絡(luò)是否為另一網(wǎng)絡(luò)的后繼

?mc()：對于給定的網(wǎng)絡(luò)和給定的公式，判斷該網(wǎng)絡(luò)是否滿足該公式

?sat()和valid()：對于給定的公式，分別判斷該公式是否可滿足或是否有效

?satFind()：基于給定情況，找到滿足給定公式的網(wǎng)絡(luò)

文章結(jié)構(gòu)如下。第2節(jié)介紹敵友邏輯（[10]）的語法和語義。第3節(jié)引入敵友邏輯的公理化，并證明其可靠性和完全性。第4節(jié)介紹敵友邏輯模型檢測、有效性檢測和可滿足性檢測的程序?qū)崿F(xiàn)；其中第4.1和4.2節(jié)分別涵蓋語義（網(wǎng)絡(luò)相關(guān)）和語法（句法檢查）的程序?qū)崿F(xiàn)，而對模型、有效性和可滿足性檢測程序的說明則在第4.3節(jié)。文章最后一節(jié)總結(jié)并討論后續(xù)工作。程序代碼、例子和后期更新將通過如下網(wǎng)站維護：http://www.xixilogic.org/projects/lae。

2 敵友邏輯

本節(jié)簡要介紹敵友邏輯（[10]）的語法、語義及其模型檢測等問題。以自然數(shù)表示主體，ω表示所有主體的集合。當(dāng)自然數(shù)n用于表示網(wǎng)絡(luò)的個體與或者語言的參數(shù)時，它代表一個自然數(shù)的集合（即集合{0,1,...,n?1}）。這種處理方式與公理集合論中對自然數(shù)的常見定義保持一致（不妨參考[11]）。

2.1 網(wǎng)絡(luò)與穩(wěn)定性

n節(jié)點網(wǎng)絡(luò)是具有n個節(jié)點的帶三個符號的有窮無向完全圖。準確地講，一個n節(jié)點網(wǎng)絡(luò)是一個有序?qū)?n,E)，使得：

?n={0,...,n?1}是有窮的主體集；

?E:{{i,j}|i,j∈n}→{1,0,?1}是一個全函數(shù)，用于表示每對主體之間的

積極(+)、消極(?)或中立(0)連帶，并且滿足E({i,i})=0。

這里不考慮自反圈（例如i是自己的朋友或敵人）或兩個主體之間具有多重關(guān)系（例如i和j既是朋友又是敵人）等情形。在不引起混淆的情況下，通常以ij或ji表示邊{i,j}。有時也以E(ij)或E(ji)（或者E(i,j)或E(j,i)）表示E({i,j})。

在敵友邏輯中，兩個主體之間的共識或吸引力定義為使他們建立或保持朋友關(guān)系的理由數(shù)，即他們的共同朋友或敵人的總數(shù)。類似的，兩個主體間的分歧或排斥力是使他們建立或保持敵對關(guān)系理由數(shù)，即與其一為友但與另一主體為敵的主體的總數(shù)。準確說來，令N=(n,E)為一網(wǎng)絡(luò)且i,j∈n，則ij之間的共識（記為attr(ij)）和分歧（記為rep(ij)）滿足：

兩主體間關(guān)系的穩(wěn)定性取決于他們現(xiàn)有的關(guān)系和彼此間的共識與分歧。如果i和j是朋友（即E(ij)=1），且他們之間的共識不小于分歧，則他們的關(guān)系是穩(wěn)定的。類似地，如果i和j是敵人，且彼此間分歧不小于共識，則也是穩(wěn)定的。而中立關(guān)系只有當(dāng)吸引力等于排斥力時才是穩(wěn)定的。除此以外的情況都是不穩(wěn)定的。ij連帶的穩(wěn)定性評分以score(ij)表示，定義如下：

不難發(fā)現(xiàn)，如果score(ij)≥0，那么ij連帶是穩(wěn)定的。反之，則不穩(wěn)定。

如果網(wǎng)絡(luò)中所有的邊都穩(wěn)定，則稱該網(wǎng)絡(luò)穩(wěn)定。反之則不穩(wěn)定。一個網(wǎng)絡(luò)的穩(wěn)定性評分是其中所有邊的穩(wěn)定性評分之和。

稱網(wǎng)絡(luò)N2=(n,E1)是網(wǎng)絡(luò)N1=(n,E2)的后繼（記為N1?N2），如果滿足如下條件之一：

?當(dāng)N1穩(wěn)定時：N1=N2,

?當(dāng)N1不穩(wěn)定時：N1與N2僅在一條邊ij的符號上有差別，同時滿足：要么在N1中有attr(ij)>rep(ij)且E2(ij)=1，要么在N1中有rep(ij)>attr(ij)且E2(ij)=?1。

網(wǎng)絡(luò)集上的后繼關(guān)系形成了一個樹形結(jié)構(gòu)，其每條分支代表網(wǎng)絡(luò)隨時間演進的過程，僅有的循環(huán)出現(xiàn)于穩(wěn)定網(wǎng)絡(luò)到自身的回路。關(guān)于上述定義和結(jié)論的更多解釋詳見（[10]）。這里值得強調(diào)的是，網(wǎng)絡(luò)的演進過程中穩(wěn)定性評分并不一定遞增。雖然在多數(shù)情況下，后繼網(wǎng)絡(luò)的穩(wěn)定性評分確實高于其前驅(qū)，并且這確實反映了網(wǎng)絡(luò)結(jié)構(gòu)趨于平衡的性質(zhì)，但并不能排除穩(wěn)定性評分走低的臨時情況。

2.2 語言和語義

這里引入有窮版本的LAE，即可用主體集為某個自然數(shù)n={0,1,...,n?1}，記為LAEn。參數(shù)n可以是任意大于等于3的自然數(shù)（當(dāng)n<3時網(wǎng)絡(luò)平衡概念失去意義，因此不予考慮）。LAEn的語言Ln的語法定義如下：

其中i∈n。原子命題P(i,j)、N(i,j)和O(i,j)將分別用于表示ij邊是積極、消極和中立的，而stb和bal將分別表示網(wǎng)絡(luò)是穩(wěn)定和平衡的。符號T、～、/、/、->和是命題聯(lián)結(jié)詞（正文中使用中綴形式∧、∨、→和?分別表示后四個符號以方便閱讀）。其他算子來自CTL（[2,3]）。

Ln通過大小為n的網(wǎng)絡(luò)的集合加以解釋。任意N=(n,E)是否滿足（記作|=）某個Ln公式可歸納定義如下（其中φ,ψ∈Ln且i,j∈n）：

語句“ij邊穩(wěn)定”（記為stb(i,j)）可以在Ln中表達如下：

因此不必作為原子語句引入。

由上述語義可以得到一系列邏輯LAEn(n∈N且n≥3)，通常以LAE表示任意這樣的邏輯。如下定義引自（[10]）：

定理1(LAE的計算復(fù)雜性).LAE的模型檢測與有效性檢測問題都是PSPACE完全的。

3 公理系統(tǒng)

由定理1，敵友邏輯LAE的有效性檢測問題是可判定的，因此是可公理化的：至少可以窮舉所有有效式。但這并不意味著可以得到一個契合語法證明直觀的公理系統(tǒng)。本節(jié)給出LAE的公理系統(tǒng)，并證明其可靠性和完全性。

下文將給出邏輯LAEn的公理系統(tǒng)LAEn，其中引入了描述這一概念。描述（將以δ表示）是形如∧i,j∈npi,j的公式，其中pi,j是原子命題P(i,j)、N(i,j)或O(i,j)。描述將用于刻畫網(wǎng)絡(luò)，而最好的方式是使同一網(wǎng)絡(luò)被唯一的描述所刻畫。為實現(xiàn)這一目的，需要增加一些限制條件。

首先約定描述中的邊按照特定順序排列，例如規(guī)定p1,2永遠出現(xiàn)在p1,3的左邊，這樣可以避免出現(xiàn)對同一網(wǎng)絡(luò)的邏輯等值的不同描述。令N=(n,E)為一網(wǎng)絡(luò)，N的描述，記為δ(N)，是滿足如下要求的合取式∧i,j∈npi,j（合取項有確定的順序）：

在上述限制條件下，不難證明δ(N)是存在且唯一的。此外，并非所有的描述都是某個網(wǎng)絡(luò)的描述（例如出現(xiàn)合取支P(1,1)，或同時出現(xiàn)P(1,2)和N(2,1)等情況），但如果δ是N的描述，即δ=δ(N)，則稱δ描述了N。不難證明，δ(N)描述了唯一一個網(wǎng)絡(luò)，即N。

穩(wěn)定公理（記為SF）是如下公式：

其中δ1,...,δm枚舉了所有穩(wěn)定網(wǎng)絡(luò)的描述。類似地，平衡公理（記為BF）是如下公式：

其中，δ1,...,δm枚舉了所有平衡網(wǎng)絡(luò)的描述。

令δ描述網(wǎng)絡(luò)N，則δ的明日公理（記為tf(δ)）是如下公式:

其中，δ1,...,δm是δ所描述的網(wǎng)絡(luò)的所有后繼的描述。明日公理tf(δ)可以簡寫為δ→?{δ1,...,δm}，其中的?有時稱為覆蓋模態(tài)詞（cover modality）。明日公理的數(shù)量是有窮的。

邏輯LAEn的公理系統(tǒng)LAEn如圖2所示。LAEn由CTL的公理和規(guī)則（[4]）、用于刻畫網(wǎng)絡(luò)以及網(wǎng)絡(luò)更新的公理和規(guī)則以及一些CTL時態(tài)算子的定義公理組成。{AX,AU,EU}是CTL時態(tài)算子的一個完全集，因此其他算子EX、AG、EG、AF和EF都是可定義的，這些定義公理都放在“CTL模態(tài)詞定義”欄目下。此外，CTL公理DX可由明日公理推導(dǎo)出，因此可以刪去。

不難驗證LAEn的可靠性：所有公理都有效并且所有規(guī)則都保持有效性。其具體證明不再贅述。這里主要關(guān)注LAEn的完全性。下面的結(jié)論適用于任意數(shù)量的主體（即任意n∈ω且n≥3），因此以Φ?φ表示公式φ是以公式集Φ為前提在系統(tǒng)LAEn中可推演的（?φ即表示φ是LAEn的定理）。

引理1.假設(shè)?δ→?{δ1,...,δm}，則如下結(jié)論成立：

1.如果對所有i=1,...,m都有?δi→φ，則?δ→AXφ

2.如果存在i=1,...,m使得?δi→～φ，則?δ→～AXφ

引理2.對任意網(wǎng)絡(luò)的描述δ和任意公式φ，要么?δ→φ，要么?δ→～φ。

證明.網(wǎng)絡(luò)的描述中的兩個不同合取支不能同時為集合{P(i,j),N(i,j),O(i,j)}中的元素。這由公理(PN)和(Neut)保證。此外，P(i,j)和P(j,i)（對于N和O也類似）要么同為網(wǎng)絡(luò)描述的兩個合取支，要么都不是，這由公理(Symm)和(Neut)保證。因此，網(wǎng)絡(luò)描述的一致性可以通過命題邏輯和這些公理得到。因此?δ→φ和?δ→～φ不能同時成立。

下面通過對φ做結(jié)構(gòu)歸納來證明?δ→φ與?δ→～φ中至少有一個成立。

?φ是原子公式P(i,j)。如果P(i,j)是δ的一個合取支，那么?δ→P(i,j)。否則N(i,j)和O(i,j)之一是δ的合取支。因此，要么?δ→N(i,j)，要么?δ→O(i,j)。又因為?N(i,j)→ ～P(i,j)（根據(jù)PN）且?O(i,j)→ ～P(i,j)（根據(jù)Neut），故有 ? δ→ ～P(i,j)。

?φ為N(i,j)和O(i,j)的情形可作類似證明。

?φ=～ψ：若?δ→～ψ，由歸納假設(shè)知?δ→ψ，故?δ→～～ψ。

?φ=(ψ → χ)：若 ?δ→ (ψ → χ)，則?δ→ ～ψ且 ?δ→ χ。因此，?δ→(～ψ∨χ)，即?δ→(ψ →χ)。

?其他命題聯(lián)結(jié)詞情形可類似證明。

?φ為stb的情形。假設(shè)?δ→stb。在此情況下δ不可能描述穩(wěn)定網(wǎng)絡(luò)。否則根據(jù)穩(wěn)定性公理，? stb ? (δ1∨···∨δm)（其中δ1,...,δm是所有穩(wěn)定網(wǎng)絡(luò)的描述）。如果δ描述穩(wěn)定網(wǎng)絡(luò)，那么δ是某個δi（i=1,...,m）。于是? δ→ (δ1∨···∨δm)，并因此?δ→stb，與假設(shè)矛盾。所以δ描述的不是穩(wěn)定網(wǎng)絡(luò)，并且δ與所有的δi都至少有一個合取支是不同的。由此可知，?δ→～(δ1∨···∨δm)。否則存在i=1,...,m使得?δ→δi，矛盾。根據(jù)穩(wěn)定性公理，?δ→～stb。

?φ為AXψ的情形。假設(shè)?δ→AXψ。由明日公理，有?δ→?{δ1,...,δm}（其中δ1,...,δm是δ所描述網(wǎng)絡(luò)的所有后繼的描述）。在根據(jù)引理1(1)，存在i=1,...,m使得?δi→ψ。由歸納假設(shè)知?δi→～ψ。故由引理1(2)，?δ→～AXψ。

?φ為AU(ψ,χ)的情形。假設(shè)?δ→ AU(ψ,χ)。通過(AU)進行等值替換，有?δ→ (χ∨(ψ∧AXAU(ψ,χ)))。由此可知，(1)?δ→ χ且[(2)?δ→ ψ或(3)?δ→AXAU(ψ,χ)]。當(dāng)(1)和(2)同時成立時，根據(jù)歸納假設(shè)，有?δ→～χ和 ? δ→ ～ψ。由此可知 ? δ→ ～(χ∨(ψ∧AXAU(ψ,χ)))。再由 (AU)，有?δ→ ～AU(ψ,χ)。當(dāng)(1)和(3)同時成立時，由(3)和引理1(1)知，明日公理δ→ ?{δ1,...,δm}中存在δi(1 ≤ i≤ m)使得? δi→ AU(ψ,χ)。這就得到與開頭假設(shè)部分相似的情形，但是建立在δ的后繼δi之上。繼續(xù)這個過程有窮多次（明日公理有窮）直到得到?δs→AU(ψ,χ)，其中δs描述穩(wěn)定網(wǎng)絡(luò)（即?δs→stb）。由此可得 ? δs→ (χ ∨ (ψ ∧ AXAU(ψ,χ)))，同理亦可得 (1′)? δs→ χ 且 [(2′)? δs→ ψ 或 (3′)? δs→ AXAU(ψ,χ)]。對于 (1′)和 (2′)同時成立的情形，仍有?δs→～χ且?δs→～ψ，并且?δs→～AU(ψ,χ)成立。通過反復(fù)使用(AU)進行等價替換，可得? δ→ ～AU(ψ,χ)。當(dāng)(1′)和(3′)同時成立時，因為δs→ ?δs是明日公理，根據(jù)(1’)和(Tm1)，有?δs→～AU(ψ,χ)。反復(fù)使用引理1(2)并使用(AU)進行等價替換，可以得到?δ→～AU(ψ,χ)。

?φ=EU(ψ,χ)的情況與AU(ψ,χ)類似，使用公理(Tm2)替代(Tm1)即可。

根據(jù)“CTL模態(tài)詞定義”類型中的公理，包含其他時態(tài)算子的公式可歸約為不含這些算子的公式，從而結(jié)論對所有公式成立。

引理3.任給極大一致的公式集Φ，描述δ和公式φ。如果δ,φ∈Φ，則?δ→φ。證明.使用反證法，假設(shè)δ,φ∈Φ且?δ→φ。由引理2知?δ→～φ。根據(jù)Φ的極大性，有～φ∈Φ，從而Φ不一致。矛盾！

任給極大一致的Ln公式集Φ，以NΦ表示網(wǎng)絡(luò)(n,E)，其中E滿足：

可以證明NΦ存在且唯一。

引理4.令Φ為極大一致的公式集，且δ是網(wǎng)絡(luò)的描述。則如下命題等價：

1.NΦ|=δ 2.δ描述NΦ3.δ∈Φ

引理5.令Φ為極大一致的公式集，則NΦ|=Φ。

證明.假設(shè)δ描述NΦ。由引理4可得NΦ|=δ和δ∈Φ。對任意φ∈Φ，由引理3，有?δ→φ。再由LAEn的可靠性知|=δ→φ，故NΦ|=φ。因此NΦ|=Φ。

與CTL只有弱完全性不同，LAEn具有強完全性。這主要是因為在LAEn中所有的時間線都是有窮的（每個網(wǎng)絡(luò)都能在有限步到達穩(wěn)定，且穩(wěn)定網(wǎng)絡(luò)不再發(fā)生變化）。

定理2(強完全性).任給極大一致的公式集Φ和公式φ，如果Φ|=φ，則Φ?φ。

4 程序?qū)崿F(xiàn)

本節(jié)介紹基于Python的LAE模型和有效性檢測程序，主要分為網(wǎng)絡(luò)的實現(xiàn)（語義角度）、語法檢測（語形角度）和模型檢測等的實現(xiàn)（語義和語形交叉）三個部分。

4.1 網(wǎng)絡(luò)的實現(xiàn)

在程序?qū)崿F(xiàn)中，n節(jié)點網(wǎng)絡(luò)（n∈ω）是二元組(n,E)，其中E:n×n→{?1,0,1}滿足E(i,j)=E(j,i)，且對所有i,j∈n都有E(i,i)=0。該定義與第2節(jié)中的差別在于這里的每個主體對都是有序的，但因為保證了對稱性，兩個定義是共通的。

n節(jié)點網(wǎng)絡(luò)可以看成是n×n矩陣，其中每個元素(i,j)代表主體i與j之間的連帶。左下圖矩陣表示一個6節(jié)點網(wǎng)絡(luò)，對應(yīng)于右下圖所示網(wǎng)絡(luò)。

如前所述，網(wǎng)絡(luò)示意圖中的實線表示積極連帶，虛線表示消極連帶，而中性連帶則不畫線。該表示法與經(jīng)典文獻（[1]）中一致。

4.1.1 生成和表示

對于程序?qū)崿F(xiàn)而言，網(wǎng)絡(luò)其實就是前面定義的矩陣。但程序同時支持通過指定網(wǎng)絡(luò)中的積極和消極連帶來生成網(wǎng)絡(luò)。

netInit()與netGen()這兩個函數(shù)用于生成網(wǎng)絡(luò)。函數(shù)netInit(n)初始化一個所有的邊都是中性連帶的n節(jié)點網(wǎng)絡(luò)，即大小為n×n、元素全為0的矩陣。函數(shù)netGen(net,sign,*edges)可以通過為列表*edges中的邊規(guī)定符號sign來修改網(wǎng)絡(luò)net。

例如，以下幾行代碼生成上面圖形中給出的6節(jié)點網(wǎng)絡(luò)，該網(wǎng)絡(luò)命名為net1（可使用命令print(net1)進行查看）。

函數(shù)netSize()返回所輸入網(wǎng)絡(luò)的大小。如果對上面定義的網(wǎng)絡(luò)net1執(zhí)行命令netSize(net1)，則返回值為6。

4.1.2 評分計算

對于給定的網(wǎng)絡(luò)，邊(i,j)的共識、分歧和穩(wěn)定性評分分別由函數(shù)attr()、rep()和score()給出：

?attr(net,i,j)：返回網(wǎng)絡(luò)net中邊(i,j)的共識；

?rep(net,i,j)：返回網(wǎng)絡(luò)net中邊(i,j)的分歧；

?score(net,i,j)：返回網(wǎng)絡(luò)net中邊(i,j)的穩(wěn)定性評分。

如果省略參數(shù)i與j，則輸出結(jié)果為一個矩陣，其右上部每個位置的值都為對應(yīng)邊的相應(yīng)值。例如，attr(4net)（其中，4net是一個4節(jié)點網(wǎng)絡(luò)）的結(jié)果如下：

需要注意的是，對于在自循環(huán)ii，共識為包含i的全部連帶的數(shù)量，而分歧為0。這些特殊情況目前在程序中并考慮，但不會導(dǎo)致后續(xù)檢測結(jié)論出現(xiàn)錯誤。

用第4.1.1節(jié)中的例子，執(zhí)行print(attr(net1))、print(rep(net1))和print(score(net1))命令將分別得到如下矩陣：

網(wǎng)絡(luò)的穩(wěn)定性評分被定義為其所有邊穩(wěn)定性評分的總和。函數(shù)staScore()（勿與score()混淆）可用于獲得網(wǎng)絡(luò)的穩(wěn)定性評分。例如，命令staScore(net1)返回4。

4.1.3 后繼

函數(shù)isStable()用于檢測一個網(wǎng)絡(luò)是否穩(wěn)定。函數(shù)succNum()返回給定網(wǎng)絡(luò)所有不同后繼的數(shù)量。采用第4.1.1和4.1.2節(jié)中的例子，succNum(net1)返回2，即網(wǎng)絡(luò)net1有兩個后繼。

函數(shù)successors()返回給定網(wǎng)絡(luò)的所有后繼網(wǎng)絡(luò)的列表。例如，執(zhí)行命令successors(net1)將輸出如下結(jié)果（其中兩個矩陣分別表示net1的兩個后繼）：

函數(shù)isSucc()可用來檢測一個網(wǎng)絡(luò)是否是另一網(wǎng)絡(luò)的后繼。如果存在時間線N0? N1? ···? Nn使得N=N0且N′=Nn，則稱網(wǎng)絡(luò)N′是N 的n步后繼。執(zhí)行命令isSucc(net1,net2,num)，如果net2是net1的num步后繼，則返回True，否則返回False。

定義如下網(wǎng)絡(luò)：

然后使用檢測它們中的某些是否為否另外一些的后繼：

得到的結(jié)果分別為True、True、True、True、True和False。

4.2 語法檢測

函數(shù)formChk(n,string)檢驗一個字符串是否為Ln的公式，即滿足語法規(guī)則且只包含0到n?1主體的字符串。如果滿足，則返回值為True。若否，則為False。此外，這個功能也被用在裝飾器argsChk()中，該裝飾器可保證其他函數(shù)輸入的公式始終符合標(biāo)準。

例如，運行以下代碼得到的輸出

返回的值分別為True、True、False以及False。

4.3 模型檢測、有效性檢測和可滿足性檢測的實現(xiàn)

模型檢測、有效性檢測和可滿足性檢測分別以函數(shù)mc()、sat()和valid()加以實現(xiàn)。下面給出具體說明。

任給網(wǎng)絡(luò)N（由net表示）和公式φ（由formula表示），如果N|=φ，則命令mc(net,formula)返回True，否則返回False。

為方便輸入網(wǎng)絡(luò)，提供了函數(shù)desc()用以生成網(wǎng)絡(luò)的描述（描述的定義見第3節(jié)）。實際輸出的是部分的網(wǎng)絡(luò)描述（矩陣），即僅僅是矩陣對角線右上方的那些連帶。這樣做并不會丟失信息，因為對于網(wǎng)絡(luò)這樣的無向而言，對角線兩邊完全對稱。例如，print(desc(net1))輸出如下：

/(N(0,1),/(O(0,2),/(O(0,3),/(N(0,4),/(N(0,5),/(P(1,2),

/(O(1,3),/(P(1,4),/(N(1,5),/(O(2,3),/(P(2,4),/(N(2,5),

/(O(3,4),/(O(3,5),N(4,5)))))))))))))))

上面使用的是前綴表達式，改用中綴表示并去除多余括號，即如下公式：不難驗證，desc(net1)在且只在網(wǎng)絡(luò)net1中為真。

任給公式φ，命令sat(n,φ)返回True，如果φ是n可滿足的，即存在n節(jié)點網(wǎng)絡(luò)N使得N|=φ；否則返回False。命令valid(n,φ)返回True，如果φ是n有效的，即所有n節(jié)點網(wǎng)絡(luò)N都滿足N|=φ；否則返回False。

目前還未對可滿足性和有效性檢測工具進行算法優(yōu)化，只是通過測試所有網(wǎng)絡(luò)將兩類檢測問題歸約為模型檢測問題，因此大型網(wǎng)絡(luò)的結(jié)果輸出可能會比較慢。

函數(shù) satFind(n,formula,mode='normal')在默認情況（'normal'模式）下，會查找滿足給定Ln公式的所有網(wǎng)絡(luò)（可能非常耗時）。如果找不到，則返回False。如果設(shè)置mode='min'，則輸出滿足給定公式的最小網(wǎng)絡(luò)（如果不可滿足則返回False）。例如，print(satFind(5,'AXP(1,2)',True))的輸出如右圖所示。

5 結(jié)語

本文給出了敵友邏輯（[10]）的公理系統(tǒng)和程序?qū)崿F(xiàn)。公理系統(tǒng)包含穩(wěn)定公理（SF）和明日公理（TF）以及依賴網(wǎng)絡(luò)描述的規(guī)則Tm1和Tm2。這些公理和規(guī)則是純語形的，但很大程度上復(fù)制了網(wǎng)絡(luò)更新的形式語義定義。我們不確定是否可以在不使用網(wǎng)絡(luò)描述的前提下對敵友邏輯進行公理化，但我們給出的公理系統(tǒng)絕非毫無意義。它是對CTL公理系統(tǒng)的保守擴充，至少表明CTL的公理和規(guī)則對于本文引入的基于網(wǎng)絡(luò)的形式語義仍然是有效的。

目前的程序?qū)崿F(xiàn)嚴格地依照語義定義來進行。這也就意味著程序可以進行優(yōu)化。例如，如果遇到形如AU(φ,ψ)∨～AU(φ,ψ)這種可以通過命題邏輯簡單判定的公式，程序中仍然需要（兩次）檢測AU(φ,ψ)是否為真。又如，可滿足性檢測的程序算法是從最小的網(wǎng)絡(luò)逐一開始檢測直到找到滿足的網(wǎng)絡(luò)，但通常來說，還有更好的策略去找到滿足條件的網(wǎng)絡(luò)。優(yōu)化模型檢測算法的方法有很多，這是從事定理證明等相關(guān)領(lǐng)域研究者經(jīng)常面臨的任務(wù)。本文的重點是給出行之有效的程序?qū)崿F(xiàn)，而進一步的優(yōu)化則是未來的工作方向。

網(wǎng)絡(luò)中邊的符號目前僅允許{?1,0,1}中的，對此進行推廣是一件自然而然的事情。如果將符號的數(shù)字理解為概率，那么恰當(dāng)?shù)姆柗秶赡苁浅Ｓ糜诒硎靖怕实膶崝?shù)區(qū)間[?1,1]。在這種情況下，一對主體的概率或許可以視為其共識或分歧符號的乘積。如果將符號理解為關(guān)系的強度，則使用自然數(shù)、有理數(shù)或?qū)崝?shù)都是可行的。關(guān)系的強度可以是共識或分歧中的最小值，或是它們的和。在結(jié)構(gòu)平衡理論中增加關(guān)系強度的刻畫早在（[12]）中就已經(jīng)出現(xiàn)，這些將留作未來的任務(wù)。

使用圖形表示網(wǎng)絡(luò)可以使模型檢測工具更加實用，我們打算在未來加以實現(xiàn)。除此以外，敵友邏輯適用于不同領(lǐng)域的版本也具有研究價值，我們將探討允許網(wǎng)絡(luò)更新算子、與博弈論結(jié)合等研究思路。