多值交互时序逻辑的模型检验研究

摘要： 为了对包含多值信息的开放系统进行形式化验证，在多值逻辑的基础上提出了多值交互时序逻辑并研究了该逻辑的模型检验问题。首先，引入多值并发博弈结构作为此类开放系统的模型，该模型的最大特点是可以建模带有多值信息的开放系统。其次，给出基于此模型的多值交互时序逻辑的语法和语义，该逻辑可以描述带有多值信息的待验证属性。最后，基于不动点理论给出多值交互时序逻辑的模型检验算法，并对算法的时间复杂度进行了分析，结果表明，可以在多项式时间内完成对多值交互时序逻辑的模型检验。

关键词： 模型检验； 多值逻辑； 交互时序逻辑； 并发博弈结构

中图分类号： 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］作为一种自动化验证技术，已广泛应用于软硬件系统行为的验证之中^［5-6］。但随着软硬件系统复杂程度的提高，许多系统呈现出多种不确定性和不一致性，这使得经典的模型检验技术不再适用。为了解决这一问题，研究者提出了多值模型检验技术^［7］。相比经典模型检验技术，多值模型检验技术具有更贴近实际系统、建模方式更灵活以及验证方法更高效等优点^［8-9］。

目前，多值模型检验技术在理论和应用研究方面都取得了显著的进展，如电车能耗决策^［10］、模拟电路^［11］等。2016年，Pan等^［12］研究了取值为一般有限格的多值计算树逻辑（multi-valued computation tree logic，MVCTL）的模型检验问题。同年，Meller等^［13］基于抽象和细化的思想，提出一种用于多值模型检验的组合方法。2019年，Li等^［14］为解决多值逻辑χCTL不能表达定量性质的问题，将可能性理论引入χCTL的模型检验中，完成了对 χCTL的定量分析。2021年，Li等^［15］基于广义可能性度量理论，研究了广义可能性模糊线性时序逻辑（generalized possibilistic fuzzy linear temporal logic，GPoFTL）

的模型检验问题。近年来，多值模型检验的重要性急速攀升，但这些技术不适用于带有不确定性和不一致信息的开放系统^［16-17］的验证。

因此，在解决这一问题之前，先介绍一种应用于传统开放系统的规约语言，该规约语言的出现是因为

封闭系统的行为仅受内部状态的影响，而开放系统在其行为中还会受到外部环境交互的影响。这导致以往的模型检验技术不能直接应用于开放系统中。为此，Alur等^［18］引入并发博弈结构（concurrent game structure，CGS）作为开放系统的行为模型，并提出交互时序逻辑（alternating-time temporal logic，ATL）用以描述开放系统的待验证属性。目前，ATL已在多个领域有了成功的应用，例如区块链智能合约^［19］、网络拥塞博弈^［20］等。本文的研究便是对ATL进行多值扩展，从而给带有多值信息的开放系统的验证问题提供解决方案。与本文研究最相关的是2017年，袁红娟等^［21］提出模糊交互时态逻辑（fuzzy alternating-time temporal logic，FATL），FATL所采用的模型是模糊并发博弈结构（fuzzy concurrent gamejz4IHhVIUWeHLJJfgOazyGpm2KL5Ehn9mJ0KYUlOa2k= structure，FCGS），其主要创新在于将CGS中原子命题的取值从二值扩展至［0，1］区间。然而，这一扩展仍然存在一些限制，尤其是在应对带有不一致信息的开放系统时。因此，

本文采用多值并发博弈结构（multi-valued concurrent game structure，MVCGS），将CGS中原子命题的取值与状态间的迁移值从二值推广到多值的情形。这一创新不仅适用于存在不一致信息的开放系统，还可用于各类带有多值信息的开放系统。

1 预备知识

本节将简要地介绍格论和格值集合的一些相关符号和概念，更多细节可以参考文献［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，≤）和一个经典的集合X，集合X上的格值集f：X→L是一个函数。当可由上下文清楚地确定时，格值集f可以被简写成f，

f也被称为多值集合，并用（X）指代X在格上的所有多值集合构成的集合。对于任意的f，g∈（X），如果满足对于任意的x∈X都有f（x）≤g（x），则称fg。若fg且gf，则称f=g。多值集合f的一个支撑是集合supp（f）={x∈Xf（x）>0}，其中0是格中的最小元。

令=（L，≤）是一个偏序集，对于一个给定的函数f：L→L和任意的x，y∈L，若x≤y时有f（x）≤f（y），则称函数f是单调的。对于一个元素x∈L，若x=f（x），则称x是函数f的一个不动点；若x≤f（x），则称x是函数f的一个后置不动点；若x≥f（x），则称x是函数f的一个前置不动点。对于完备格上的单调函数f：L→L，Tarski定理^［22］保证了最小不动点和最大不动点的存在，分别用符号μf和νf表示。

除非另有明确说明，否则将会被假设为具有最小元0、最大元1和补运算的有限分配格，其中0≠1。

2 多值交互时序逻辑

2.1 多值并发博弈结构（MVCGS）

为了对具有不确定性和不一致信息的开放系统进行建模和分析，将文献［18］的CGS推广到多值的情形，从而得到MVCGS，即状态上的原子命题的取值与状态间的迁移值不再是真或假，而是De Morgan代数^［7］上的一个元素，其具体定义如下。

定义1 MVCGS是一个六元组，M=（n，Q，Π，π，d，δ），其中：

1） n≥1是系统中智能体的个数，用自然数1，…，n来指代每一个智能体，用Σ来代表智能体的集合{1，…，n}。

2） Q是一个非空的有限状态集合。

3） Π是一个原子命题的有限集合。

4） π：Q→（Π）是一个赋值函数。对于状态s∈Q和原子命题p∈Π，π（s）（p）表示原子命题p在状态s上成立

的可能性。

5） 对于任意状态q∈Q和任意智能体a∈Σ，da（q）≥1是一个自然数，表示智能体a在状态q上可选的动作数，用数字1，…，da（q）来指代智能体a在状态q上的动作。对于每个状态q∈Q，在q上的一个动作向量是一个n元组〈j1，…，jn〉，它满足对于任意的智能体a都有1≤ja≤da（q）。给定一个状态q∈Q，用D（q）来表示动作向量的集合{1，…，d1（q）}×…×{1，…，dn（q）}Nn，用D（Q）=∪{D（q）q∈Q}来指代所有状态上的动作向量构成的集合，函数D被称为动作函数。

6） δ：Q×D（Q）→（Q）是一个多值迁移函数。对于任意的q∈Q，δ（q，j1，…，jn）（q′）表示的是当智能体们博弈的结果为〈j1，…，jn〉∈D（q）时，系统从状态q迁移到状态q′的真值，其中q′∈Q。

对于任意的q∈Q和任意的动作向量〈j1，…，jn〉∈D（q），假设supp（δ（q，j1，…， jn））≠。若δ（q，j1，…，jn）（q′）的值大于格中的最小元0，则称q′是q的后继，且有q′∈supp（δ（q，j1，…，jn））。

在一个MVCGS中，路径λ是一条状态与动作交替的无限序列，即

λ=q0σ0q1σ1…，

其中：qi∈Q，σi∈D（qi），且满足对于任意的i≥0，δ（qi，j1，…，jn）（qi+1）>0。将起始状态为q的路径称为q-路径。一条有限路径ρ是一条无限路径的前缀，该前缀终止在状态qn，并用符号last（ρ）来指代状态qn。用PathM，q（FPathM，q）来表示从状态q开始的所有无限路径（有限路径）的集合，并用PathM（FPathM）来指代在结构M中的所有无限路径（有限路径）。路径中状态的个数用ρ来表示。给定一条无限路径λ，和下标i≥0，

λ（i），λ［i］和λ［0，i］分别表示与λ的第i+1个迁移相关的动作向量，λ的第i+1个状态和λ中长度为i+1的有限前缀。

智能体集合Σ上的一个子集AΣ，被称为一个联盟。为了方便起见，用符号来指代Σ＼A。

很显然，经典CGS是MVCGS的一种特殊情况，当格中的集合L={0，1}时，MVCGS就变成了一个经典CGS。

设1表示一定为真，0表示一定为假，DK表示不知道，DC表示不关心，S表示应该为真，N表示不应该为真。

为了更好地理解定义1，下面给出一个简单的例子。

例1 用一个MVCGS M=（n，Q，Π，π，d，δ）和=（2×2+2，≤，）来建模市场中两家饮料公司销售可乐的情况，其具体建模情况如下。

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

2） Q={s0，s1，s2}，其中：s0表示市场处于供小于求的状态；s1表示市场处于供给平衡的状态；s2表示市场处于供大于求的状态。

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表示在供大于求的市场状态下，公司1采取薄利多销的可能性为“不知道”。

5） 各公司动作的建模为：d1（s0）=d1（s1）=d1（s2）={1，2}，d2（s0）=d2（s1）=d2（s2）={1，2}。例如，d1（s0）={1，2}表示供小于求的情况下，公司1增加自家可乐的产量投入市场（动作1）和改善可乐的配方从而改善可乐的味道（动作2）。

6） 迁移函数为：δ（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表示在供小于求的市场状态下，公司1和公司2分别采取增加自家可乐产量投入市场和提高可乐售价的动作后，市场从供小于求的状态迁移到供给平衡的状态的可能性为“不知道”。

MVCGS的示例图如图1所示，在图中用圆圈表示模型的状态。对于任意的s∈Q，σ∈D（s）和t∈supp（δ（s，σ）），采用一条从s到t且被σδ（s，σ）（t）标记的边来表示迁移。对于δ（s，σ）（t）=0的迁移，则从图中删除。

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

2.2 多值交互时序逻辑（MVATL）

为了描述含有不一致和不确定信息的开放系统的系统规约，引入多值交互时序逻辑（multi-valued alternating-time temporal logic，MVATL）作为MVCGS的规约语言。在语法上，MVATL是计算树逻辑的多模态版本，其为每个联盟AΣ关联了如下的模态算子。

1） 〈〈A〉〉Xφ表示联盟A下一次迁移的结果会满足φ。

2） 〈〈A〉〉Gφ表示联盟A每次迁移的结果都满足φ。

3） 〈〈A〉〉φ1Uφ2表示联盟A在保持迁移的结果都满足φ1的同时，最终会有一个迁移的结果满足φ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）来指代在状态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构成的集合。当A={a}时，A-策略FA便是智能体a的一个策略。对于一个q-路径λ=q0σ0q1σ1…，其中q0=q，如果对于任意的i≥0，都有λ（i）∈out（FA（λ［0，i］））（out（F（λ［0，i］）））且状态qi+1是状态qi的后继，则称λ与FA是一致的，并用out（q，FA）来指代与A-策略FA一致的q-路径的集合。值得注意的是，当起始状态q、A-策略FA和-策略F都固定时，MVCGS M就归约成一个多值Kripke结构。

定义3 令M=（n，Q，Π，π，d，δ）是MVCGS，φ为MVATL公式，对于任意的状态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，FA，F）

（δ

（q，FA（q），F（q））（λ［1］）∧‖φ‖（λ［1］）），

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

infF∈Πsupλ∈out（q，FA，F）infi≥0（‖φ‖（λ［i］）∧

δ（λ［i］，FA（λ［0，i］），F（λ［0，i］））（λ［i+1］）），

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

infF∈Π

supλ∈out（q，FA，F）

supi≥0

（inf0≤j<i（‖φ1‖（λ［j］）∧δ（λ［j］，FA（λ［0，j］），F（λ［0，j］））（λ［j+1］）∧‖φ2‖（λ［i］））。

3 MVATL的模型检验算法

本节将根据上述定义的语法和语义，证明MVATL的不动点特性，并给出相应的模型检验算法。

3.1 时序算子的不动点特性

引理1 下列不动点特性成立。

1） 对于任意的多值集合Y∈（Q），令函数F1表示为

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

supσA∈DA（q）inf

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

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

‖〈〈A〉〉Gφ‖是函数F1的一个最大不动点，即‖〈〈A〉〉Gφ‖=νY.F1（Y）。

2） 对于任意的多值集合Y∈（Q），令函数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‖是函数F2的一个最小不动点，即‖〈〈A〉〉φ1Uφ2‖=μY.F2（Y）。

证明 1） 易证F1是单调的。因此，由Tarski不动点定理知，算子F1具有一个最大不动点。令

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

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

-策略F，存在一条q-路径

λ∈out（q，FA，F）满足对于任意的i≥0，有l≤‖φ‖（λ［i］）∧δ（λ［i］，FA（λ［0，i］），F（λ［0，i］））（λ［i+1］）。特别地，λ［0］=q，即

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

对于任意的σ∈out（q，FA（q）），设F′A是一个A-策略，表示从状态q到达状态λ［1］之后A-策略FA的后续部分。令λ［1］=q′，那么由

F′A的定义可知，存在q′-路径λ′∈out（q′，F′A），有F′A（λ′）=FA（qσλ′），其中σ=〈FA（q），F（q）〉，且有

l≤‖〈〈A〉〉Gφ‖（q′）。令FA（q）=σA，F（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的一个后置不动点。构建一个A-策略FA，使得对于任意的-策略F∈Π，都会存在一条q-路径λ∈out（q，FA，F），使得对于路径λ的任意非空有限前缀ρ的最后一个状态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（ρ）=σ时，式（6）和式（7）成立。

当ρ=k时，假设已经构建出策略FA，使得式（6）和式（7）成立。根据归纳假设可知，存在一个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（ρ）〉q′）=σA，

F（ρ〈FA（ρ），F（ρ）〉q′）=σ（9）

时，式（6）和式（7）成立。那么由FA的构造方法可知，l≤‖〈〈A〉〉Gφ‖（q）。因此，‖〈〈A〉〉Gφ‖是算子F1的最大后置不动点。

2） 易证算子F2也是单调的。因此，由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的语义解释。那么构造A-策略FA，使得FA（q）=σA，且满足对于任意的σ∈D（q），有FA（q〈σA，σ〉λ′）=F′A（λ′）。因此，由定义3可知，l≤‖〈〈A〉〉φ1Uφ2‖（q）。综上可得，‖〈〈A〉〉φ1Uφ2‖是算子F2的一个前置不动点。

接着令Y是算子F2的一个前置不动点。设l≤‖〈〈A〉〉φ1Uφ2‖（q），由定义3可知，存在一条q-路径λ∈out（q，FA，F）满足存在某个i≥0，使得l≤‖φ2‖（λ［i］），且对于任意的0≤j<i，有l≤‖φ1‖（λ［j］）∧δ（λ［j］，FA（λ［0，j］），F（λ［0，j］））（λ［j+1］）。

设I是i的集合，令k=maxI。当k=0时，由F2的定义知，l≤Y（q）。

设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，FA，F），有q′∈supp（δ（q，FA（λ），F（λ））），满足对于i≤m，

即l≤‖〈〈A〉〉φ1Uφ2‖（q′），那么由归纳假设可知l≤Y（q′）。因此，当k=m+1时，由F2的定义可知，l≤Y（q）。

综上可知，‖〈〈A〉〉φ1Uφ2‖是算子F2的最小不动点。

3.2 模型检验

本节将利用MVATL的不动点特性来解决模型检验问题，该模型检验问题可以定义为：对于一个给定的MVCGS M，一个在M中的状态q和一个MVATL公式φ，计算‖φ‖（q）的值。为了方便讨论，下面给出MVATL公式的长度定义。

令φ是一个MVATL公式，其长度记作φ，归纳定义为

p=1，

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

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

令模型MVCGS M的状态数为Q，智能体数为k=Σ，那么M的规模大小为

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是单调的，当i=0时，

有g0g1。

设i=k时，gigi+1成立。当i=k+1时，由归纳假设知gi-1gi，因此F2（gi-1）F2（gi）。那么由F2（gi-1）=gi以及F2（gi）=gi+1，可得gigi+1。因此，对任意的i≥0，有gigi+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‖

输入： 一个带有状态集合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

下面给出一个重要结论。

定理1 给定一个MVCGS M=（n，Q，Π， π，d，δ）和MVATL公式φ，φ的模型检验问题都可以在O（L·Q·M·φ）时间内解决。

证明 由引理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时，有g1（s0）=0，g1（s1）=DC，g1（s2）=DK。当i=1时，经计算可得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 结语

本文研究了MVATL的模型检验问题，引入MVGCS作为此类开放系统的模型，给出基于此模型的MVATL的语法和语义，扩展了多值模型检验技术的应用范围，使其可以适用于具有不确定和不一致信息的开放系统。研究结果表明，MVATL具有不动点特性。基于此结论，采用不动点迭代算法来解决MVATL的模型检验问题，可以在多项式时间内完成对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结构的子模型修复算法［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］袁红娟， 马艳芳， 潘海玉. 模糊交互时态逻辑的模型检测［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.