摘要： 為了對包含多值信息的開放系統(tǒng)進行形式化驗證，在多值邏輯的基礎(chǔ)上提出了多值交互時序邏輯并研究了該邏輯的模型檢驗問題。首先，引入多值并發(fā)博弈結(jié)構(gòu)作為此類開放系統(tǒng)的模型，該模型的最大特點是可以建模帶有多值信息的開放系統(tǒng)。其次，給出基于此模型的多值交互時序邏輯的語法和語義，該邏輯可以描述帶有多值信息的待驗證屬性。最后，基于不動點理論給出多值交互時序邏輯的模型檢驗算法，并對算法的時間復雜度進行了分析，結(jié)果表明，可以在多項式時間內(nèi)完成對多值交互時序邏輯的模型檢驗。

關(guān)鍵詞： 模型檢驗； 多值邏輯； 交互時序邏輯； 并發(fā)博弈結(jié)構(gòu)

中圖分類號： TP301

文獻標志碼： A

文章編號： 1671-6841（2025）02-0078-07

DOI： 10.13705/j.issn.1671-6841.2023192

Model Checking Research of Multi-valued Alternating-time Temporal Logic

LING Canhong1， CHANG Liang1， ZHOU Jie²， PAN Haiyu1

（1.Guangxi Key Laboratory of Trusted Software， Guilin University of Electronic Technology， Guilin 541004， China;

2.College of Mathematics and Science， Shanghai Normal University， Shanghai 200234， China）

Abstract： In order to formally verify open systems containing multi-valued information， a multi-valued alternating-time temporal logic was proposed based on multi-valued logic， and the model checking problem of this logic was explored. Firstly， a multi-valued concurrent game structure was introduced as a model for such open systems. The key feature of the model was that it could model open systems with multi-valued information. Secondly， the syntax and semantics of multi-valued alternating-time temporal logic based on this model were provided， which could describe properties with multi-valued information to be verified. Finally， a model checking algorithm for multi-valued alternating-time temporal logic was proposed based on fixed-point theory， and the time complexity of the algorithm was analyzed. The analysis results indicated that model checking for multi-valued alternating-time temporal logic could be completed in polynomial time.

Key words： model checking; multi-valued logic; alternating-time temporal logic; concurrent game structure

0 引言

模型檢驗^［1-4］作為一種自動化驗證技術(shù)，已廣泛應用于軟硬件系統(tǒng)行為的驗證之中^［5-6］。但隨著軟硬件系統(tǒng)復雜程度的提高，許多系統(tǒng)呈現(xiàn)出多種不確定性和不一致性，這使得經(jīng)典的模型檢驗技術(shù)不再適用。為了解決這一問題，研究者提出了多值模型檢驗技術(shù)^［7］。相比經(jīng)典模型檢驗技術(shù)，多值模型檢驗技術(shù)具有更貼近實際系統(tǒng)、建模方式更靈活以及驗證方法更高效等優(yōu)點^［8-9］。

目前，多值模型檢驗技術(shù)在理論和應用研究方面都取得了顯著的進展，如電車能耗決策^［10］、模擬電路^［11］等。2016年，Pan等^［12］研究了取值為一般有限格的多值計算樹邏輯（multi-valued computation tree logic，MVCTL）的模型檢驗問題。同年，Meller等^［13］基于抽象和細化的思想，提出一種用于多值模型檢驗的組合方法。2019年，Li等^［14］為解決多值邏輯χCTL不能表達定量性質(zhì)的問題，將可能性理論引入χCTL的模型檢驗中，完成了對 χCTL的定量分析。2021年，Li等^［15］基于廣義可能性度量理論，研究了廣義可能性模糊線性時序邏輯（generalized possibilistic fuzzy linear temporal logic，GPoFTL）

的模型檢驗問題。近年來，多值模型檢驗的重要性急速攀升，但這些技術(shù)不適用于帶有不確定性和不一致信息的開放系統(tǒng)^［16-17］的驗證。

因此，在解決這一問題之前，先介紹一種應用于傳統(tǒng)開放系統(tǒng)的規(guī)約語言，該規(guī)約語言的出現(xiàn)是因為

封閉系統(tǒng)的行為僅受內(nèi)部狀態(tài)的影響，而開放系統(tǒng)在其行為中還會受到外部環(huán)境交互的影響。這導致以往的模型檢驗技術(shù)不能直接應用于開放系統(tǒng)中。為此，Alur等^［18］引入并發(fā)博弈結(jié)構(gòu)（concurrent game structure，CGS）作為開放系統(tǒng)的行為模型，并提出交互時序邏輯（alternating-time temporal logic，ATL）用以描述開放系統(tǒng)的待驗證屬性。目前，ATL已在多個領(lǐng)域有了成功的應用，例如區(qū)塊鏈智能合約^［19］、網(wǎng)絡(luò)擁塞博弈^［20］等。本文的研究便是對ATL進行多值擴展，從而給帶有多值信息的開放系統(tǒng)的驗證問題提供解決方案。與本文研究最相關(guān)的是2017年，袁紅娟等^［21］提出模糊交互時態(tài)邏輯（fuzzy alternating-time temporal logic，F(xiàn)ATL），F(xiàn)ATL所采用的模型是模糊并發(fā)博弈結(jié)構(gòu)（fuzzy concurrent gamejz4IHhVIUWeHLJJfgOazyGpm2KL5Ehn9mJ0KYUlOa2k= structure，F(xiàn)CGS），其主要創(chuàng)新在于將CGS中原子命題的取值從二值擴展至［0，1］區(qū)間。然而，這一擴展仍然存在一些限制，尤其是在應對帶有不一致信息的開放系統(tǒng)時。因此，

本文采用多值并發(fā)博弈結(jié)構(gòu)（multi-valued concurrent game structure，MVCGS），將CGS中原子命題的取值與狀態(tài)間的遷移值從二值推廣到多值的情形。這一創(chuàng)新不僅適用于存在不一致信息的開放系統(tǒng)，還可用于各類帶有多值信息的開放系統(tǒng)。

1 預備知識

本節(jié)將簡要地介紹格論和格值集合的一些相關(guān)符號和概念，更多細節(jié)可以參考文獻［7，22］。

令=（L，≤）是一個格，對于任意的x，y∈L，當x≤y不成立時，用符號xy來指代。若有x∈L，對于任意的a，b∈L，滿足當x≠0且x=a∨b時，有x=a或x=b，則稱x為的并即約元。在分配格中，若x∈L且x≠0，則x為的并即約元當且僅當x≤a∨b時，有x≤a或x≤b。令JI（）為中并即約元的集合，若是一個有限分配格，則稱是由并即約元生成的，即對于任意的x∈L，有x=∨{y∈JI（）：y≤x}。

當可由上下文清楚地確定時，并即約元的集合

JI（）可以簡寫為JI。

對于任意給定的一個格=（L，≤）和一個經(jīng)典的集合X，集合X上的格值集f：X→L是一個函數(shù)。當可由上下文清楚地確定時，格值集f可以被簡寫成f，

f也被稱為多值集合，并用（X）指代X在格上的所有多值集合構(gòu)成的集合。對于任意的f，g∈（X），如果滿足對于任意的x∈X都有f（x）≤g（x），則稱fg。若fg且gf，則稱f=g。多值集合f的一個支撐是集合supp（f）={x∈Xf（x）>0}，其中0是格中的最小元。

令=（L，≤）是一個偏序集，對于一個給定的函數(shù)f：L→L和任意的x，y∈L，若x≤y時有f（x）≤f（y），則稱函數(shù)f是單調(diào)的。對于一個元素x∈L，若x=f（x），則稱x是函數(shù)f的一個不動點；若x≤f（x），則稱x是函數(shù)f的一個后置不動點；若x≥f（x），則稱x是函數(shù)f的一個前置不動點。對于完備格上的單調(diào)函數(shù)f：L→L，Tarski定理^［22］保證了最小不動點和最大不動點的存在，分別用符號μf和νf表示。

除非另有明確說明，否則將會被假設(shè)為具有最小元0、最大元1和補運算的有限分配格，其中0≠1。

2 多值交互時序邏輯

2.1 多值并發(fā)博弈結(jié)構(gòu)（MVCGS）

為了對具有不確定性和不一致信息的開放系統(tǒng)進行建模和分析，將文獻［18］的CGS推廣到多值的情形，從而得到MVCGS，即狀態(tài)上的原子命題的取值與狀態(tài)間的遷移值不再是真或假，而是De Morgan代數(shù)^［7］上的一個元素，其具體定義如下。

定義1 MVCGS是一個六元組，M=（n，Q，Π，π，d，δ），其中：

1） n≥1是系統(tǒng)中智能體的個數(shù)，用自然數(shù)1，…，n來指代每一個智能體，用Σ來代表智能體的集合{1，…，n}。

2） Q是一個非空的有限狀態(tài)集合。

3） Π是一個原子命題的有限集合。

4） π：Q→（Π）是一個賦值函數(shù)。對于狀態(tài)s∈Q和原子命題p∈Π，π（s）（p）表示原子命題p在狀態(tài)s上成立

的可能性。

5） 對于任意狀態(tài)q∈Q和任意智能體a∈Σ，da（q）≥1是一個自然數(shù)，表示智能體a在狀態(tài)q上可選的動作數(shù)，用數(shù)字1，…，da（q）來指代智能體a在狀態(tài)q上的動作。對于每個狀態(tài)q∈Q，在q上的一個動作向量是一個n元組〈j1，…，jn〉，它滿足對于任意的智能體a都有1≤ja≤da（q）。給定一個狀態(tài)q∈Q，用D（q）來表示動作向量的集合{1，…，d1（q）}×…×{1，…，dn（q）}Nn，用D（Q）=∪{D（q）q∈Q}來指代所有狀態(tài)上的動作向量構(gòu)成的集合，函數(shù)D被稱為動作函數(shù)。

6） δ：Q×D（Q）→（Q）是一個多值遷移函數(shù)。對于任意的q∈Q，δ（q，j1，…，jn）（q′）表示的是當智能體們博弈的結(jié)果為〈j1，…，jn〉∈D（q）時，系統(tǒng)從狀態(tài)q遷移到狀態(tài)q′的真值，其中q′∈Q。

對于任意的q∈Q和任意的動作向量〈j1，…，jn〉∈D（q），假設(shè)supp（δ（q，j1，…， jn））≠。若δ（q，j1，…，jn）（q′）的值大于格中的最小元0，則稱q′是q的后繼，且有q′∈supp（δ（q，j1，…，jn））。

在一個MVCGS中，路徑λ是一條狀態(tài)與動作交替的無限序列，即

λ=q0σ0q1σ1…，

其中：qi∈Q，σi∈D（qi），且滿足對于任意的i≥0，δ（qi，j1，…，jn）（qi+1）>0。將起始狀態(tài)為q的路徑稱為q-路徑。一條有限路徑ρ是一條無限路徑的前綴，該前綴終止在狀態(tài)qn，并用符號last（ρ）來指代狀態(tài)qn。用PathM，q（FPathM，q）來表示從狀態(tài)q開始的所有無限路徑（有限路徑）的集合，并用PathM（FPathM）來指代在結(jié)構(gòu)M中的所有無限路徑（有限路徑）。路徑中狀態(tài)的個數(shù)用ρ來表示。給定一條無限路徑λ，和下標i≥0，

λ（i），λ［i］和λ［0，i］分別表示與λ的第i+1個遷移相關(guān)的動作向量，λ的第i+1個狀態(tài)和λ中長度為i+1的有限前綴。

智能體集合Σ上的一個子集AΣ，被稱為一個聯(lián)盟。為了方便起見，用符號來指代Σ＼A。

很顯然，經(jīng)典CGS是MVCGS的一種特殊情況，當格中的集合L={0，1}時，MVCGS就變成了一個經(jīng)典CGS。

設(shè)1表示一定為真，0表示一定為假，DK表示不知道，DC表示不關(guān)心，S表示應該為真，N表示不應該為真。

為了更好地理解定義1，下面給出一個簡單的例子。

例1 用一個MVCGS M=（n，Q，Π，π，d，δ）和=（2×2+2，≤，）來建模市場中兩家飲料公司銷售可樂的情況，其具體建模情況如下。

1） n=2，表示有兩家公司：公司1和公司2。

2） Q={s0，s1，s2}，其中：s0表示市場處于供小于求的狀態(tài)；s1表示市場處于供給平衡的狀態(tài)；s2表示市場處于供大于求的狀態(tài)。

3） Π={p，r}，表示公司1銷售可樂的方式，其中：p表示高價壟斷；r表示薄利多銷。

4） π（s0）（p）=DK，π（s2）（r）=DK，π（s1）（p）=π（s1）（r）=DC，π（s0）（r）=π（s2）（p）=0。例如，

π（s2）（r）=DK表示在供大于求的市場狀態(tài)下，公司1采取薄利多銷的可能性為“不知道”。

5） 各公司動作的建模為：d1（s0）=d1（s1）=d1（s2）={1，2}，d2（s0）=d2（s1）=d2（s2）={1，2}。例如，d1（s0）={1，2}表示供小于求的情況下，公司1增加自家可樂的產(chǎn)量投入市場（動作1）和改善可樂的配方從而改善可樂的味道（動作2）。

6） 遷移函數(shù)為：δ（s0，1，1）（s1）=δ（s2，1，2）（s1）=δ（s1，1，1）（s2）=δ（s1，1，2）（s1）=DK，δ（s0，2，2）（s0）=δ（s2，2，2）（s2）=DC，δ（s0，1，2）（s1）=δ（s0，2，1）（s0）=δ（s1，2，1）（s0）=δ（s2，1，1）（s1）=S，δ（s1，2，2）（s0）=T，δ（s2，2，1）（s2）=N。例如，δ（s0，1，1）（s1）=DK表示在供小于求的市場狀態(tài)下，公司1和公司2分別采取增加自家可樂產(chǎn)量投入市場和提高可樂售價的動作后，市場從供小于求的狀態(tài)遷移到供給平衡的狀態(tài)的可能性為“不知道”。

MVCGS的示例圖如圖1所示，在圖中用圓圈表示模型的狀態(tài)。對于任意的s∈Q，σ∈D（s）和t∈supp（δ（s，σ）），采用一條從s到t且被σδ（s，σ）（t）標記的邊來表示遷移。對于δ（s，σ）（t）=0的遷移，則從圖中刪除。

格2×2+2的示例圖如圖2所示，在圖中展示了格=（2×2+2，≤，）的哈斯圖。

2.2 多值交互時序邏輯（MVATL）

為了描述含有不一致和不確定信息的開放系統(tǒng)的系統(tǒng)規(guī)約，引入多值交互時序邏輯（multi-valued alternating-time temporal logic，MVATL）作為MVCGS的規(guī)約語言。在語法上，MVATL是計算樹邏輯的多模態(tài)版本，其為每個聯(lián)盟AΣ關(guān)聯(lián)了如下的模態(tài)算子。

1） 〈〈A〉〉Xφ表示聯(lián)盟A下一次遷移的結(jié)果會滿足φ。

2） 〈〈A〉〉Gφ表示聯(lián)盟A每次遷移的結(jié)果都滿足φ。

3） 〈〈A〉〉φ1Uφ2表示聯(lián)盟A在保持遷移的結(jié)果都滿足φ1的同時，最終會有一個遷移的結(jié)果滿足φ2。

定義2 令Π是原子命題的集合，MAVTL公式的語法歸納定義為

φ∶

pφφ1∨φ2〈〈A〉〉Xφ

〈〈A〉〉Gφ〈〈A〉〉φ1Uφ2，

其中：p∈Π；AΣ。

2.3 基于MVCGS的MVATL語義

接下來將提供基于MVCGSs的MVATL的語義解釋。令q，q′∈Q，AΣ，其中A=m，A-動作σ是一個m元組（σa）a∈A，并滿足對于任意的a∈A，都有1≤σa≤da（q）。用符號DA（q）來指代在狀態(tài)q上的所有A-動作的集合。當存在一個動作向量〈j1，…，jn〉∈D（q），使得對于任意的智能體a∈A，有ja=σa，那么就說該動作向量〈j1，…，jn〉與A-動作σ∈DA（q）是一致的，并用out（σ）來指代與A-動作σ一致的動作向量的集合。

值得注意的是，對于一個A-動作σ∈DA（q）和一個-動作σ′∈D（q），它們的組合可以定義一個唯一的動作向量〈j1，…，jn〉∈D（q）。其中，如果i∈A，則ji=σi；如果i∈，則ji=σ′i。令AΣ，A-策略FA是一個映射FA：FPathM→∪｛DA（q）q∈Q}，并滿足對于任意的ρ∈FPathM，都有FA（ρ）∈DA（last（ρ））。使用符號ΠA來指代所有A-策略FA構(gòu)成的集合。當A={a}時，A-策略FA便是智能體a的一個策略。對于一個q-路徑λ=q0σ0q1σ1…，其中q0=q，如果對于任意的i≥0，都有λ（i）∈out（FA（λ［0，i］））（out（F（λ［0，i］）））且狀態(tài)qi+1是狀態(tài)qi的后繼，則稱λ與FA是一致的，并用out（q，F(xiàn)A）來指代與A-策略FA一致的q-路徑的集合。值得注意的是，當起始狀態(tài)q、A-策略FA和-策略F都固定時，MVCGS M就歸約成一個多值Kripke結(jié)構(gòu)。

定義3 令M=（n，Q，Π，π，d，δ）是MVCGS，φ為MVATL公式，對于任意的狀態(tài)q∈Q，φ在M上的語義定義為

‖p‖（q）=π（q）（p），

‖φ‖（q）=‖φ‖（q），

‖φ1∨φ2‖（q）=‖φ1‖（q）∨‖φ2‖（q），

‖〈〈A〉〉Xφ‖（q）=supFA∈ΠA

infF

∈Πsupλ∈out（q，F(xiàn)A，F(xiàn)）

（δ

（q，F(xiàn)A（q），F(xiàn)（q））（λ［1］）∧‖φ‖（λ［1］）），

‖〈〈A〉〉Gφ‖（q）=supFA∈ΠA

infF∈Πsupλ∈out（q，F(xiàn)A，F(xiàn)）infi≥0（‖φ‖（λ［i］）∧

δ（λ［i］，F(xiàn)A（λ［0，i］），F(xiàn)（λ［0，i］））（λ［i+1］）），

‖〈〈A〉〉φ1Uφ2‖（q）=supFA∈ΠA

infF∈Π

supλ∈out（q，F(xiàn)A，F(xiàn)）

supi≥0

（inf0≤j<i（‖φ1‖（λ［j］）∧δ（λ［j］，F(xiàn)A（λ［0，j］），F(xiàn)（λ［0，j］））（λ［j+1］）∧‖φ2‖（λ［i］））。

3 MVATL的模型檢驗算法

本節(jié)將根據(jù)上述定義的語法和語義，證明MVATL的不動點特性，并給出相應的模型檢驗算法。

3.1 時序算子的不動點特性

引理1 下列不動點特性成立。

1） 對于任意的多值集合Y∈（Q），令函數(shù)F1表示為

F1（Y）（q）=‖φ‖（q）∧

supσA∈DA（q）inf

σ∈D（q）supq′∈Q（δ（q，

σA，σ）（q′）∧Y（q′））。（1）

‖〈〈A〉〉Gφ‖是函數(shù)F1的一個最大不動點，即‖〈〈A〉〉Gφ‖=νY.F1（Y）。

2） 對于任意的多值集合Y∈（Q），令函數(shù)F2表示為

F2（Y）（q）=‖φ2‖（q）∨（‖φ1‖（q）∧

supσA∈DA（q）

infσ∈D（q）supq′∈Q（δ（q，σA，σ）（q′）∧Y（q′）））。（2）

‖〈〈A〉〉φ1Uφ2‖是函數(shù)F2的一個最小不動點，即‖〈〈A〉〉φ1Uφ2‖=μY.F2（Y）。

證明 1） 易證F1是單調(diào)的。因此，由Tarski不動點定理知，算子F1具有一個最大不動點。令

q∈Q且l∈JI，并且滿足

l≤‖〈〈A〉〉Gφ‖（q），由定義3可知，存在一個A-策略FA，對于任意的

-策略F，存在一條q-路徑

λ∈out（q，F(xiàn)A，F(xiàn)）滿足對于任意的i≥0，有l(wèi)≤‖φ‖（λ［i］）∧δ（λ［i］，F(xiàn)A（λ［0，i］），F(xiàn)（λ［0，i］））（λ［i+1］）。特別地，λ［0］=q，即

l≤‖φ‖（q）。（3）

對于任意的σ∈out（q，F(xiàn)A（q）），設(shè)F′A是一個A-策略，表示從狀態(tài)q到達狀態(tài)λ［1］之后A-策略FA的后續(xù)部分。令λ［1］=q′，那么由

F′A的定義可知，存在q′-路徑λ′∈out（q′，F(xiàn)′A），有F′A（λ′）=FA（qσλ′），其中σ=〈FA（q），F(xiàn)（q）〉，且有

l≤‖〈〈A〉〉Gφ‖（q′）。令FA（q）=σA，F(xiàn)（q）=σ，則有

l≤supσA∈DA（q）infσ∈D（q）

supq′∈Q

（δ（q，σA，

σ）（q′）∧‖〈〈A〉〉Gφ‖（q′））。（4）

綜合式（3）和式（4），可得

l≤‖φ‖（q）∧supσA∈DA（q）infσ∈D（q）

supq′∈Q（δ

（q，σA，σ）（q′）∧‖〈〈A〉〉Gφ‖（q′））。（5）

因此，‖〈〈A〉〉Gφ‖是算子F1的一個后置不動點。

接著令Z是算子F1的一個后置不動點。構(gòu)建一個A-策略FA，使得對于任意的-策略F∈Π，都會存在一條q-路徑λ∈out（q，F(xiàn)A，F(xiàn)），使得對于路徑λ的任意非空有限前綴ρ的最后一個狀態(tài)last（ρ），有

l≤‖φ‖（last（ρ）），（6）

l≤supσA∈DA（last（ρ））infσ∈D（last（ρ））

supq′∈Q（δ（last

（ρ），σA，σ）（q′）∧Z（q′））。（7）

對ρ的長度實施歸納法證明，當ρ=1時，即ρ=q。若l≤Z（q），則由F1的定義可知l≤‖φ‖（q）且存在某個σA∈DA（q），對于任意的σ∈D（q），都會存在一個q′∈Q，使得l≤δ（q，σA，σ）（q′）∧Z（q′）。因此，令FA（ρ）=σA，F(xiàn)（ρ）=σ時，式（6）和式（7）成立。

當ρ=k時，假設(shè)已經(jīng)構(gòu)建出策略FA，使得式（6）和式（7）成立。根據(jù)歸納假設(shè)可知，存在一個q′∈Q，使得

l≤Z（q′）≤‖φ‖（q′）∧（supσA∈DA（q′）

infσ∈D（q′）

supq″∈Q

δ（q′，σA，σ）（q″）∧Z（q″））。（8）

即l≤‖φ‖（q′）且存在某個σA∈DA（q′），對于任意的σ∈D（q′），都會存在一個q″∈Q，使得l≤δ（q′，σA，σ）（q″）∧Z（q″）。因此，令

FA（ρ〈FA（ρ），F(xiàn)（ρ）〉q′）=σA，

F（ρ〈FA（ρ），F(xiàn)（ρ）〉q′）=σ（9）

時，式（6）和式（7）成立。那么由FA的構(gòu)造方法可知，l≤‖〈〈A〉〉Gφ‖（q）。因此，‖〈〈A〉〉Gφ‖是算子F1的最大后置不動點。

2） 易證算子F2也是單調(diào)的。因此，由Tarski不動點定理知，算子F2具有一個最小不動點。令

q∈Q且l∈JI，并且滿足

l≤F2（‖〈〈A〉〉φ1Uφ2‖）（q），那么由定義3可知，

l≤‖φ2‖（q），（10）

或者

l≤‖φ1‖（q）∧supσA∈DA（q）

infσ∈D（q）

supq′∈Q（δ

（q，σA，σ）（q′）∧‖〈〈A〉〉φ1Uφ2‖（q′））。（11）

若式（10）成立，那么由定義3知，l≤‖〈〈A〉〉φ1Uφ2‖（q）。若式（11）成立，即l≤‖φ1‖（q）且存在某個σA∈DA（q），對于任意的σ∈D（q），都會存在某個q′∈Q，使得l≤δ（q，σA，σ）（q′）∧‖〈〈A〉〉φ1Uφ2‖（q′），即存在一個

A-策略F′A使得q′滿足〈〈A〉〉φ1Uφ2的語義解釋。那么構(gòu)造A-策略FA，使得FA（q）=σA，且滿足對于任意的σ∈D（q），有FA（q〈σA，σ〉λ′）=F′A（λ′）。因此，由定義3可知，l≤‖〈〈A〉〉φ1Uφ2‖（q）。綜上可得，‖〈〈A〉〉φ1Uφ2‖是算子F2的一個前置不動點。

接著令Y是算子F2的一個前置不動點。設(shè)l≤‖〈〈A〉〉φ1Uφ2‖（q），由定義3可知，存在一條q-路徑λ∈out（q，F(xiàn)A，F(xiàn)）滿足存在某個i≥0，使得l≤‖φ2‖（λ［i］），且對于任意的0≤j<i，有l(wèi)≤‖φ1‖（λ［j］）∧δ（λ［j］，F(xiàn)A（λ［0，j］），F(xiàn)（λ［0，j］））（λ［j+1］）。

設(shè)I是i的集合，令k=maxI。當k=0時，由F2的定義知，l≤Y（q）。

設(shè)k≤m時，若l≤‖〈〈A〉〉φ1Uφ2‖（q），則l≤Y（q）。當k=m+1時，令l≤‖〈〈A〉〉φ1Uφ2‖（q），那么由定義3可知，存在一個

A-策略FA，對于任意的-策略F，存在一條

q-路徑λ∈out（q，F(xiàn)A，F(xiàn)），有q′∈supp（δ（q，F(xiàn)A（λ），F(xiàn)（λ））），滿足對于i≤m，

即l≤‖〈〈A〉〉φ1Uφ2‖（q′），那么由歸納假設(shè)可知l≤Y（q′）。因此，當k=m+1時，由F2的定義可知，l≤Y（q）。

綜上可知，‖〈〈A〉〉φ1Uφ2‖是算子F2的最小不動點。

3.2 模型檢驗

本節(jié)將利用MVATL的不動點特性來解決模型檢驗問題，該模型檢驗問題可以定義為：對于一個給定的MVCGS M，一個在M中的狀態(tài)q和一個MVATL公式φ，計算‖φ‖（q）的值。為了方便討論，下面給出MVATL公式的長度定義。

令φ是一個MVATL公式，其長度記作φ，歸納定義為

p=1，

φ1=〈〈A〉〉Xφ1=φ1+1，

φ1∨φ2=〈〈A〉〉φ1Uφ2=φ1+φ2+1。

令模型MVCGS M的狀態(tài)數(shù)為Q，智能體數(shù)為k=Σ，那么M的規(guī)模大小為

M=Q+∑q∈Q∑σ∈D（q）supp（δ（q，σ））。

引理2 對于任意的p，r∈AP，最多需要L·Q次迭代就可以計算出‖〈〈A〉〉pUr‖和‖〈〈A〉〉Gp‖的值。

證明 對于任意給定的p，r∈AP，定義一系列在Q上的多值集合g0，g1，…，即對任意的i≥0，gi∈（Q）如下：對任意的s∈Q，

g0（s）=0，

gi+1（s）=‖r‖（s）∨（‖p‖（s）∧

supσA∈DA（s）infσ∈D（s）sups′∈Q（δ（s，σA，σ）（s′）∧gi（s′）））。由引理1可知，算子F2是單調(diào)的，當i=0時，

有g(shù)0g1。

設(shè)i=k時，gigi+1成立。當i=k+1時，由歸納假設(shè)知gi-1gi，因此F2（gi-1）F2（gi）。那么由F2（gi-1）=gi以及F2（gi）=gi+1，可得gigi+1。因此，對任意的i≥0，有g(shù)igi+1。又因為L和Q是有限的，所以由Tarski不動點定理可知，等式gi+1=gi最多會在L·Q次迭代后成立，即‖〈〈A〉〉pUr‖=g|L|·|Q|。同理可證，‖〈〈A〉〉Gp‖最多也只需要L·Q次迭代。

下面給出‖〈〈A〉〉pUr‖的算法，‖〈〈A〉〉Gp‖的算法也可按照類似的方法給出。

算法1 計算‖〈〈A〉〉pUr‖

輸入： 一個帶有狀態(tài)集合Q和格=（L，≤，）的MVCGS M，MVATL公式〈〈A〉〉pUq。

輸出： ‖〈〈A〉〉pUr‖。

1. 令g，t是在L（Q）上的格值集合；

2. 將g的值初始化為0；

3. for i←1 to L·Q do

4. 將g的值復制到t中；

5. for s∈Q do

6. g（s）←‖q‖（s）∨（‖p‖（s）∧supσA∈DA（s）

infσ∈D（s）sups′∈Q（δ（s，σA，σ）（s′）∧t（s′）））

7. return g

下面給出一個重要結(jié)論。

定理1 給定一個MVCGS M=（n，Q，Π， π，d，δ）和MVATL公式φ，φ的模型檢驗問題都可以在O（L·Q·M·φ）時間內(nèi)解決。

證明 由引理2可知，最多通過L·Q次迭代就可以到達一個不動點，而每次迭代都需要花費M的時間。因此，對于每個不動點的計算最多需要花費L·Q·M的時間。由于每個公式最多包含φ個子公式，可知不動點算法解決MVATL公式的模型檢驗問題的時間為O（L·Q·M·φ）。

下面給出一個示例來說明該不動點算法是如何解決MVATL的模型檢驗問題的。

例2 令M是例1所定義的MVCGS，

A=｛1｝，φ=〈〈A〉〉pUr。令g0（s）=0且

gi+1（s）=‖r‖（s）∨（‖p‖（s）∧

supσA∈DA（s）infσ∈D（s）sups′∈Q（δ（s，σA，σ）（s′）∧gi（s′））），

其中i≥0，s∈Q。

由g的定義可知，當i=0時，有g(shù)1（s0）=0，g1（s1）=DC，g1（s2）=DK。當i=1時，經(jīng)計算可得g2（s0）=N，g2（s1）=DC，g2（s2）=DK。當i=2時，可知g3（s0）=N，g3（s1）=DC，g3（s2）=DK。那么由引理2可知，‖〈〈A〉〉pUr‖=g2。

4 結(jié)語

本文研究了MVATL的模型檢驗問題，引入MVGCS作為此類開放系統(tǒng)的模型，給出基于此模型的MVATL的語法和語義，擴展了多值模型檢驗技術(shù)的應用范圍，使其可以適用于具有不確定和不一致信息的開放系統(tǒng)。研究結(jié)果表明，MVATL具有不動點特性?；诖私Y(jié)論，采用不動點迭代算法來解決MVATL的模型檢驗問題，可以在多項式時間內(nèi)完成對MVATL的模型檢驗。

參考文獻：

［1］ CLARKE E M， GRUMBERG O， PELED D A. Model checking［M］. Cambridge： MIT Press， 1999.

［2］ BAIER C， KATOEN J P. Principles of model checking［M］. Cambridge： MIT Press， 2008.

［3］ 林惠民， 張文輝. 模型檢測： 理論、方法與應用［J］. 電子學報， 2002， 30（S1）： 1907-1912.

LIN H M， ZHANG W H. Model cha106dfc8b1a359e01a8228d1f60f7571ecking： theories， techniques and applications［J］. Acta electronica sinica， 2002， 30（S1）： 1907-1912.

［4］ 王戟， 詹乃軍， 馮新宇， 等. 形式化方法概貌［J］. 軟件學報， 2019， 30（1）： 33-61.

WANG J， ZHAN N J， FENG X Y， et al. Overview of formal methods［J］. Journal of software， 2019， 30（1）： 33-61.

［5］ DING L， WAN H Y， HU L K， et al. Identifying counterexamples without variability in software product line model checking［J］. Computers， materials & continua， 2023， 75（2）： 2655-2670.

［6］ DFAGO X， HERIBAN A， TIXEUIL S， et al. Using model checking to formally verify rendezvous algorithms for robots with lights in Euclidean space［J］. Robotics and autonomous systems， 2023， 163： 104378.

［7］ CHECHIK M， DEVEREUX B， EASTERBROOK S， et al. Multi-valued symbolic model-checking［J］. ACM transactions on software engineering and methodology， 2003， 12（4）： 371-408.

［8］ 王輝， 石鐵柱， 錢俊彥， 等. 模糊Kripke結(jié)構(gòu)的子模型修復算法［J］. 鄭州大學學報（理學版）， 2023， 55（1）： 77-83.

WANG H， SHI T Z， QIAN J Y， et al. The sub-model repair algorithm of fuzzy Kripke structures［J］. Journal of Zhengzhou university （natural science edition）， 2023， 55（1）： 77-83.

［9］ 馬占有， 李健祥， 李召愷， 等. 廣義可能性計算樹邏輯模型檢測中的成本分析［J］. 鄭州大學學報（理學版）， 2022， 54（4）： 34-41.

MA Z Y， LI J X， LI Z K， et al. Cost analysis of generalized possibilistic computation tree logic model checking［J］. Journal of Zhengzhou university （natural science edition）， 2022， 54（4）： 34-41.

［10］DEPTUA A， AUGUSTYNOWICZ A， STOSIAK M， et al. The concept of using an expert system and multi-valued logic trees to assess the energy consumption of an electric car in selected driving cycles［J］. Energies， 2022， 15（13）： 4631.

［11］WANG J Y， LIN Y Z， HU C H， et al. A kind of optoelectronic memristor model and its applications in multi-valued logic［J］. Electronics， 2023， 12（3）： 646.

［12］PAN H Y， LI Y M， CAO Y Z， et al. Model checking computation tree logic over finite lattices［J］. Theoretical computer science， 2016， 612： 45-62.

［13］MELLER Y， GRUMBERG O， SHOHAM S. A framework for compositional verification of multi-valued systems via abstraction-refinement［J］. Information and computation， 2016， 247： 169-202.

［14］LI Y M， LEI L H， LI S J. Computation tree logic model checking based on multi-valued possibility measures［J］. Information sciences， 2019， 485： 87-113.

［15］LI Y M， WEI J L. Possibilistic fuzzy linear temporal logic and its model checking［J］. IEEE transactions on fuzzy systems， 2021， 29（7）： 1899-1913.

［16］FILATOTCHEV I， IRELAND R D， STAHL G K. Contextualizing management research： an open systems perspective［J］. Journal of management studies， 2022， 59（4）： 1036-1056.

［17］LU Z Y， DELANEY D T， LILLIS D. A survey on microservices trust models for open systems［J］. IEEE access， 2023， 11： 28840-28855.

［18］ALUR R， HENZINGER T A， KUPFERMAN O. Alternating-time temporal logic［J］. Computer standards & interfaces， 1999， 21（2）： 142.

［19］NAM W， KIL H. Formal verification of blockchain smart contracts via ATL model checking［J］. IEEE access， 2022， 10： 8151-8162.

［20］GOEMINNE A， MARKEY N， SANKUR O. Non-blind strategies in timed network congestion games［C］∥International Conference on Formal Modeling and Analysis of Timed Systems. Cham： Springer International Publishing， 2022： 183-199.

［21］袁紅娟， 馬艷芳， 潘海玉. 模糊交互時態(tài)邏輯的模型檢測［J］. 計算機工程與科學， 2017， 39（12）： 2290-2296.

YUAN H J， MA Y F， PAN H Y. Model checking for fuzzy alternating-time temporal logic［J］. Computer engineering & science， 2017， 39（12）： 2290-2296.

［22］DAVEY B A， PRIESTLEY H A. Introduction to lattices and order［M］. 2nd ed. New York： Cambridge University Press， 2002.