发布日期：2025-01-04 16:14 点击次数：181
模型检查(model-checking)作为一种自动化系统验证方法, 已广泛应用于协议、硬件和软件验证[1].它可以将某个实际验证对象转化为数学模型, 利用形式化语言将待验证的问题描述为系统规约, 最后通过模型检查算法来证明系统模型是否满足系统规约.在模型检查研究初期, 主要考虑封闭式系统(closed system).对于这种系统而言, 所有可能的行为包括不确定性都被该系统当前状态决定, 外部环境不影响系统的行为.封闭式系统常采用Kripke结构建模, 采用线性时态逻辑LTL和计算树时态逻辑CTL(computation tree logic)等形式化语言描述系统规约, 对应的模型检查算法也已经被提出和应用[1, 2].
然而, 面向封闭式系统的模型检查方法不适用于开放式系统(open system)的验证.与封闭式系统不同, 开放式系统的行为不仅依赖于系统的当前状态, 同时也依赖于系统与环境的交互, 开放式系统中的不确定性选择往往取决于环境.1996年, Kupferman和Vardi将面向封闭式系统的模型检查方法扩展到了开放式系统[3], 该方法称为模块检查(module-checking).在模块检查框架中, 开放式系统采用一种类似Kripke结构的有限状态系统建模, 称为模块(module), 其状态包括系统状态和环境状态, 分别描述系统本身的状态和环境的状态.一个开放式系统满足一个规约当且仅当无论环境怎么选择, 系统的行为都要满足规约.
近几年, 模型检查已应用于多智能体系统(multi-agents system, 简称MAS)的验证.MAS是一种新型的智能系统设计和开发范式, 由多个自主智能体组成, 其目的是将大而复杂的系统划分为多个简单自主智能体, 彼此互相通信和协调来完成系统功能.MAS已被广泛应用于复杂系统的设计和开发, 如自主航空器控制系统[4].在MAS中, 每个智能体都有局部的状态(local state), 其不确定性通过智能体的策略决定, 全局状态(global state)由所有智能体的局部状态组成, 其行为则由所有智能体共同决定.1997年, Alur等人提出了面向MAS的模型检查方法, 其采用并发博弈结构(concurrent game structure, 简称CGS)进行建模, 提出了交替时态逻辑(alternating-time temporal logic, 简称ATL和ATL*)用于描述系统规约, 设计了相应的模型检查算法[5].ATL和ATL*是经典时态逻辑CTL和CTL*的扩展, 引入了联合模态操作(coalition modalities):《A》φ和[[A]]φ, 其中, A是一个智能体集合. 《A》φ为真当且仅当A中的智能体有一个联合策略, 无论其他智能体如何选择, 目标公式φ都成立; 而[[A]]φ则是《A》φ的对偶形式.在该框架中, 所有智能体都可看到其他智能体所在的局部状态, 同时可以记录所有历史状态. CGS也可以通过解释系统(interpreted system, 简称IS)表达, 其中每个智能体是一个Kripke结构, CGS模型可以通过Mealy型或Moore型同步组合而获得[5].
在实际应用中, MAS可能是一个分布式系统, 每个智能体仅能观察到其自身的局部状态, 而无法知道其他智能体所在的局部状态, 即不完全信息(imperfect information); 或由于资源问题, 智能体无法记录所有历史状态, 即不完全记忆(imperfect recall).为解决这个问题, Schobbens利用CGS模型的语义刻画了智能体的能力, 定义其相应的策略类型[6], 并对ATL和ATL*模型检查问题进行了研究.在不完全记忆场景下, 每个智能体的决策仅依赖于系统的当前状态, 反之依赖于历史状态有限路径; 在不完全信息场景下, 每个智能体在面对其不可区分的全局状态或历史状态有限路径时必须选择一样的策略.以下我们用R表示完全记忆, r表示不完全记忆.类似的, 我们用I表示完全信息, i表示不完全信息.Schobbens指出:在iR场景下, ATL模型检查问题是不可判定的.证明见文献[7].在其他场景下, 模型ATL和ATL*模型检查问题是可判定的, 比如ATL和ATL*模型检查在ir场景下分别可以在PNP和PSPACE时间判定, 详见文献[6].Jamroga等人证明, ATL模型检查问题在ir场景下是PNP-完备的, 并设计实现了一个高效的算法[8, 9].虽然在完全信息时, 是否完全记忆对ATL模型检查没有任何影响, 但是在不完全信息场景下或对ATL*逻辑, 是否完全记忆却具有重要的影响[10].除此之外, 为了描述更多的系统规约, Chatterjee等人提出了LTL逻辑的一阶量词扩展逻辑(strategy logic, 简称SL)[11-13], 在ATL, ATL*或AMC中引入知识操作等[14-18].
虽然这些工作都考虑了智能体的不同能力, 但仍然存在如下问题:考虑《A》φ的语义, 在IR场景下, A中的智能体和不在A中的智能体(用A表示)都具有相同的能力.但是在Ir, iR或ir场景时, 已知工作中仅仅考虑了A中的智能体要符合Ir, iR或ir能力, 而A中的智能体却采用IR策略.这样做的一个好处是:不管在何种场景下, 《∅》φ均可对应到ATL/ATL*中的所有路径量词∀, [[∅]]对应到存在路径量词∃.可见, A和A的智能体拥有不同的能力.但是当联合模态操作出现嵌套时, 例如公式《A》φ包含一个子公式《A′》j′, 且A≠A′时, 某些智能体为了满足公式《A》φ和《A′》j′, 将会具有不同的策略类型, 导致智能体策略类型的不一致性.这种将智能体的能力隐含于公式中的方式既不利于理解, 也不利于应用.
为解决这个问题, 有两种方案:第1种是在MAS中指明智能体所具备的能力; 另一种是在逻辑公式中指明智能体所具备的能力.本文采用第1种方案, 主要出于以下两方面的原因.
1) 智能体的策略类型往往取决于MAS本身, 且不同智能体在同一MAS中具备不同的策略类型, 这类系统称为异构多智能体系统(heterogeneous mutli-agent system).同时, 一个MAS中智能体的策略能力一般不会随着验证规约不同而改变;
2) 第2种方案需要在规约中显示枚举所有智能体, 且在嵌套联合模态操作中容易出现智能体策略类型前后不一致.
基于第1种方法, 本文提出了一种解释系统的扩展, 带类型解释系统(typed interpreted system, 简称TIS), 其中每个智能体被赋予了IR, Ir, iR或ir中的一种策略类型, 代表智能体在系统中的策略能力.在一个TIS中, 智能体可以具备不同策略能力, 因此可以对异构多智能体系统进行建模, 也避免智能体策略类型的不一致性问题.本文根据TIS模型定义了ATL的语义, 并研究其模型检查问题.当TIS系统中的智能体被赋予iR能力, 由于ATL模型检查在iR场景下是不可判定的[7], 这将直接导致此情况下ATL在TIS上的模型检查问题是不可判定的.当TIS中智能体仅被赋予Ir, IR或ir能力, 并且ATL公式中出现的智能体都不是IR策略类型时, ATL模型检查问题是可判定的, 并提出了一种复杂度为EXPTIME算法, 设计实现了基于有序二叉决策图(ordered binary decision diagram, 简称OBDD)的符号化模型检查工具ShTMC, 实验结果证明了ShTMC的可用性.
本文第1节首先介绍相关工作.第2节简介背景知识, 包括解释系统和ATL逻辑等.第3节通过一个示例揭示经典语义的不足.第4节提出带类型解释系统, 研究ATL的语义, 提出模型检查算法.第5节介绍实验结果.第6节总结和展望.
1 相关工作
近几年, ATL/ATL*语义定义已经引起了国内外的关注.在经典ATL/ATL*语义中, 对于公式《A》φ, 当A中智能体选择了某联合策略, 对目标φ进行验证时, 如果遇到其他联合模态操作, 如《A′》φ′或[[A′]]φ′, 所有智能体将忘记之前选择的策略, 然后重新选择新的策略去满足φ′, 即可撤销策略(revocable strategies).这种语义定义方式与博弈论的语义不一致.为此, Agotnes等人提出了不可撤销的语义(irrevocable strategies)[19], 即A中智能体确定了某一种联合策略后, 即使遇到其他联合模态操作, A中智能体还是必须遵照之前选择的策略进行.根据这种语义, Agotnes等人给出了ATL在IR和Ir场景下的模型检查算法.
为了能在规约上对策略进行约束, Pinchinat在Dμ逻辑中引入了决策操作[20], 使得可以在规约中建立谓词和智能体策略间的联系, 并对该逻辑的表达能力进行了研究.
在Agotnes等人工作基础之上[19], Brihaye等人在ATL/ATL*中引入了策略上下文(strategy contexts)和记忆约束(memory constraints)[20-22].策略上下文可以保存智能体选择的策略, 从而解决经典语义中的策略不可撤销性问题, 同时还能指定哪些智能体的策略是可撤销的.而记忆约束则限制了智能体能保存的信息量.在这种语义下, Brihaye等人对Ir和IR场景下的模型检查问题和逻辑表达力进行了分析.
Goranko等人研究了基于博弈论的ATL+的语义, 该语义与经典的语义等价, 并在此基础上提出了一种新的模型检查算法[23].除上述工作之外, 为了平衡逻辑表达能力和模型检查算法复杂度, Wang等人提出了Strategy Logic的两种子类:BSIL逻辑[24]和TCL逻辑[25], 并对这两种逻辑的可满足性和模型检查问题进行了研究.
本文研究的语义跟上述工作都不同, 上述工作都假设在一个MAS中, 智能体的策略类型是一样的或不在模态操作中出现的智能体都采用IR策略类型, 而本文提出的语义却允许在同一MAS中, 各智能体拥有不同的策略类型, 因此, 之前的模型检查算法均不适用于本文研究的语义.另外, 本文的智能体策略类型是通过模型在语法层进行定义, 而非以往工作通过语义定义.
2 背景知识
本节简单回顾Kripke结构, 并发博弈结构, 解释系统和交替时态逻辑ATL.
2.1 Kripke结构
定义1.假定AP为非空原子命题集合, Kripke结构(Kripke structure)是一个四元组:K≜(Q, Q0, δ, L).其中,
● Q是有限状态集合Q0⊆Q;
● Q0⊆Q是初始状态集合;
● δ:Q→2Q是状态迁移函数.
● L:AP→2Q是系统的标签函数, 对于任意状态q和原子命题p, q∈L(p)表示p命题在状态q时为真.
K的路径(path)是一个无限状态序列π=g0g1g2…, 其中, 对任意i≥0, 满足gi+1∈δ(gi).Paths(g)表示所有从状态g出发的路径集合.
2.2 并发博弈结构
并发博弈结构通过引入“智能体行为”这一概念对Kripke模型进行了扩展.对于CGS, 它的系统状态演变取决于系统中所有智能体的并发行为.
定义2.假定AP为非空原子命题集合, CGS是一个多元组:G≜(Q, Q0, Agt, Ac, (~i)i∈Agt, λ, δ, L).其中,
● Q是有限状态集合;
● Q0⊆Q是初始状态集合;
● Agt={1, …, k}为有限非空智能体集合;
● Ac是有限动作集合;
● ~i⊆Q×Q是状态的等价关系, g~ig′表示状态g和g′对于智能体i是不可区分的;
● λ:Q×Agt→2Ac是智能体的动作规范, 对于一个给定状态g, λ(g, i)表示智能体i在状态g时所有可选择的动作集, 且满足λ(g, i)=l(g′, i), 若g~ig′成立;
● δ:Q×AcAgt→Q是状态迁移函数, 满足:对于任意状态g, 动作组〈a1, …, ak〉, 如果δ(g, 〈a1, …, ak〉)有定义, 则ai∈λ(g, i).
● L:AP→2Q是系统的标签函数, 对于任意状态q和原子命题p, q∈L(p)表示p命题在状态q时为真.
G的路径(path)是一个无限状态序列π=g0g1g2…, 其中, 对任意i≥0, 存在动作组αi∈AcAgt, 满足gi+1=δ(gi, αi).给定一条路径π=g0g1g2…, 路径的一个任意前缀称为有限路径.
2.3 解释系统
解释系统是Kripke结构的另一种扩展[16], 相比于CGS更适用于MAS的建模.因为IS的全局状态是由其内部所有智能体的局部状态组成的, 而在CGS中, 系统只有全局状态这一概念, 因此CGS中无法直接观察单个智能体的局部状态迁移关系.当系统不满足规约时, 也无法从反例中具体分析是否某个智能体导致规约不成立, 除非有全局状态到局部状态的映射关系.鉴于IS的这一特性, 本文将以IS为例进行扩展, 但本文提出的思想同样适用于扩展CGS.
定义3.假定Agt={1, …, k}为智能体集合, AP为非空原子命题集合, IS是一个多元组:
$
J\triangleq ({{\langle {{Q}_{i}}, A{{c}_{i}}, {{\lambda }_{i}}, {{\delta }_{i}}, Q_{i}^{0}\rangle }_{i\in Agt}}, L).
$
其中,
● Qi是智能体i的局部状态集合.所有智能体的局部状态集合的积Q1×Qk为系统的全局状态集合, 用Q表示系统的全局状态集合.对于任意一个全局状态g∈Q, g(i)表示在全局状态g中, 智能体i的局部状态;
● Aci是智能体i可选的非空有限动作集.所有智能体动作集合的积Ac=Ac1x…xAck被称为系统的联合动作集.联合动作用α=〈a1, …, ak〉∈Ac1×…×Ack表示, α(i)表示智能体i的动作;
● $ {{\lambda }_{i}}:{{Q}_{i}}\to {{2}^{A{{c}_{i}}}} $是智能体i的动作规范, 给定局部状态q, λi(q)表示智能体i在局部状态q时所有可选择的动作集, 定义λi(g)=λi(g(i)).这表明智能体的行为是受限的, 可选动作与其当前所处的局部状态有关.对于一个给定的全局状态g, 以λ(g)表示集合λ1(g)×…×λk(g);
● δi:Qi×Ac→Qi是智能体i的状态转移函数, 给定局部状态q和联合动作α满足α(i)∈λi(q), δi(q, α)是i在下一时刻的局部状态.定义δ为全局状态迁移关系, 满足δ((q1, …, qk), α)=(δ1(q1, a), …, δk(qk, a));
● $ Q_{i}^{0}\subseteq {{Q}_{i}} $是智能体i的初始状态集合, 本文用Q0表示全局初始状态集合$Q_{1}^{0}\times ...\times Q_{k}^{0} $;
● L:AP→2Q是系统的标签函数, 对于任意的全局状态g和原子命题p, g∈L(p)表示p命题在全局状态g时为真.
从解释系统J, 可以推导出CGS系统(Q, Q0, Agt, Ac′, (~i)i∈Agt, λ′, δ, L), 其中,
● Q, Q0, Agt, δ和L如定义3所述;
● Ac′=Ac1∪…∪Ack;
● λ′定义为λ′(g, i)=λi(g(i));
● ~i定义为:g~ig′当且仅当g(i)=g′(i).
J的路径(path)是无限全局状态序列π=g0g1g2…, 其中, 对任意m≥0, 存在联合动作αm∈Ac, 满足gm+1=δ(gm, αm).给定一条路径π=g0g1g2…和j≥0, 以π(j)表示序列中第j处的全局状态gj, 并用proji(π)代表智能体i在π中的分量, 即局部状态序列g0(i)g1(i)g2(i)….
有限路径τ=g0g1…gn是路径π=g0g1g2…的前缀.给定有限路径τ=g0g1…gn和0≤m≤n, 以τ(m)表示序列中第m处的全局状态gm, lst(τ)是τ的最后一个状态, proji(τ)代表智能体i在τ中的分量, 即局部状态序列g0(i)g1(i)…gn(i).
下文将以Paths表示所有可能的路径集, 以Trks表示所有可能有限路径的集.对于给定的全局状态g, 以Paths(g)和Trks(g)表示所有从g出发的路径和有限路径集合.
2.4 策略
在IS中, 智能体i在某一状态下可能存在多个可以选择的动作, 这种不确定性采用策略(strategy)θi来决定.而策略根据智能体是否可以观察到其他智能体的状态和是否依赖于历史状态有不同的定义方式.本文采用文献[6]的定义方式, 定义4种不同策略类型:IR, Ir, iR和ir, 具体定义如下.
● IR.θi:Trks→Aci:对于任何一个智能体i以及任意一条有限路径τ, 满足θi(τ)∈λi(lst(τ)), 即, 策略函数θi为智能体i定义了从有限路径到可选动作的映射函数;
● Ir.θi:Trks→Aci:对两条有限路径τ1和τ2满足lst(τ1)=lst(τ2), 那么智能体i将选择相同的动作, 即θi(τ1)= θi(τ2).因此, 智能体i选择的动作只依赖系统当前的状态, 不依赖于历史有限路径;
● iR.θi:Trks→Aci:类似于IR策略, 不同的是:对于两条有限路径τ1和τ2, 如果proji(τ1)=proji(τ2), 则θi(τ1)= θi(τ2).直观地讲, iR策略表示智能体i在任何两条无法区分的有限路径上都选择同一个动作;
● ir.θi:Trks→Aci:ir融合了iR和Ir的所有特点, 在ir中, 如果lst(τ1)(i)=lst(τ2)(i), 则θi(τ1)=θi(τ2).即, 智能体i仅能根据当前自身的局部状态来判断选择一个动作.
给定智能体集合A, A表示其补集, A的联合σ-策略就是A中所有智能体的σ-策略构成的集合, 即θA={θi|i∈A}, 其中, σ∈{IR, Ir, iR, ir}, 本文用θA(i)表示智能体i在θA中的策略.
给定智能体集A、全局状态g以及联合σ-策略θA, 以Outσ(g, θA)表示A中的所有智能体严格按照策略θA选择动作, 从初识状态g开始, 系统所有可能路径的集合, 即:对于任意π∈Outσ(g, θA)都有π(0)=g, 以及任意时刻j≥0, 存在联合动作α∈λ(π(j)), 满足π(j+1)=δ(π(j), α)和对于所有智能体i∈A, α(i)=θA(i)(π(0)…π(j))成立.
2.5 交替时态逻辑ATL
交替时态逻辑(alternating-time temporal logic, 简称ATL)是CTL的一种扩展[5], 将存在路径量词∃替换为联合模态操作《A》, 其中, A为一个智能体集合.
定义4. ATL的语法如下:ϕ::=p|¬φ|φ1∨φ2|《A》Xφ|《A》Gφ|《A》φ1Uφ2.其中, A⊆Agt.
定义5.给定解释系统$ J=({{\langle {{Q}_{i}}, A{{c}_{i}}, {{\lambda }_{i}}, {{\delta }_{i}}, Q_{i}^{0}\rangle }_{i\in Agt}}, L) $、全局状态g和ATL公式φ, 公式的可满足性J, g⊨σφ通过如下所示归纳定义.
● J, g⊨σp当且仅当g∈L(p);
● J, g⊨σ¬φ当且仅当J, g⊭σφ;
● J, g⊨σφ1∨φ2当且仅当J, g⊨σφ1或J, g⊨σφ2;
● J, g⊨σ《A》Xφ当且仅当存在一个联合σ-策略θA, 对于所有路径π∈Outσ(g, θA), 都有J, π(1)⊨σφ;
● J, g⊨σ《A》Gφ当且仅当存在一个联合σ-策略θA, 对于所有路径π∈Outσ(g, θA), 在任何时刻j≥0, 都有J, π(j)⊨σφ;
● J, g⊨σ《A》φ1Uφ2当且仅当存在一个联合σ-策略θA, 对于所有路径π∈Outσ(g, θA), 都存在一个时刻j≥0, 使得J, π(j)⊨σφ2成立; 并且对于所有时刻0≤i < j, 都有J, π(i)⊨σφ1成立.
解释系统J满足公式φ当且仅当所有J中的全局初始状态都满足φ.类似的, 可以定义ATL在CGS系统上的语义, 详见文献[5].
给定公式φ, 在某语义下, 所有智能体采用同一个策略类型, 即称为智能体的策略类型是一致的; 反之为不一致的.考虑公式《{1, 2, 3}》(p U《{1, 2}》Xφ), 在IR语义时是一致的; 而在其他语义时, 由于智能体3的策略类型在满足p U《{1, 2}》Xφ和φ时可能会不同, 因此是不一致的.
计算树逻辑是ATL逻辑的一种特殊子类, 其中, 所有《A》φ公式中的A必须是空集∅, 即, 《∅》表示所有路径量词.CTL在Kripke结构的语义见文献[1].
定理1.给定IS系统$ J=({{\langle {{Q}_{i}}, A{{c}_{i}}, {{\lambda }_{i}}, {{\delta }_{i}}, Q_{i}^{0}\rangle }_{i\in Agt}}, L)$、全局状态g和ATL公式φ, 以下结论成立.
(1) J, g⊨iRφ问题是不可判定的;
(2) J, g⊨IRφ和J, g⊨Irφ问题是PTIME-完备的[5, 10].
(3) J, g⊨IRφ当且仅当J, g⊨Irφ[10].
(4) J, g⊨irφ问题是PNP-完备的[6, 8].
证明:Dima and Tiplea证明了ATL在CGS上的模型检查问题在iR场景下是不可判定的[7], 其将图灵机停机问题规约到一个仅包含3个智能体的CGS系统G满足ATL公式《{1, 2}》G ok的问题.因此只需要将该CGS系统转化到一个IS系统J, 使得J, g⊨iR《{1, 2}》G ok当且仅当G中的状态g在iR场景满足《{1, 2}》G ok.
考虑CGS系统G=(Q, Q0, Agt, Ac, (~i)i∈Agt, λ, δ, L), 对于任意智能体i, 假设${{Q}_{i}}=\{Q_{i}^{1}, ..., Q_{i}^{{{n}_{i}}}\} $为关系~i在Q上的等价类集, 以|g|i表示状态g在Qi中的等价类.对于公式《{1, 2}》G ok而言, 智能体3的等价类Q3不影响其可满足性, 因此~3可以替换为最小等价关系, 即g~3g′当且仅当g=g′.本文假设~3为最小等价关系.
给定状态g和动作组α=〈a1, a2, a3〉, 以αg表示动作组α=〈a1, a2, (a3, g)〉.
定义IS系统$ J=({{\langle {{Q}_{i}}, A{{c}_{i}}, {{\lambda }_{i}}, {{\delta }_{i}}, Q_{i}^{0}\rangle }_{i\in Agt}}, L) $, 其中,
● Ac1=Ac2=Ac, Ac3=Ac×Q;
● 对于任意的i, δi(|g|i, αg)=|g′|i当且仅当δ(g, α)=g′;
● λi(|g′|i)={αg|α∈λ(g, i), g∈|g′|i};
● $ Q_{i}^{0}=\{|g{{|}_{i}}|g\in Q\} $.
对于公式《{1, 2}》G ok, 只有智能体1和智能体2需要考虑联合iR-策略, 而智能体3是采用IR-策略.根据ATL语义, J, g⊨iR《{1, 2}》G ok当且仅当G的状态g在iR场景满足《{1, 2}》G ok.
2.6 示例
考虑系统模型$ J=({{\langle {{Q}_{i}}, A{{c}_{i}}, {{\lambda }_{i}}, {{\delta }_{i}}, Q_{i}^{0}\rangle }_{i\in Agt}}, L) $, 其中,
● Agt={A, B};
● QA={A1, A2}, QB={B1, B2, B3};
● AcA={a1, a2}, AcB={b1, b2};
● δA和δB如图 1所示, 节点表示局部状态, 边表示状态迁移关系, 边上的标识是智能体的联合动作;
Fig. 1 Local transition graphs of A and B
图 1 智能体A和智能体B的局部状态转移图
● λA={A1:{a1, a2}, A2:{a2}}, λB={B1:{b1}, B2:{b1, b2}, B3:{b1}};
● $ Q_{A}^{0}=\{{{A}_{1}}\}, Q_{B}^{0}=\{{{B}_{1}}\} $;
● L(eva)={(A2, B2)}.
示例的全局状态转移关系如图 2所示.
Fig. 2 Transitionrelation of system
图 2 全局状态迁移关系
考虑ATL公式:φ=《{B}》True U eva.不难发现,
● 若智能体A在状态(A1, B1)时选择动作a1, 系统将进入状态(A1, B2);
● 在状态(A1, B2)时, 如果B选择动作b1, A选择动作a1; 如果B选择动作b2, A选择动作a2, 系统将进入状态(A1, B3); 若A继续选择动作a1, 系统重回状态(A1, B1).
如此反复, 系统将永远不会到达状态(A2, B2).因此, 对于任意的σ∈{IR, Ir, iR, ir}, J, (A1, B1)⊨σφ都不成立.
但是在实际应用中, 比如在无线传感器网络中, 每个节点是一个智能体, 其存储资源非常有限; 同时, 为了降低能耗, 不可能时刻跟其他智能体保持通信来获取其他智能体的局部状态.因此在上述例子中, 如果将A的策略类型限制为ir, 在状态(A1, B2)时, A只能选择动作a1; 如果B选择动作b2, 系统最终将到达(A2, B2).因此, 智能体的策略类型对公式可满足性的结果有直接的影响.而在经典的语义下, 无法对此类规约进行描述和验证; 同时, CGS和IS都无法对这类异构多智能体系统建模.针对这个问题, 本文将在解释系统中引入智能体策略类型函数来描述智能体的策略类型, 从而验证上述类型的规约.
3 基于策略类型的解释系统
通过讨论可知, 传统的多智能体系统验证框架在语义表述方面仍然存在不足.因此提出基于策略类型的解释系统, 为每个智能体引入专属的策略类型.
3.1 TIS模型
定义6.基于策略类型的解释系统(typed interpreted system, 简称TIS)是二元组:T≜(J, Λ), 其中,
● $ J=({{\langle {{Q}_{i}}, A{{c}_{i}}, {{\lambda }_{i}}, {{\delta }_{i}}, Q_{i}^{0}\rangle }_{i\in Agt}}, L) $是一个解释系统;
● Λ:Agt→{IR, Ir, iR, ir}是一个映射函数, 为每个智能体关联一种策略类型.
TIS依旧沿用传统解释系统中对路径和有限路径的定义, 但是需要重新定义策略.与已有工作通过语义来定义智能体的策略不同, 在TIS模型中, 智能体的策略类型由TIS模型给出, 如, Λ(i)表示智能体i只能采用Λ(i)-策略.
给定一个智能体集合A, A的联合策略就是A中所有智能体的策略构成的集合, 即:
θA≜{θi|i∈A, θi是Λ(i)-策略}.
本文用θA(i)表示智能体i在θA中的策略, 以SA表示A所有可能的联合策略集合.已知智能体集合A和初始状态g, 两个联合策略θA和$ {{\theta }_{{\bar{A}}}} $唯一地确定了一条路径$ Path({{\theta }_{A}}, {{\theta }_{{\bar{A}}}})\triangleq \pi $, 满足π(0)=g, 以及任意一个时刻j, 都存在联合动作α∈λ(π(j)), 使得π(j+1)=δ(π(j), α), 其中:对于任意i∈A, α(i)=θA(i)(π(0)…π(j)); 对于任意$ i\in \bar{A}, \alpha (i)={{\theta }_{{\bar{A}}}}(i) $(π(0)…π(j)).给定智能体集合A、初始状态g、一个联合策略θA, 定义:
$
Out(g, {{\theta }_{A}})\triangleq \bigcup\nolimits_{{{\theta }_{{\bar{A}}}}\in {{S}_{{\bar{A}}}}}{Path({{\theta }_{A}}, {{\theta }_{{\bar{A}}}})}.
$
事实1.给定TIS T=(J, L)和智能体集合A, 对于任意σ∈{IR, Ir, iR, ir}, 如果所有i∈A, Λ(i)=σ, 则以下结论成立.
1)
θA是J中A的一个联合σ-策略当且仅当θA是T中A的联合策略;
2) 对于T中A的任意一个联合策略θA, Out(g, θA)⊆Outσ(g, θA);
3) 当所有$ i\in \bar{A} $满足Λ(i)=IR时, 对于任意一个T中A的联合策略θA, Out(g, θA)≡Outσ(g, θA).
证明:根据联合σ-策略和联合策略的定义, 结论1)显而易见.
Out(g, θA)⊆Outσ(g, θA):对于任意路径π∈Out(g, θA), 证明π∈Outσ(g, θA)成立即可.假设一条路径π=g0g1…, 其中, g0=g, 即:对于智能体集$ \bar{A} $, 始终存在联合策略$ {{\theta }_{{\bar{A}}}}=\{{{\theta }_{i}}|i\in \bar{A}\}\in {{S}_{{\bar{A}}}} $, 任意时刻m≥0, gm+1=δ(gm, αm)成立.其中, αm是所有智能体的联合动作, 即:对于智能体i∈A, 有αm(i)=θA(i)(g0…gm)成立; 对于智能体$i\in \bar{A} $, 有$ {{\alpha }_{m}}(i)={{\theta }_{{\bar{A}}}}(i) $(g0…gm)成立.显然, 通过以上方法找到的路径, 一定存在于Outσ(g, θA)中.因此, 结论2)成立.
Out(g, θA)⊇Outσ(g, θA):证明对于任意路径π∈Outσ(g, θA), 都有π∈Out(g, θA)成立.设有条路径π=g0g1…, 其中, g0=g, 且在任意m≥0, gm+1=δ(gm, αm)成立; 同时, 对于智能体$ i\in A, {{\alpha }_{m}}(i)={{\theta }_{{\bar{A}}}}(i)({{g}_{0}}...{{g}_{m}}) $成立.此时, 在任意m≥0, 智能体$ i\in \bar{A} $, 我们令$ {{\theta }_{{\bar{A}}}}(i)({{g}_{0}}...{{g}_{m}})={{\alpha }_{m}}(i) $.对于智能体$ i\in \bar{A} $, 由于Λ(i)=IR, 则有$ {{\theta }_{{\bar{A}}}}\in {{S}_{{\bar{A}}}} $, 使得π∈Out(g, θA)成立.综上, 结论3)成立.
定义7.给定一个TIS T、全局状态g和ATL公式φ, 则可满足性T, g⊨φ通过如下归纳定义.
● T, g⊨p当且仅当g∈L(p);
● T, g⊨¬φ当且仅当T, g⊭¬φ;
● T, g⊨φ1∨φ2当且仅当T, g⊨φ1或T, g⊨φ2;
● T, g⊨《A》Xφ当且仅当存在联合策略θA, 对于任意路径π∈Out(g, θA), 都有T, π(1)⊨φ;
● T, g⊨《A》Gφ当且仅当存在联合策略θA, 对于任意路径π∈Out(g, θA), 在任何时刻j≥0, 都有T, π(j)⊨φ;
● T, g⊨《A》φ1Uφ2当且仅当存在联合策略θA, 对于所有路径π∈Out(g, θA), 都存在一个时刻j≥0, 使得T, π(j)⊨φ2成立, 并且对于所有时刻0≤i < j, 都有T, π(i)⊨φ1.
定理2. ATL在TIS上的模型检查问题是不可判定的.
证明:根据定理1的证明, 可以把图灵机停机问题规约到一个IS J是否满足《{1, 2}》G ok的问题上.而从J模型可以构造成TIS系统T=(J, Λ), 其中, Λ满足Λ(1)=Λ(2)=ir, Λ(3)=IR, 从而将图灵机停机问题规约到ATL在TIS模型检查问题.
由于定理2, 只需要考虑TIS系统T=(J, Λ)满足Λ:Agt→{IR, Ir, ir}的模型检查问题.本文研究满足L:Agt→{IR, Ir, ir}的TIS模型检查问题, 但是ATL公式中出现的智能体必须是Ir或ir类型, 即, 所有ATL公式中出现的《A》φ公式满足:如果i∈A, 则Λ(i)∈{Ir, ir}.对于一般情况, 目前作者还没有解决方案, 留待未来解决.
3.2 模型检查算法
对于任何一个智能体, 如果其策略类型为Ir或ir, 那么其策略数量是有限的.因此, 可以通过不确定地猜测每个智能体的策略, 然后再验证猜测是否正确.给定TIS系统T和ATL公式φ, 并且公式φ中出现的智能体是Ir或ir类型,
