多值交互時(shí)序邏輯的模型檢驗(yàn)研究

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

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

中圖分類號(hào)： TP301

文獻(xiàn)標(biāo)志碼： A

文章編號(hào)： 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 引言

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

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

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

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

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

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

1 預(yù)備知識(shí)

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

令=（L，≤）是一個(gè)格，對(duì)于任意的x，y∈L，當(dāng)x≤y不成立時(shí)，用符號(hào)xy來(lái)指代。若有x∈L，對(duì)于任意的a，b∈L，滿足當(dāng)x≠0且x=a∨b時(shí)，有x=a或x=b，則稱x為的并即約元。在分配格中，若x∈L且x≠0，則x為的并即約元當(dāng)且僅當(dāng)x≤a∨b時(shí)，有x≤a或x≤b。令JI（）為中并即約元的集合，若是一個(gè)有限分配格，則稱是由并即約元生成的，即對(duì)于任意的x∈L，有x=∨{y∈JI（）：y≤x}。

當(dāng)可由上下文清楚地確定時(shí)，并即約元的集合

JI（）可以簡(jiǎn)寫為JI。

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

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

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

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

2 多值交互時(shí)序邏輯

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

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

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

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

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

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

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

的可能性。

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

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

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

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

λ=q0σ0q1σ1…，

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

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

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

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

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

為了更好地理解定義1，下面給出一個(gè)簡(jiǎn)單的例子。

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

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

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

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

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

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

5） 各公司動(dòng)作的建模為：d1（s0）=d1（s1）=d1（s2）={1，2}，d2（s0）=d2（s1）=d2（s2）={1，2}。例如，d1（s0）={1，2}表示供小于求的情況下，公司1增加自家可樂(lè)的產(chǎn)量投入市場(chǎng)（動(dòng)作1）和改善可樂(lè)的配方從而改善可樂(lè)的味道（動(dòng)作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表示在供小于求的市場(chǎng)狀態(tài)下，公司1和公司2分別采取增加自家可樂(lè)產(chǎn)量投入市場(chǎng)和提高可樂(lè)售價(jià)的動(dòng)作后，市場(chǎng)從供小于求的狀態(tài)遷移到供給平衡的狀態(tài)的可能性為“不知道”。

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

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

2.2 多值交互時(shí)序邏輯（MVATL）

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

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

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

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

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

φ∶

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

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

其中：p∈Π；AΣ。

2.3 基于MVCGS的MVATL語(yǔ)義

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

值得注意的是，對(duì)于一個(gè)A-動(dòng)作σ∈DA（q）和一個(gè)-動(dòng)作σ′∈D（q），它們的組合可以定義一個(gè)唯一的動(dòng)作向量〈j1，…，jn〉∈D（q）。其中，如果i∈A，則ji=σi；如果i∈，則ji=σ′i。令A(yù)Σ，A-策略FA是一個(gè)映射FA：FPathM→∪｛DA（q）q∈Q}，并滿足對(duì)于任意的ρ∈FPathM，都有FA（ρ）∈DA（last（ρ））。使用符號(hào)ΠA來(lái)指代所有A-策略FA構(gòu)成的集合。當(dāng)A={a}時(shí)，A-策略FA便是智能體a的一個(gè)策略。對(duì)于一個(gè)q-路徑λ=q0σ0q1σ1…，其中q0=q，如果對(duì)于任意的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）來(lái)指代與A-策略FA一致的q-路徑的集合。值得注意的是，當(dāng)起始狀態(tài)q、A-策略FA和-策略F都固定時(shí)，MVCGS M就歸約成一個(gè)多值Kripke結(jié)構(gòu)。

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

‖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的模型檢驗(yàn)算法

本節(jié)將根據(jù)上述定義的語(yǔ)法和語(yǔ)義，證明MVATL的不動(dòng)點(diǎn)特性，并給出相應(yīng)的模型檢驗(yàn)算法。

3.1 時(shí)序算子的不動(dòng)點(diǎn)特性

引理1 下列不動(dòng)點(diǎn)特性成立。

1） 對(duì)于任意的多值集合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的一個(gè)最大不動(dòng)點(diǎn)，即‖〈〈A〉〉Gφ‖=νY.F1（Y）。

2） 對(duì)于任意的多值集合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的一個(gè)最小不動(dòng)點(diǎn)，即‖〈〈A〉〉φ1Uφ2‖=μY.F2（Y）。

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

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

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

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

λ∈out（q，F(xiàn)A，F(xiàn)）滿足對(duì)于任意的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）

對(duì)于任意的σ∈out（q，F(xiàn)A（q）），設(shè)F′A是一個(gè)A-策略，表示從狀態(tài)q到達(dá)狀態(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的一個(gè)后置不動(dòng)點(diǎn)。

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

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

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

supq′∈Q（δ（last

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

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

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

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

infσ∈D（q′）

supq″∈Q

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

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

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

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

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

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

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）且存在某個(gè)σA∈DA（q），對(duì)于任意的σ∈D（q），都會(huì)存在某個(gè)q′∈Q，使得l≤δ（q，σA，σ）（q′）∧‖〈〈A〉〉φ1Uφ2‖（q′），即存在一個(gè)

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

接著令Y是算子F2的一個(gè)前置不動(dòng)點(diǎn)。設(shè)l≤‖〈〈A〉〉φ1Uφ2‖（q），由定義3可知，存在一條q-路徑λ∈out（q，F(xiàn)A，F(xiàn)）滿足存在某個(gè)i≥0，使得l≤‖φ2‖（λ［i］），且對(duì)于任意的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。當(dāng)k=0時(shí)，由F2的定義知，l≤Y（q）。

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

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

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

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

綜上可知，‖〈〈A〉〉φ1Uφ2‖是算子F2的最小不動(dòng)點(diǎn)。

3.2 模型檢驗(yàn)

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

令φ是一個(gè)MVATL公式，其長(zhǎng)度記作φ，歸納定義為

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 對(duì)于任意的p，r∈AP，最多需要L·Q次迭代就可以計(jì)算出‖〈〈A〉〉pUr‖和‖〈〈A〉〉Gp‖的值。

證明 對(duì)于任意給定的p，r∈AP，定義一系列在Q上的多值集合g0，g1，…，即對(duì)任意的i≥0，gi∈（Q）如下：對(duì)任意的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)的，當(dāng)i=0時(shí)，

有g(shù)0g1。

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

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

算法1 計(jì)算‖〈〈A〉〉pUr‖

輸入： 一個(gè)帶有狀態(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的值復(fù)制到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

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

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

證明 由引理2可知，最多通過(guò)L·Q次迭代就可以到達(dá)一個(gè)不動(dòng)點(diǎn)，而每次迭代都需要花費(fèi)M的時(shí)間。因此，對(duì)于每個(gè)不動(dòng)點(diǎn)的計(jì)算最多需要花費(fèi)L·Q·M的時(shí)間。由于每個(gè)公式最多包含φ個(gè)子公式，可知不動(dòng)點(diǎn)算法解決MVATL公式的模型檢驗(yàn)問(wèn)題的時(shí)間為O（L·Q·M·φ）。

下面給出一個(gè)示例來(lái)說(shuō)明該不動(dòng)點(diǎn)算法是如何解決MVATL的模型檢驗(yàn)問(wèn)題的。

例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的定義可知，當(dāng)i=0時(shí)，有g(shù)1（s0）=0，g1（s1）=DC，g1（s2）=DK。當(dāng)i=1時(shí)，經(jīng)計(jì)算可得g2（s0）=N，g2（s1）=DC，g2（s2）=DK。當(dāng)i=2時(shí)，可知g3（s0）=N，g3（s1）=DC，g3（s2）=DK。那么由引理2可知，‖〈〈A〉〉pUr‖=g2。

4 結(jié)語(yǔ)

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

參考文獻(xiàn)：

［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］ 林惠民， 張文輝. 模型檢測(cè)： 理論、方法與應(yīng)用［J］. 電子學(xué)報(bào)， 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］. 軟件學(xué)報(bào)， 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)的子模型修復(fù)算法［J］. 鄭州大學(xué)學(xué)報(bào)（理學(xué)版）， 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ì)算樹邏輯模型檢測(cè)中的成本分析［J］. 鄭州大學(xué)學(xué)報(bào)（理學(xué)版）， 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］袁紅娟， 馬艷芳， 潘海玉. 模糊交互時(shí)態(tài)邏輯的模型檢測(cè)［J］. 計(jì)算機(jī)工程與科學(xué)， 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.