模型检查(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场景下分别可以在P^NP和PSPACE时间判定, 详见文献[6].Jamroga等人证明, ATL模型检查问题在ir场景下是P^NP-完备的, 并设计实现了一个高效的算法^{[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, Q₀, δ, L).其中,

●  Q是有限状态集合Q₀⊆Q;

●  Q₀⊆Q是初始状态集合;

●  δ:Q→2^Q是状态迁移函数.

●  L:AP→2^Q是系统的标签函数, 对于任意状态q和原子命题p, q∈L(p)表示p命题在状态q时为真.

K的路径(path)是一个无限状态序列π=g₀g₁g₂…, 其中, 对任意i≥0, 满足g_i+1∈δ(g_i).Paths(g)表示所有从状态g出发的路径集合.

2.2 并发博弈结构

并发博弈结构通过引入“智能体行为”这一概念对Kripke模型进行了扩展.对于CGS, 它的系统状态演变取决于系统中所有智能体的并发行为.

定义2.假定AP为非空原子命题集合, CGS是一个多元组:G≜(Q, Q₀, Agt, Ac, (~_i)_i∈Agt, λ, δ, L).其中,

●  Q是有限状态集合;

●  Q₀⊆Q是初始状态集合;

●  Agt={1, …, k}为有限非空智能体集合;

●  Ac是有限动作集合;

●  ~_i⊆Q×Q是状态的等价关系, g~_ig′表示状态g和g′对于智能体i是不可区分的;

●  λ:Q×Agt→2^Ac是智能体的动作规范, 对于一个给定状态g, λ(g, i)表示智能体i在状态g时所有可选择的动作集, 且满足λ(g, i)=l(g′, i), 若g~_ig′成立;

●  δ:Q×Ac^Agt→Q是状态迁移函数, 满足:对于任意状态g, 动作组〈a₁, …, a_k〉, 如果δ(g, 〈a₁, …, a_k〉)有定义, 则a_i∈λ(g, i).

●  L:AP→2^Q是系统的标签函数, 对于任意状态q和原子命题p, q∈L(p)表示p命题在状态q时为真.

G的路径(path)是一个无限状态序列π=g₀g₁g₂…, 其中, 对任意i≥0, 存在动作组α_i∈Ac^Agt, 满足g_i+1=δ(g_i, α_i).给定一条路径π=g₀g₁g₂…, 路径的一个任意前缀称为有限路径.

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). $

其中,

●  Q_i是智能体i的局部状态集合.所有智能体的局部状态集合的积Q₁×Q_k为系统的全局状态集合, 用Q表示系统的全局状态集合.对于任意一个全局状态g∈Q, g(i)表示在全局状态g中, 智能体i的局部状态;

●  Ac_i是智能体i可选的非空有限动作集.所有智能体动作集合的积Ac=Ac₁x…xAc_k被称为系统的联合动作集.联合动作用α=〈a₁, …, a_k〉∈Ac₁×…×Ac_k表示, α(i)表示智能体i的动作;

●  $ {{\lambda }_{i}}:{{Q}_{i}}\to {{2}^{A{{c}_{i}}}} $是智能体i的动作规范, 给定局部状态q, λ_i(q)表示智能体i在局部状态q时所有可选择的动作集, 定义λ_i(g)=λ_i(g(i)).这表明智能体的行为是受限的, 可选动作与其当前所处的局部状态有关.对于一个给定的全局状态g, 以λ(g)表示集合λ₁(g)×…×λ_k(g);

●  δ_i:Q_i×Ac→Q_i是智能体i的状态转移函数, 给定局部状态q和联合动作α满足α(i)∈λ_i(q), δ_i(q, α)是i在下一时刻的局部状态.定义δ为全局状态迁移关系, 满足δ((q₁, …, q_k), α)=(δ₁(q₁, a), …, δ_k(q_k, a));

●  $ Q_{i}^{0}\subseteq {{Q}_{i}} $是智能体i的初始状态集合, 本文用Q₀表示全局初始状态集合$Q_{1}^{0}\times ...\times Q_{k}^{0} $;

●  L:AP→2^Q是系统的标签函数, 对于任意的全局状态g和原子命题p, g∈L(p)表示p命题在全局状态g时为真.

从解释系统J, 可以推导出CGS系统(Q, Q₀, Agt, Ac′, (~_i)_i∈Agt, λ′, δ, L), 其中,

●  Q, Q₀, Agt, δ和L如定义3所述;

●  Ac′=Ac₁∪…∪Ac_k;

●  λ′定义为λ′(g, i)=λ_i(g(i));

●  ~_i定义为:g~_ig′当且仅当g(i)=g′(i).

J的路径(path)是无限全局状态序列π=g₀g₁g₂…, 其中, 对任意m≥0, 存在联合动作α_m∈Ac, 满足g_m+1=δ(g_m, α_m).给定一条路径π=g₀g₁g₂…和j≥0, 以π(j)表示序列中第j处的全局状态g_j, 并用proj_i(π)代表智能体i在π中的分量, 即局部状态序列g₀(i)g₁(i)g₂(i)….

有限路径τ=g₀g₁…g_n是路径π=g₀g₁g₂…的前缀.给定有限路径τ=g₀g₁…g_n和0≤m≤n, 以τ(m)表示序列中第m处的全局状态g_m, lst(τ)是τ的最后一个状态, proj_i(τ)代表智能体i在τ中的分量, 即局部状态序列g₀(i)g₁(i)…g_n(i).

下文将以Paths表示所有可能的路径集, 以Trks表示所有可能有限路径的集.对于给定的全局状态g, 以Paths(g)和Trks(g)表示所有从g出发的路径和有限路径集合.

2.4 策略

在IS中, 智能体i在某一状态下可能存在多个可以选择的动作, 这种不确定性采用策略(strategy)θ_i来决定.而策略根据智能体是否可以观察到其他智能体的状态和是否依赖于历史状态有不同的定义方式.本文采用文献[6]的定义方式, 定义4种不同策略类型:IR, Ir, iR和ir, 具体定义如下.

●  IR.θ_i:Trks→Ac_i:对于任何一个智能体i以及任意一条有限路径τ, 满足θ_i(τ)∈λ_i(lst(τ)), 即, 策略函数θ_i为智能体i定义了从有限路径到可选动作的映射函数;

●  Ir.θ_i:Trks→Ac_i:对两条有限路径τ₁和τ₂满足lst(τ₁)=lst(τ₂), 那么智能体i将选择相同的动作, 即θ_i(τ₁)= θ_i(τ₂).因此, 智能体i选择的动作只依赖系统当前的状态, 不依赖于历史有限路径;

●  iR.θ_i:Trks→Ac_i:类似于IR策略, 不同的是:对于两条有限路径τ₁和τ₂, 如果proj_i(τ₁)=proj_i(τ₂), 则θ_i(τ₁)= θ_i(τ₂).直观地讲, iR策略表示智能体i在任何两条无法区分的有限路径上都选择同一个动作;

●  ir.θ_i:Trks→Ac_i:ir融合了iR和Ir的所有特点, 在ir中, 如果lst(τ₁)(i)=lst(τ₂)(i), 则θ_i(τ₁)=θ_i(τ₂).即, 智能体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|¬φ|φ₁∨φ₂|《A》Xφ|《A》Gφ|《A》φ₁Uφ₂.其中, 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⊨_σφ₁∨φ₂当且仅当J, g⊨_σφ₁或J, g⊨_σφ₂;

●  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》φ₁Uφ₂当且仅当存在一个联合σ-策略θ_A, 对于所有路径π∈Out_σ(g, θ_A), 都存在一个时刻j≥0, 使得J, π(j)⊨_σφ₂成立; 并且对于所有时刻0≤i < j, 都有J, π(i)⊨_σφ₁成立.

解释系统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φ问题是P^NP-完备的^{[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, Q₀, Agt, Ac, (~_i)_i∈Agt, λ, δ, L), 对于任意智能体i, 假设${{Q}_{i}}=\{Q_{i}^{1}, ..., Q_{i}^{{{n}_{i}}}\} $为关系~_i在Q上的等价类集, 以|g|_i表示状态g在Q_i中的等价类.对于公式《{1, 2}》G ok而言, 智能体3的等价类Q₃不影响其可满足性, 因此~₃可以替换为最小等价关系, 即g~₃g′当且仅当g=g′.本文假设~₃为最小等价关系.

给定状态g和动作组α=〈a₁, a₂, a₃〉, 以α_g表示动作组α=〈a₁, a₂, (a₃, g)〉.

定义IS系统$ J=({{\langle {{Q}_{i}}, A{{c}_{i}}, {{\lambda }_{i}}, {{\delta }_{i}}, Q_{i}^{0}\rangle }_{i\in Agt}}, L) $, 其中,

●  Ac₁=Ac₂=Ac, Ac₃=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};

●  Q_A={A₁, A₂}, Q_B={B₁, B₂, B₃};

●  Ac_A={a₁, a₂}, Ac_B={b₁, b₂};

●  δ_A和δ_B如图 1所示, 节点表示局部状态, 边表示状态迁移关系, 边上的标识是智能体的联合动作;

●  λ_A={A₁:{a₁, a₂}, A₂:{a₂}}, λ_B={B₁:{b₁}, B₂:{b₁, b₂}, B₃:{b₁}};

●  $ Q_{A}^{0}=\{{{A}_{1}}\}, Q_{B}^{0}=\{{{B}_{1}}\} $;

●  L(eva)={(A₂, B₂)}.

示例的全局状态转移关系如图 2所示.

考虑ATL公式:φ=《{B}》True U eva.不难发现,

●  若智能体A在状态(A₁, B₁)时选择动作a₁, 系统将进入状态(A₁, B₂);

●  在状态(A₁, B₂)时, 如果B选择动作b₁, A选择动作a₁; 如果B选择动作b₂, A选择动作a₂, 系统将进入状态(A₁, B₃); 若A继续选择动作a₁, 系统重回状态(A₁, B₁).

如此反复, 系统将永远不会到达状态(A₂, B₂).因此, 对于任意的σ∈{IR, Ir, iR, ir}, J, (A₁, B₁)⊨_σφ都不成立.

但是在实际应用中, 比如在无线传感器网络中, 每个节点是一个智能体, 其存储资源非常有限; 同时, 为了降低能耗, 不可能时刻跟其他智能体保持通信来获取其他智能体的局部状态.因此在上述例子中, 如果将A的策略类型限制为ir, 在状态(A₁, B₂)时, A只能选择动作a₁; 如果B选择动作b₂, 系统最终将到达(A₂, B₂).因此, 智能体的策略类型对公式可满足性的结果有直接的影响.而在经典的语义下, 无法对此类规约进行描述和验证; 同时, 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中的策略, 以S_A表示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)成立即可.假设一条路径π=g₀g₁…, 其中, g₀=g, 即:对于智能体集$ \bar{A} $, 始终存在联合策略$ {{\theta }_{{\bar{A}}}}=\{{{\theta }_{i}}|i\in \bar{A}\}\in {{S}_{{\bar{A}}}} $, 任意时刻m≥0, g_m+1=δ(g_m, α_m)成立.其中, α_m是所有智能体的联合动作, 即:对于智能体i∈A, 有α_m(i)=θ_A(i)(g₀…g_m)成立; 对于智能体$i\in \bar{A} $, 有$ {{\alpha }_{m}}(i)={{\theta }_{{\bar{A}}}}(i) $(g₀…g_m)成立.显然, 通过以上方法找到的路径, 一定存在于Out_σ(g, θ_A)中.因此, 结论2)成立.

Out(g, θ_A)⊇Out_σ(g, θ_A):证明对于任意路径π∈Out_σ(g, θ_A), 都有π∈Out(g, θ_A)成立.设有条路径π=g₀g₁…, 其中, g₀=g, 且在任意m≥0, g_m+1=δ(g_m, α_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⊨φ₁∨φ₂当且仅当T, g⊨φ₁或T, g⊨φ₂;

●  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》φ₁Uφ₂当且仅当存在联合策略θ_A, 对于所有路径π∈Out(g, θ_A), 都存在一个时刻j≥0, 使得T, π(j)⊨φ₂成立, 并且对于所有时刻0≤i < j, 都有T, π(i)⊨φ₁.

定理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类型, ||φ||_T表示所有满足公式φ的状态集合.在给出具体算法前, 先引入一些基本定义.

给定智能体集合A和策略类型函数Λ:Agt→{IR, Ir, ir}, $ A_{r}^{\mathit{\Lambda} } $表示智能体集合A的子集并满足:$ i\in A_{r}^{\mathit{\Lambda} } $当且仅当Λ(i)∈{Ir, ir}.$ F_{A}^{\mathit{\Lambda} } $表示$ f:A_{r}^{\mathit{\Lambda} }\times Q\to Ac $函数集合并满足:对任意$ i\in A_{r}^{\mathit{\Lambda} } $, 任意状态g∈Q.

1) f(i, g)∈λ_i(g(i));

2) 如果Λ(i)=ir, 则对任意状态g′∈Q, 若g(i)=g′(i)成立, 则f(i, g)=f(i, g′).

给定两个函数$ f\in F_{A}^{\mathit{\Lambda} }, \bar{f}\in F_{{\bar{A}}}^{\mathit{\Lambda} } $和TIS系统T, $ T(f, \bar{f}) $表示一个Kripke结构(Q, Q₀, δ′, L), 其中, δ′定义为q′∈δ′(q)当且仅当$ q=({{q}_{1}}, ..., {{q}_{k}}), {q}'=({{{q}'}_{1}}, ..., {{{q}'}_{k}}) $, 存在一个联合动作α∈Ac, 满足如下条件.

1) δ(q, α)=q′;

2) 对任意i∈Agt, 如果$i\in A_{r}^{\mathit{\Lambda} } $, 则f(i, q)=a(i); 如果$ i\in \bar{A}_{r}^{\mathit{\Lambda} } $, 则$ \bar{f}(i, q)=\alpha (i) $.

||φ||_T计算方法见算法1, 其中假设:对于一个给定的Kripke结构和CTL公式φ, MC(K, φ)返回满足公式φ的状态集合, 该问题可以在多项式时间内解决^[1].具体来说, 输入一个ATL公式φ和一个TIS系统T, 通过公式的结构归纳法计算满足子公式的状态集合.第2行~第5行显而易见, 难点在公式φ=《A》φ′.由于φ′中可能有嵌套形如ϕ=《A′》φ″的子公式, 对于这种情况, 采用递归调用, 先计算满足这些公式的状态集, 然后把这些公式替换为一些新的原子命题, 并更新L函数(第7行~第10行).根据假设, 对任意i∈A, Λ(i)∈{Ir, ir}成立, 因此, A中智能体的策略数量是有限的, 可以通过枚举法验证每一条可能的策略.对每种A中智能体策略的策略组合$f\in F_{A}^{\mathit{\Lambda} } $, 考虑所有A的策略.对于A策略类型为Ir或ir智能体, 同理枚举所有可能的策略组合.而策略类型为IR的策略数量是无限的, 无法通过枚举进行处理.因此, 将问题规约到CTL在Kripke结构上的模型检查问题.其主要思想为:g∈ ||《A》ϕ′||_T当且仅当存在一个联合策略θ_A(等价于第12行的f), 任意路径π∈Out(g, θ_A)都满足ϕ′.即:当且仅当存在一个联合策略θ_A, 对任意联合策略$ {{\theta }_{\bar{A}_{r}^{\mathit{\Lambda} }}}$(等价于第13行的$ \bar{f} $), 任意路径$ \pi \in Out(g, {{\theta }_{A}}\oplus {{\theta }_{\bar{A}_{r}^{\mathit{\Lambda} }}}) $都满足ϕ′, 其中$ {{\theta }_{A}}\oplus {{\theta }_{\bar{A}_{r}^{\mathit{\Lambda} }}} $是一个联合策略, 满足:对于任意i∈Agt, 任意状态g∈Q.

$ \left\{ \begin{array}{*{35}{l}} ({{\theta }_{A}}\oplus {{\theta }_{\bar{A}_{r}^{\mathit{\Lambda} }}})(i)(g)={{\theta }_{A}}(i)(g), \text{ if }i\in A \\ ({{\theta }_{A}}\oplus {{\theta }_{\bar{A}_{r}^{\mathit{\Lambda} }}})(i)(g)={{\theta }_{\bar{A}_{r}^{\mathit{\Lambda} }}}(i)(g), \text{ if }i\in \bar{A}_{r}^{\mathit{\Lambda} } \\ \end{array} \right.. $

算法1.模型检查算法.

输入:ATL公式φ, TIS系统$ T=(({{\langle {{Q}_{i}}, A{{c}_{i}}, {{\lambda }_{i}}, {{\delta }_{i}}, Q_{i}^{0}\rangle }_{i\in Agt}}, L), \mathit{\Lambda} ); $

输出:||φ||_T.

MC(T, φ)

1.  begin

2.  switch φ do

3.       case φ=p: return L(p);

4.       case φ=¬φ′: return Q/MC(T, φ′);

5.       case φ=φ₁∨φ₂: return MC(T, φ₁)∪MC(T, φ₂);

6.       case φ=《A》φ′:

7.      for each subformula ϕ=《A′》φ in φ′ do

8.          Replace ϕ by a fresh atomic proposition p_ϕ in φ

9.          Let L(p_ϕ)=MC(T, j);

10.       end for

11.      S:=∅;

12.      for each $ f\in F_{A}^{\mathit{\Lambda} } $ do

13.                 $ S:=S\cup \left( \bigcap\nolimits_{_{\bar{f}\notin F_{{\bar{A}}}^{\mathit{\Lambda} }}}{MC(T(f, \bar{f}), \langle \langle \varnothing \rangle \rangle {\phi }')} \right) $;

14.      end for

15.      return S;

16.    end switch

17.     end

根据$ T(f, \bar{f}) $的定义可见:对于任意g, $ T(f, \bar{f}) $中的Paths(g)等价于$ Out(g, {{\theta }_{A}}\oplus {{\theta }_{\bar{A}_{r}^{\mathit{\Lambda} }}}). $

定理3.给定一个TIS T=(J, L)满足Λ:Agt→{IR, Ir, ir}时, 对于所有ATL公式, 其中出现的智能体i的策略类型Λ(i)∈{Ir, ir}满足时, 模型检查问题可在EXPTIME内判断.

证明:正确性通过ATL结构归纳方法证明.对于p, ¬ϕ′和φ₁∨φ₂, 结论显然成立, 因此仅需要考虑《A》ϕ′.由于A中的智能体采用ir或Ir策略, 因此, $ F_{A}^{\mathit{\Lambda} } $中的函数一一对应到S_A中的联合策略θ_A; 同理, $ F_{A}^{\mathit{\Lambda} } $中的函数一一对应到$ {{S}_{{\bar{A}}}} $中的联合策略$ {{\theta }_{{\bar{A}}}} $.在$ T(f, \bar{f})$中Paths(g)与T中在给定θ_A和$ {{\theta }_{{\bar{A}}}}$时所有从g出发的路径$ Out(g, {{\theta }_{A}}\oplus {{\theta }_{\bar{A}_{r}^{\mathit{\Lambda} }}}) $等价.

$ g\in \bigcap\nolimits_{\bar{f}\notin F_{{\bar{A}}}^{\mathit{\Lambda} }}{MC(T(f, \bar{f}), \langle \langle \varnothing \rangle \rangle {\phi }')} $当且仅当所有π∈Out(g, θ_A)满足公式ϕ′.因此正确性成立.

复杂度:CTL在Kripke结构上的模型检查问题可在多项式时间内解决, 算法1中的第6行~第14行内需要考虑两个递归, 而$ F_{A}^{\mathit{\Lambda} } $和$ F_{{\bar{A}}}^{\mathit{\Lambda} } $中函数数量最多为|Ac|^Q×|Agt|, 因此, 算法1可以在EXPTIME内终止.

备注1.该模型检查算法同样适用于ATL*逻辑, 只需要对MC(K, φ)调用CTL*在Kripke结构的模型检查算法即可.不仅如此, 该算法也可以很容易地扩展“知识”操作, 如, K_iφ表示智能体i知道φ为真.

4 ShTMC模型检查工具及实验

根据算法1, 本文在开源软件MCMAS^{[26, 27]}基础上设计实现了基于OBDD的符号化模型检查工具ShTMC.MCMAS采用解释系统编程语言(interpreted systems programming language, 简称ISPL)描述多个智能体的状态转移, 支持多种包括CTL, ATL逻辑的基于OBDD的符号化模型检查.为便于系统建模, MCMAS中可以定义一种特殊的智能体, 叫环境(environment).环境中定义的状态信息可以全部或部分被其他智能体观察到, 这样可以减少智能体间的同步和通信.本文在ISPL语言中增加智能体策略类型描述语法用于TIS建模, 同时继承了环境智能体这一特性.

为了验证本文所提出方法的性能, 以匿名协议——DCP(dining cryptographers protocol)及其变种为例, 在Cygwin平台上进行实验.DCP是一个基于数学不可解特性的基础安全匿名通信协议, 其主要特点是通过提供匿名信息服务来避免恶意攻击.具体描述如下:该协议中有k个密码员一起就餐, 餐费是匿名者支付的, 可能是其中一个密码员付的餐费, 或者是他们的雇主付的餐费.密码员之间尊重彼此支付餐费的隐私, 但是他们希望知道是不是雇主付了餐费.为解决这个问题, 他们制定了如下的协议:每个人都抛掷一个质地均匀的硬币, 抛掷结果能且仅能被自己和坐在自己右边的人知晓.然后, 每个人同时大声告知所有人, 自己抛掷的硬币和坐在自己左边的人抛掷的硬币正反面是否一致.如果某个密码员就是匿名支付者, 那么他所告知的硬币正反面是否一致的这个信息的就要和他亲眼看到的事实相反(即两个硬币正反面一致就要说成不一致; 正反面不一致就要说成一致).此时, 如果有奇数个人声明“硬币正反面不一致”, 那么这次晚餐是由其中一个密码员支付的, 但这位匿名密码员谁, 其他密码员是不清楚的; 反之, 如果声明“硬币正反名不一致”的人数是偶数, 那么这次餐费则是由他们的雇主支付的.

在这个例子中, 每个密码员可以建模为一个智能体, 其局部状态信息包括该密码员是否支付餐费(即:paid, not-paid)和是否看到硬币正反面一致(即:see-equal, see-different和初始值empty), 其是否声明看到币正反面一致则用动作刻画(即:say-equal, say-different和初始值none).因此, 密码员的局部状态数量为6个.另外有一个环境智能体用于建模每个密码员硬币投掷的正反面(即0和1)情况, 其局部状态数量为8个.全局状态数量为8×6^k.但在这个系统中并不是所有全局状态都可达, 比如在k=3时, 可达的全局状态数量只有96个.

针对DCP模型, 本文验证了ATL公式:〈agent1〉F(odd→(agent1paid or agent2paid or agent3paid)).该公式是为分析ShTMC工具的性能随意构造的, 其中, agent1代表密码员1, agent1paid表示密码员1支付了餐费, agent2paid和agent3paid类似.Odd表示有奇数个人声明“硬币正反面不一致”.

表 1展示了ShTMC模型检查工具对DCP系统的验证结果, 其中, 第1列给出了密码员数量, m(n)表示一共有m个密码员, 其前n个密码员是ir策略类型, 其他则是IR策略类型, 环境智能体也采用IR策略类型; 第2列给出了系统中可达状态数量; 第3列是BDD中布尔变量数; 第4列给出了执行时间, -表示时间超过40分钟; 第5列给出了BDD所使用的内存.BDD变量顺序按照MCMAS默认排序.

从表 1可见:在密码员数量为m时, 如果所有密码员都采用ir策略(即n=m), 那么可达状态数量会比m > n > 0时少.这是因为当所有智能体都是ir策略时, 智能体将无法区分全局状态故而只能选择同一个动作, 并导致了系统中的某些状态不可达.当有一个或多个智能体不是ir时, 原本只能选择同一动作的智能体可以选择更多动作, 此时, 这些不可达的状态将可达.另一方面, 在相同密码员数量时, 随着采用ir策略的智能体数量增加, 集合$ F_{A}^{\mathit{\Lambda} }$会变大, 直接导致算法1需要更多的运行时间.虽然在m > 6时, 系统运行时间较多, 但BDD的变量数目不大, 说明ShTMC可以验证规模较大的系统.

5 结语与展望

针对以往工作在多智能体系统中智能体策略能力建模的不足, 本文提出了带策略类型的解释系统作为异构多智能体系统模型, 该系统模型允许各智能体有其独立的策略能力.以ATL逻辑为例, 本文研究了ATL逻辑在带策略类型的解释系统下的语义和模型检查问题.由于模型表达能力过强, ATL模型检查算法问题不可判定.因此, 本文考虑一种特殊的带策略类型的解释系统, 其中, 在ATL公式联合模态操作中出现的智能体可以是Ir或ir策略类型, 而其他智能体可以是IR, ir或者Ir策略类型, 提出了一个EXPTIME复杂度的模型检查算法, 设计并实现了工具原型ShTMC.

本文仅仅是针对多智能体系统中智能体策略能力建模的不足问题的初步工作, 尚有很多问题有待后续深入研究:(1)其他表达力更强的ATL逻辑的扩展, 如ATL*, Strategy Logic的语义和模型检查问题; (2)其他可能的策略类型, 如可撤销和可删除策略类型等.