随着计算机软硬件系统的飞速发展, 人工智能(artificial intelligence, 简称AI)^[1]理论与技术日益成熟, 并且在计算机领域内得到了前所未有的重视, 其应用领域在逐渐扩大及深入.其中, 智能机器人越来越多地出现在人们的日常生活中, 例如体育产业中的足球机器人、日常生活中的家用伺服机器人以及工业自动焊接机器人等.所以, 保障AI产品的安全性和可靠性, 是如今人们面临的刻不容缓的问题.模型检测(model checking)^[2]是一种简单明了并且实现了自动化的、用于验证软硬件系统是否满足人们期望性质的技术.它已经广泛应用到各类软硬件系统的性能检测中, 如运输控制系统、电子商务、航空航天领域.近年来, 模型检测方法也已经应用到AI产品的性能检测中.模型检测是一种基于逻辑的、应用广泛的、对有限状态系统进行自动化程序验证的技术, 最早由著名学者Clarke与Emerson以及Quielle与Sifakis于20世纪80年代分别提出.在模型检测中, 系统S编码为迁移系统M_S, 要验证的性质规约P用逻辑公式ϕ_P表示, 验证系统S是否满足规约P, 转化为模型M_S是否满足逻辑公式ϕ_P.其中, M_S满足公式ϕ_P简写为M_S|=ϕ_P.

验证AI产品的性能需要将其形式化规约, 而MAS^[2]是AI中应用广泛的分布式系统, 它可以将大而复杂的系统描述成多个彼此可以互相协调通信的小而易管理的系统, 从而完成各自的或者共同的目标.MAS在表达实际系统时, 通过各智能体之间的通信、合作、互解、协调、调度、管理及控制来表达系统的结构、功能及行为特性.采用多智能体系统解决实际应用问题.该系统具有很强的鲁棒性和可靠性, 并具有较高的问题求解效率. MAS已经广泛应用于各个领域, 如智能机器人、交通控制、分布式预测、监控及诊断、分布式智能决策及虚拟现实.MAS引起了众多技术领域的广泛关注, 因此, 设计、实现及验证该系统的工具显得尤为迫切.特别是当MAS应用于安全验证相关领域时, 验证其是否满足设计要求就显得尤其重要了.针对多智能体系统的模型检测方法的研究, 已有学者取得了突出成果^{[4, 5]}.

本文根据文献[6]中提出的APTL模型检测方法实现了多智能体系统模型检测器MCMAS_APTL, 其用APTL公式表示MAS的性质用于检测MAS的性能.APTL公式不仅可以描述经典时序逻辑LTL公式可以描述的性质, 而且可以描述与区间相关的顺序和循环性质以及开放系统和多智能体系统中的与合作和博弈相关的性质, 因此, 用APTL公式可方便描述多智能体系统的性质.

状态爆炸问题是模型检测过程面临的常见问题之一, 即随着变量个数的增多, 系统的状态空间呈指数级增长.在模型检测过程中, 能够缓解空间爆炸问题的技术有二值判断图(BDD)^[7]、抽象技术、限界模型检测、化简和假设-保证推理.MCMAS_APTL是基于APTL的多智能体系统的符号化模型检测器.它利用APTL公式表达多智能体系统的性质, 借助工具MCMAS^[8]中的符号化多智能体系统模块符号化表示要验证的系统, 进而验证模型是否满足给定的APTL公式.该工具不仅可以验证多智能体系统, 还可用于验证普通的反应系统.

MAS的模型检测方法已引起众多学者的广泛关注并且进行了深入研究.文献[9]中提出了验证MAS性质的限界模型检测方法, 通过扩展CTL*得到包括认知模态的逻辑CTL*K.CTL*K可描述同步解释系统的性质, 而且可描述时序和认知两个方面的性质.文献[10]提出了一个基于AUML状态机模型的MAS模型检测机制.文中利用了比较高效的模型检测工具MCMAS.它不仅可用于检测MAS的认知性质, 而且可以检测MAS的智能体的行为是否正确或智能体之间的合作关系, 但该文献不能检测MAS中智能体之间的博弈性质.文献[11]提出了一种自动生成控制器的机制, 当输入一种机器人模型和任务环境以及一种任务或者机器人的行为后, 该控制器就能保证机器人完成任务.该文献中的方法是首先创造一种符合规约LTL公式的控制器, 其中, 任务规约用LTL公式描述, 如机器人的搜索、救援、覆盖面以及障碍躲避等.文献[12]提出了一种在语法层对智能体策略类型进行刻画的系统模型.它允许不同智能体具备不同的策略类型, 研究了基于新模型的ATL模型检测方法并且开发了检测工具.文献[13]研究了下推多智能体系统的模型检测方法, 引入了下推认知博弈结构作为模型, 涉及到的时序逻辑为ATEL、ATEL*和AEMC.本文中的MCMAS_APTL工具利用了比较高效的模型检测工具MCMAS中的符号化表示系统部分, 性质规约用APTL公式描述, 其中, APTL公式简单易懂, 表达能力强, APTL公式可以方便地描述多智能体系统的性质, 所以该工具可方便地用于多智能体系统的性质验证.

本文第1节简单介绍交替投影时序逻辑语法、语义及其他基本概念.第2节阐述多智能体系统模型检测器MCMAS_APTL的框架和实现过程.第3节给出机器人足球赛模型检测实例.第4节对本文进行总结.

1 基础概念 1.1 交替投影时序逻辑

语法. APTL的语法定义如下:

$ P:: = p|\neg P|P \vee Q|{\bigcirc _{\left\langle {\left\langle A \right\rangle } \right\rangle }}P|\left( {{P_1}, \ldots , {P_m}} \right)pr{j_{\left\langle {\left\langle A \right\rangle } \right\rangle }}Q. $

令$\mathcal{P}$为原子命题的可数集合, $\mathcal{A}$为代理的可数集合.其中, p∈$\mathcal{P}$, A⊆$\mathcal{A}$, P_i(i=1, …, P_m), P和Q为APTL公式, ${\bigcirc _{\left\langle {\left\langle A \right\rangle } \right\rangle }}$(next)和$pr{j_{\left\langle {\left\langle A \right\rangle } \right\rangle }}$(projection)为基本的APTL时序操作符.

语义.为了定义APTL公式的语义, 首先需要介绍并发博弈结构(concurrent game structure, 简称CGS)^{[6, 8]}.CGS是一个七元组C=〈$\mathcal{P}$, $\mathcal{A}$, S, S₀, l, △, τ〉, 其中, $\mathcal{P}$是原子命题的有穷非空集合; $\mathcal{A}$是代理的有穷集合; S是状态的有穷非空集合; S₀是初始状态的有穷非空集合; $l:S \to {2^\mathcal{P}}$为标记函数, 每个状态被原子命题集合的子集标记; △^a(s)是代理a∈$\mathcal{A}$在状态s的可以做出决策的非空集合; ${\mathit{\Delta }^\mathcal{A}}(s) = {\mathit{\Delta }^{{a_1}}}(s) \times ... \times {\mathit{\Delta }^{{a_k}}}(s)$是代理集合$A = \{ {a_1}, ..., {a_k}\} \in {2^\mathcal{A}}$在状态s的决策向量的非空集合; 相应地, ${\mathit{\Delta }^\mathcal{A}}(s)$简单表示为△(s), 表示$\mathcal{A}$中的代理的决策集合; 一个决策d_a, 表示代理a在决策d上的决策, d_A表示代理集合A⊆$\mathcal{A}$在决策d的决策.对于每一个状态s∈S和决策d∈△(s), τ(s, d)∈S将状态s和代理集合$\mathcal{A}$的决策d映射到新的状态.f_A为代理集合$\mathcal{A}$在系统C中的一个策略, 该策略使得系统生成多条以初始状态s₀为起始状态的路径.定义out(s, f_A)为以状态s为起始状态策略f_A使得系统执行生成的所有的路径集合.详细讲解见文献[6].

根据CGS的定义, 在$\mathcal{P}$上定义了一个状态s, 为$\mathcal{P}$到B={true, false}的投影, 即s:$\mathcal{P}$→B.在一个CGS中, 以状态s为起始节点的一条路径λ(s)满足APTL公式P, 标记为λ(s)|=P.一个CGS C满足APTL公式P当且仅当所有以CGS的初始节点为起始节点的路径满足公式P, 标记为C|=P.

关系定义如下:

●  λ(s)|=p对于命题p∈$\mathcal{P}$ , 当且仅当p∈l(s).

●  λ(s)|=¬P当且仅当λ(s)|≠P.

●  λ(s)|=P∨Q当且仅当λ(s)|=P或λ(s)|=Q.

●  λ(s)|=${\bigcirc _{\left\langle {\left\langle A \right\rangle } \right\rangle }}$P当且仅当|λ(s)|≥2, 并且A存在一个策略f_A, 使得λ(s)∈out(s, f_A), 并且λ(s)[1, |l|]|=P.

●  λ(s)|=(P₁, …, P_m)$pr{j_{\left\langle {\left\langle A \right\rangle } \right\rangle }}$Q当且仅当A存在一个策略f_A, l(s)∈out(s, f_A), 0=r₀≤r₁≤…≤r_m≤|λ(s)|, 使得λ(s)[r_i-1, r_i]|=P_i, 0 < i≤m并且λ|=Q, l由以下两种情况得到:

a)   r_m < |λ(s)|, 那么λ=λ(s)↓(r₀, …, r_m)×λ(s)[r_m+1, …, |λ(s)|];

b)   r_m=|l(s)|, 那么λ=λ(s)↓(r₀, …, r_m).

APTL范式.将APTL公式转化为范式(normal form)^[6]形式, 是APTL模型检测中不可或缺的环节.接下来简单介绍APTL公式的范式和完全范式(complete normal form)的定义.

定义1(范式(normal form)). Q_P为APTL公式Q中的原子命题集合, 公式Q的范式定义为

$ Q \equiv {Q_e} \wedge \varepsilon \vee \vee _{i = 0}^n\left( {{Q_{ci}} \wedge {Q_i}} \right), {Q_i} \equiv \wedge _{j = 1}^r{\bigcirc _{\left\langle {\left\langle A \right\rangle } \right\rangle }}{Q_{ij}}. $

Q_e为状态公式, ${Q_{ci}} \equiv \wedge _{k = 1}^l{{\dot q}_k}, {q_k} \in {Q_p}, {{\dot q}_k}$为q_k或¬q_k, 如果i≠j, 则Q_ci≠Q_cj; Q_ii为APTL公式.

APTL公式的范式包含两部分:Q_e∧ε为终止部分, 若只有1个状态s₀的路径满足公式Q_e, 则满足Q_e∧ε; Q_ci∧Q_i为非终止部分, 公式Q_ci∧Q_i的模型为一个生成树, 其中, 该生成树的根节点满足Q_ci.

定义2(完全范式(complete normal form)). Q_P为APTL公式Q中出现的原子命题组成的集合, Q的完全范式定义为$Q \equiv {Q_e} \wedge \varepsilon \vee \vee _{i = 0}^n({m_i} \wedge {M_i}){\rm{, }}$其中, ${M_i} \equiv \wedge _{j = 1}^r{\bigcirc _{\langle \langle {A_{ij}}\rangle \rangle }}{M_{ij}}{\rm{.}}$Q_e为状态公式; ${m_i} \equiv \wedge _{k = 1}^l{{\dot q}_k}, {q_k} \in {Q_p}, {{\dot q}_k}$为q_k或¬q_k; $\vee _{i = 0}^n{m_i} \equiv {\rm{true}}$并且∨_i≠j(m_i∧m_j)≡false, m_i是原子命题的最小项, 如果有n个原子命题, 就有2ⁿ个最小项m₀, m₁, …, ${m_{{2^n} - 1}}{\rm{;}}$M_ij是原子命题的最大项, 也有2ⁿ个最大项.

文献[14]中的定理4已经证明, 任意一个APTL公式都可以转化为范式.将公式Q转化为范式后, 进一步可以转化为完全范式.如果Q的完全范式为$Q \equiv {Q_e} \wedge \varepsilon \vee \vee _{i = 0}^n({m_i} \wedge {M_i}), $则¬Q的范式为$\neg Q \equiv \neg {Q_e} \wedge \varepsilon \vee \vee _{i = 0}^n({m_i} \wedge \neg {M_i}).$

1.2 符号模型检测

模型检测是一种有效验证有限状态系统性质的技术.由于基于枚举的模型检测方法容易造成状态爆炸问题, 所以在实际应用中会遇到很多问题.研究者们尝试解决该问题, 提出了一些缓解模型检测过程中状态爆炸问题的有效方法, 如抽象技术、限界模型检测以及基于BDD的符号模型检测.符号模型检测的核心思想是建立在将状态集合和迁移关系集合用布尔方程表示的基础上的, 用布尔方程隐式地描述状态集合和迁移关系集合, 比显式地利用枚举方式描述能够显著节约存储空间.符号化模型检测方法是以状态集合为操作对象, 而不是单个状态.

符号化表示方法能够更加简洁地表示系统状态, 本文利用二值判断图(binary decision diagrams, 简称BDD)表示状态集合.通过对BDD操作, 容易实现求状态集合的前驱状态集合、后继状态集合以及状态集合的合并等.符号化模型检测算法与枚举模型检测算法的基本搜索过程相似, 本质区别在于, 一般的模型检测中以单个状态为操作对象; 而符号模型检测中以状态集合为操作对象, 且借助BDD等数据结构, 已经有功能强大的操作工具包作为后续开发基础.

二值判断图(BDD). BDD表示布尔函数的有根无环有向图, 内部节点标记对应公式中的变量, 叶子节点标记为0或1.如图 1所示为布尔函数$f(a, b, c, d) = a \wedge b \vee c \wedge \bar d$的BDD.

一个布尔公式可由不同的BDD表示, 为确保每个布尔公式对应唯一的BDD, 对BDD有两种限制:(1)对布尔公式中的变量进行排序, 如图 1中布尔公式变量排序为a < b < c < d; (2) BDD中不存在冗余子树和多余的节点.因此, 基于这两种限制, 多余的叶子节点、同构子树以及重复的非终节点可被删除, 得到最简BDD, 如图 1所示即为该公式对应的最简排序BDD.

1.3 MCMAS

MCMAS是一种多智能体模型检测工具, MCMAS的框架结构如图 2所示.

MCMAS具有成熟、高效的符号化技术, 我们借助MCMAS中模型的符号化模块实现APTL模型检测工具MCMAS_APTL.MCMAS利用解释系统编程语言(interpreted system programming language, 简称ISPL)描述要验证的系统, 支持的逻辑为CTLKD-A^DC[8].将要验证的系统和一组公式输入MCMAS, 可计算出系统是否满足公式.如果公式不成立, 则输出一条反例路径; 否则, 输出一条证据路径.

在MCMAS中要验证的程序形式化表示为解释系统(interpreted system)并用语言ISPL描述.ISPL程序将一种多智能体系统描述为包含多个智能体和环境的系统, 对于ISPL描述的智能体简单介绍如下.局部状态(local states)是智能体的私有内部状态, 是由变量描述的, 对于其他智能体是不可见的.智能体与其他智能体和环境的互动是通过将局部状态转化为公共可视化的变量完成的.智能体采取的动作(action)由智能体的局部协议(local protocol)决定.局部状态随局部演变函数变化, 该类函数根据当前的局部状态和所有智能体的全局动作(joint action)给出可能的下一个局部状态(next local state).ISPL程序的结构是根据IS的语义给出的, 并且可以广泛应用于描述多智能体系统.在程序中, 环境用关键字Environment表示, Environment中的一些局部变量对其他智能体可见.

2 原型工具

从底层开发实现模型检测工具耗时、耗力, 不可控因素较多, 本文以开源工具为基础实现我们提出的模型检测器.鉴于MCMAS工具所具有的特性和优点, 最终选择以MCMAS为基础实现APTL符号模型检测算法.

2.1 工具框架

我们开发实现了用于验证多智能体系统的APTL符号模型检测器MCMAS_APTL.该工具借助了MCMAS的符号化表示模型.MCMAS_APTL的架构如图 3所示.

MCMAS_APTL采用C++语言开发, 由3个模块组成, 分别为:用布尔函数符号化表示解释系统模块; 将APTL公式转化为范式模块; 检查解释系统是否满足APTL公式模块.第1个模块是将解释系统符号化表示, 该模块是借助工具MCMAS中的对应的部分; 第2个模块是将APTL公式转化为范式; 第3个模块是通过计算满足公式的状态集合验证输入的解释系统是否满足给定的APTL公式.

2.2 模型检测方法

符号模型检测方法有效缓解状态爆炸问题的关键环节是用布尔方程符号化表示模型, 进而用ROBDD高效地表示; 后续整个检查过程操作都是在ROBDD上进行的.APTL符号模型检测方法是将多智能体系统模型化为解释系统后进行检测的.解释系统是Kripke结构的一种扩展, 与CGS相比更适合MAS的建模.在CGS中系统只有全局状态这一概念, IS的全局状态是由内部所有智能体的局部状态组成.详细的比较见文献[6].

2.2.1 符号化表示解释系统

下面简单介绍符号化表示解释系统(interpreted system)的方法.给定一个解释系统IS=〈(L_i, Act_i, P_i, t_i)_i∈Σ, S₀, h〉.

●  编码一个智能体i(i∈$\mathcal{N}$)的局部状态需要nv(i)=$\left\lceil {{{\log }_2}\left| {{L_i}} \right|} \right\rceil $个布尔变量, 编码系统的全局状态g为布尔向量$\bar v = ({v_1}, \ldots , {v_N})$, 其中, $N = \sum\nolimits_i {nv(i)} {\rm{.}}$

●  编码一个智能体的局部行为需要na(i)=$\left\lceil {{{\log }_2}\left| {Ac{t_i}} \right|} \right\rceil $个布尔变量, 编码系统的全局行为a为布尔向量$\bar w = ({w_1}, \ldots , {w_M})$, 其中, $M = \sum\nolimits_i {na(i)} {\rm{.}}$

●  一个智能体的协议可用局部状态和行为的布尔公式蕴含关系编码.$P(\bar v, \bar w)$是所有协议的布尔函数组合得到的整个系统协议布尔函数.

●  一个智能体的演变函数是由该智能体的局部变量和其他智能体行为以及环境的可视化变量组成的布尔函数表示, $t(\bar v, \bar w, \bar v')$为所有智能体演变函数的布尔函数组合得到的整个系统演变关系布尔函数.

●  系统的初始状态集合可用一个布尔函数${S_{0\bar v}}$表示.

解释系统IS的时序迁移关系可以用布尔方程R_t(g, g')表示.该方程由所有代理的演变方程t_i得到, 即

$ {R_{t(\bar v, \bar v')}} = { \vee _{\bar w \in Act}}(t(\bar v, \bar w, \bar v') \wedge P(\bar v, \bar w)){\rm{.}} $

该公式描述全局状态间的布尔关系, 应用于时序逻辑操作符的计算.可达全局状态集合G可以用一个布尔公式表示, 并通过求解$\tau (Q) = ({S_{0\bar v}} \vee \exists (\bar v')({R_{t(\bar v', \bar v)}} \wedge {Q_{\bar v'}}))$的不动点得到.其中, Q为系统状态集合.τ的不动点可通过迭代计算τ($\emptyset $)得到^[1].

2.2.2 APTL符号模型检测器的实现

在APTL模型检测方法中, 需要验证的系统描述为解释系统IS=〈(L_i, Act_i, P_i, t_i)_i∈Σ, S₀, h〉, 要验证的性质用APTL公式表示.IS, λ$\vDash$ ϕ表示IS中的路径λ满足ϕ, 简写为λ|=ϕ.IS|=ϕ当且仅当以初始状态为起始状态的任意一条路径满足公式ϕ.

定义3(满足性质的状态集合).对于一个APTL公式ϕ和解释系统IS=〈(L_i, Act_i, P_i, t_i)_i∈Σ, S₀, h〉, 其中一条执行路径λ是系统IS中的非空状态序列, l为有穷或者无穷路径.集合Sat(ϕ)⊆G包含了所有的至少有1条以其为初始节点的路径满足公式ϕ的状态:

$ Sat\left( \phi \right) = \left\{ {g \in G\left| {\exists \lambda \in Paths\left( G \right)} \right| = \phi \;{\rm{and}}\;\lambda \left[ 0 \right] = g} \right\}, $

其中, G为系统IS的全局状态集合, Paths(G)表示全局状态组成的所有的路径集合.

对于一个解释系统IS=〈(L_i, Act_i, P_i, t_i)_i∈Σ, S₀, h〉, 给定一个代理集合A⊆Σ, 全局状态集合G₁⊆G和迁移关系t'⊆t, 函数PRE_img返回状态集合G₁中状态的前驱状态集合.Σ为系统的代理集合, G为可达全局状态集合, t为全局状态的演变函数.函数PRE_img定义如下:

$ PRE\_img(A, {G_1}, t') = \{ g \in {G_1}|\exists g'{G_1}.t'\left( {g, {P_A}} \right) = g'\} . $

解释系统IS=〈(L_i, Act_i, P_i, t_i)_i∈Σ, S₀, h〉和APTL公式ϕ中, IS|=ϕ当且仅当Sat(¬ϕ)和S₀的交集为空.依据以上的基础概念, 我们实现了函数APTL_model_checking(bdd_parameters*para, char*ϕ)检查解释系统IS=〈(L_i, Act_i, P_i, t_i)_i∈Σ, S₀, h〉是否满足APTL公式ϕ, 其中, para为系统模型的符号化表示参数.检查函数首先调用函数cal_aptl_bdd(bdd_parameters*para, char*f)计算Sat(¬ϕ)的特征函数$Sa{t_{\bar v}}(\neg \phi )$, 然后判断$Sa{t_{\bar v}}(\neg \phi ) \cdot {S_{0\bar v}}$是否为0.

●  若$Sa{t_{\bar v}}(\neg \phi ) \cdot {S_{0\bar v}} = 0{\rm{, }}$则表明Sat(¬ϕ)和S₀的交集为空, 即不存在一条路径λ∈Paths(g₀)(g₀∈S₀), 使得λ|=¬ϕ.即IS中的所有执行路径满足公式ϕ;

●  如果$Sa{t_{\bar v}}(\neg \phi ) \cdot {S_{0\bar v}} \ne 0$, 则说明在IS中至少存在1条以状态集合Sat(¬ϕ)∩S₀中的状态为起始状态的执行路径λ_ce, 使得λ_ce|=¬ϕ.

函数APTL_model_checking(bdd_parameters*para, char*ϕ)的伪代码如下所示.

void APTL_model_checking(bdd_parameters*para, char*ϕ){

1.  BDD b←cal_aptl_bdd(para, ¬ϕ);

2.  BDD temp←b*(*(para→in_st));

3.  if temp==0

    return IS|=ϕ;

4.  else

    return IS|≠ϕ;

}

其中, 函数APTL_model_checking中的第1行是计算满足公式¬ϕ的状态集合的BDD, 第2行是计算满足公式¬ϕ的状态集合与系统的初始状态集合的交集, para→in_st为表示系统的初始状态集合的BDD.

函数BDD cal_aptl_bdd(bdd_parameters*para, char*f)计算满足APTL公式ϕ的状态集合的BDD, 形参为系统模型的符号化表示参数和APTL公式ϕ, 返回的是表示满足公式ϕ的状态集合的BDD.其中, “+”和“×”分别代表逻辑“或”和“与”, $Sa{t_{\bar v}}(\phi )$为Sat(ϕ)的布尔方程.NF(f)是将公式ϕ转化为范式的过程, $PRE\_img(A, Sa{t_{\bar v}}(\varphi ), {R_t})$是计算$Sa{t_{\bar v}}(\varphi )$的前驱状态函数.FIXPOINT$(\mathcal{c}(Sa{t_{\bar v}}({\phi _{i{r_e}}}), {R_t}))$计算$\mathcal{c}(Sa{t_{\bar v}}({\phi _{i{r_e}}}), {R_t})$的不动点.

BDD cal_aptl_bdd(bdd_parameters*para, char*ϕ){

1.  mark[ϕ]=0, $Sa{t_{\bar v}}(\phi ) = 0$;

2.  $NF(\phi ) = \vee _{i = 1}^n{\mathit{\psi } _i}$;

3.  mark[ϕ_i'j]=0;

4.  vector〈BDD*〉*R_t←(para→vec_reachRT);

5.  for (int i=1; i≤n; i++){

6.    if Ψ_i≡ϕ_e∧ε then

      $Sa{t_{\bar v}}({\mathit{\psi } _i}) = Sa{t_{\bar v}}({\phi _e}) \cdot PRE(\emptyset , Sa{t_{\bar v}}(\varepsilon ), {R_t})$

7.    else if ${\mathit{\psi } _i} \equiv {\phi _i} \wedge \wedge _{j = 1}^m{\bigcirc _{\langle \langle {A_{ij}}\rangle \rangle }}{\phi _{ij}}$, 对于该公式中的公式ϕ_ii, 存在1≤k≤m, mark[ϕ_ik]==0, 或者

        1≤r≤m, mark[ϕ_ir]==1 then{

        对于所有的ϕ_ik, 令mark[ϕ_ik]=1;

        $Sa{t_{\bar v}}({\mathit{\mathit{\psi } }_i}) = Sa{t_{\bar v}}({\phi _i}) \cdot \prod\nolimits_k {(PRE({A_{ik}}, cal\_aptl\_bdd(para, {\phi _{ik}}), {R_t}))}$

        $\prod\nolimits_r {(PRE({A_{ir}}, FIXPOINT(\mathcal{c}(Sa{t_{\bar v}}({\phi _{i{r_e}}}), {R_t})), {R_t}))} $;

        其中, ${\phi _{ir}} \equiv {\phi _{i{r_e}}} \wedge \wedge _{x = 1}^y{\bigcirc _{\langle \langle {A_{i{r_{ex}}}}\rangle \rangle }}{\phi _{i{r_{ex}}}}$, $\mathcal{c}$(X, R_t)计算X的值;

     }

    }

8.  $Sa{t_{\bar v}}(\phi ) = Sa{t_{\bar v}}({\mathit{\mathit{\psi } }_1}) + Sa{t_{\bar v}}({\mathit{\mathit{\psi } }_2}) + ... + Sa{t_{\bar v}}({\mathit{\mathit{\psi } }_n})$;

9.  return $Sa{t_{\bar v}}(\phi )$;

}

函数BDD cal_aptl_bdd(bdd_parameters*para, char*ϕ)中, 第2行将公式ϕ转化为范式, 其中, Ψ_i≡ϕ_e∧ε或者Ψ_i≡${\phi _{i'}} \wedge \wedge _{j = 1}^m{\bigcirc _{\langle \langle {A_{i'j}}\rangle \rangle }}{\phi _{i'j}}$; 第4行中, para→vec_reachRT为系统模型的迁移关系.

函数cal_aptl_bdd首先将APTL公式ϕ转化为范式, 后续分别处理各项Ψ_i.

●  如果Ψ_i≡ϕ_e∧ε, 根据范式的定义, ϕ_e为状态公式, $Sa{t_{\bar v}}({\mathit{\mathit{\psi } }_i})$表示满足ϕ_e的状态集合, 并且这些状态是有穷执行路径的最终状态.

●  如果${\mathit{\psi } _i} \equiv {\phi _i} \wedge \wedge _{j = 1}^m{\bigcirc _{\langle \langle {A_{ij}}\rangle \rangle }}{\phi _{ij}}$, 首先调用函数cal_aptl_bdd计算$Sa{t_{\bar v}}({\phi _i})$.在计算过程中, 如果生成了在ϕ的转化中没有出现过的子公式ϕ_ik(1≤k≤m), 计算PRE_img(A_ik, cal_aptl_bdd(f_ik, R_t), R_t); 如果生成了在转化ϕ的过程中出现过的子公式ϕ_ir(1≤r≤m), 说明公式对应的图中存在环, 所以计算$Sa{t_{\bar v}}({\phi _{ir}})$ 变的很复杂.这个问题可以通过计算不动点得到$Sa{t_{\bar v}}({\phi _{ir}})$, 然后计算前驱集合$PRE\_img({A_{ir}}, Sa{t_{\bar v}}({\phi _{ir}}), {R_t})$.通过将上面求到的布尔方程求“与”, 得到$Sa{t_{\bar v}}({\mathit{\psi } _i})$.

最后, 布尔方程$Sa{t_{\bar v}}({\mathit{\psi } _i})$可以将所有的$Sa{t_{\bar v}}({\mathit{\psi } _i})$求“或”得到, 即$Sa{t_{\bar v}}(\phi ) = Sa{t_{\bar v}}({\mathit{\psi } _1}) + Sa{t_{\bar v}}({\mathit{\psi } _2}) + ... + Sa{t_{\bar v}}({\mathit{\psi } _n})$.

3 机器人足球赛模型检测实例

机器人足球赛^[15]是多智能体系统的典型应用, 其中涉及到了机器人之间的合作与竞争.在足球比赛过程中, 同一个组的机器人合作, 尽可能地将球踢入对方球门, 而对方机器人会尽力阻止足球进入自己球队球门.这个过程要求机器人能够根据不同的情景选取不同的策略, 其中的合作和博弈性质可以方便地用APTL公式描述.所以, 本文通过机器人足球赛的简单示例展示该工具的工作效果.

3.1 机器人足球赛的策略模型

本节介绍机器人足球赛的策略模型.

3.1.1 足球场地模型

机器人足球赛场地为长方形, 一般是长9 000mm、宽6 000mm.整个球场分为3个区域:前场、中场、后场, 这3个区域是用直线分隔开的.足球场地模型如图 4所示, 场地被量化为长30个单位、宽20个单位, 每个单位代表 300mm.(x, y)坐标表示球场中的位置, 中央点的坐标为(15, 10), 中圈的半径为3个单位长度.球门宽度为4个单位长度, 两个球门线的坐标分别为(0, 8), (0, 12)和(30, 8), (30, 12).禁区宽为4个单位长度, 长为8个单位长度.

3.1.2 策略模型

由于机器人足球赛的参数随着比赛的进行而变化, 所以机器人足球赛的路径规划问题比较复杂.在比赛中, 足球机器人不仅要考虑本队的策略和规划, 而且要考虑对方球队机器人可能的策略.所以在一个特定的场景下, 可能有多个不同的最优选择.机器人足球赛的规则和人类足球赛规则类似.一般地, 一个机器人可以采取的行动如下.

●  开球(kick off):在比赛开始时, 一个机器人将球踢出.

●  防护(go to defend):机器人去防护对方球员.

●  靠近球(go to the ball):机器人靠近球.

●  截球(intercept the ball):当对方球员持球时, 试图截取球.

●  传球(pass the ball to its teammate):当持球的机器人被对方球员拦截时, 该机器人将球传给本队队员.

●  射门(shoot the ball into the goal):机器人球员试图将球踢入对方球门.

●  带球前行(go forward with the ball):机器人持球向距离对方球门近的地方前行.

在比赛过程的任意时刻, 每一个机器人都能获取球的位置、两个球门的位置、自身的位置和其他机器人的位置.根据不同的情形, 团队中的球员担当不同的角色, 其中包括前锋(striker)、中场(midfielder)和后卫(defender).守门员与其他球员不同.在整场比赛过程中, 守门员的角色不变, 其程序也比较简单, 仅是一直在寻找、发现和观察球的情况.当球靠近球门时, 守门员试图将球踢出以防对方球队进球, 并且试图将球踢到距离本队球门较远的位置.对于一场机器人足球赛, 持球的球队采取攻击策略(attack tactic), 对方球队采取防卫策略(defensive tactic).下面详细介绍包含两个球队A和B的足球赛策略, 每队各有4名球员.

防卫策略(defensive tactic).当足球在A队的中场或者后场时, A队采取防卫策略.如果A队没有队员持球, 那么A队中距离球最近的队员试图截球, 该球员作为后卫.距离对方球门最近的队员跑去中场并作为前卫, 当本队球员截取到球后等待着传球.另外一个球员作为中场队员, 并且试图去拦截对方球员的传球.该场景如图 5(a)所示, 红色队员属于A队, 黄色队员属于B队.其中GK为守门员、S为前锋、M为中场、D为后卫.如果A队队员持球, 持球的机器人作为中场队员且必须将球传给前锋.剩余的一个队员作为后卫并且停留在罚球点(penalty spot).当前锋得到球后采取新的策略, 该队员将会有新的角色或者行为.该情形如图 5(b)所示.

进攻策略(offensive tactic).当球在前场时, A队采取进攻策略.如果A队队员持球, 持球队员作为前锋, 距离本队球门最近的队员作为后卫且站在罚球点以防对方球员进球.另一个队员作为中场队员与前锋保持在一个水平线上并且在离对方球门近的地方, 如果对方球员没有在球门和前锋之间拦截球, 那么前锋将球踢向对方球门.如果对方球员试图拦截球, 那么前锋将球传给中场队员, 并选择新的策略.以上两种情形如图 6所示.如果A队没有队员持球, A队中的前锋试图截球.后卫必须在后场以防对方球员进球.中场球员阻挡对方队员靠近自己区域以防对方队员之间传球.

3.2 实验展示

首先, 我们根据上述介绍的足球赛策略用ISPL描述机器人足球赛过程; 然后, 用工具MCMAS_APTL展示比赛过程并验证是否两个球队都有可能进球.球队分为红、黄两个队, 每队有3名队员.足球场地模型如图 4所示, 守门员的活动区域为罚球区.

守门员可以采取的动作包括act_none、run、intercept和kick the ball.显然, act_none表示守门员不行动; run表示守门员前进; intercept表示守门员拦截对方球员进球; kick the ball表示守门员踢球.前锋和中场可以采取的动作包括act_none、kick off、kick the ball、run、intercept、shoot、pass the ball、take a pass和dribbling.kick off表示球员在比赛开始时开球; pass the ball表示球员将球传递给本队球员; shoot表示球员试图将球踢入对方球门; take a pass表示球员得到本队球员传的球; dribbling表示球员持球前行.

足球赛的模型描述为一个解释系统, 红队包含3个代理(agent):r_gk、r_1和r_2, 其中, r_gk为守门员; r_1和r_2根据实际情况有3个角色——前锋(striker)、中场(midfielder)和后卫(defender).黄队也有3个代理:y_gk, y_1和y_2, 角色分配与红队类似.代理environment包含可视变量用于描述比赛过程中的环境.

以r_1为例介绍机器人的部分行为, kick off表示代理r_1在比赛开始时开球, 代码如下所示.

Agent r_1

  Vars:

    state:{s_none, kick_off, kick_the_ball, run, intercept, shoot, pass_the_ball, dribbling}

  end Vars

  Actions={act_none, kick off, kick the ball, run, intercept, shoot, pass the ball, dribbling}

  Protocol:

  ...

  state=kick_off:{kick off};

  ...

  end Protocol

  Evolution:

  ...

  state=kick_off if Environment.state=r_kickoff and Environment.ballx=15 and Environment.bally=10

    and (Environment.r_2x < 12 or Environment.r_2x > 18) and (Environment.r_2y > 13

    or Environment.r_2y < 7) and (Environment.y_1x < 12 or Environment.y_1x > 18)

    and (Environment.y_1y > 13 or Environment.y_1y < 7) and (Environment.y_2x < 12

    or Environment.y_2x > 18) and (Environment.y_2y > 13 or Environment.y_2y < 7);

  ...

  end Evolution

end Agent

其中, (Environment.ballx, Environment.bally)表示球的位置坐标, (Environment.red_gkx, Environment.red_gky)表示代理red_gk的位置坐标, 其他类似.Vars中的state为代理r_1的状态变量, 括号内为r_1的所有可能的状态取值.Actions为r_1的所有的行为动作.Protocol为r_1的协议, 如, state=kick_off:{kick off}表示当r_1的状态为kick_off时, 其采取的行动为kick off.Evolution是代理r_1的演变函数, 例如代码中r_1的演变函数, 当if后面的公式的值为真时, 代理r_1的状态为kick_off; 如果代理在某一状态时同时有多个if后面的公式的值为真, 则代理的状态是在几个可能的状态中随机选取的.

行为pass the ball表示代理r_1传球给队友r_2.如果r_1持球并且无法将球踢入对方球门, 那么r_1采取pass the ball行动, 同时, 对方球队队员会试图截球, pass the ball的代码如下所示.

Agent r_1

  ...

  Evolution:

  ...

  state=pass_the_ball

    if Environment.state=r1_ball and Environment.r_2x > Environment.r_1x

    and Environment.r_2x-Environment.r_1x≤5...

    and Environment.y_2y < Environment.r_2y)) or (Environment.r_1y > Environment.r_2y

    and Environment.r_1y-Environment.r_2y≤5...

    and Environment.y_2y < Environment.r_1y)) or (Environment.r_1y=Environment.r_2y

   ...));

  ...

  end Evolution

end Agent

shoot表示代理r_1将球踢入对方球门, ISPL代码如下所示:

Agent r_1

  ...

  Evolution:

  ...

  state=shoot if Environment.state=r1_ball and... or (Environment.y_1y < Environment.r_1y...

    or (Environment.y_2y < Environment.r_1y and Environment.r_1y-Environment.y_2y≤3)));

  state=shoot if Environment.state=r1_ball and Environment.r_1x≥20;

  ...

  end Evolution

end Agent

当y_1或者y_2持球并且条件对r_1有利, r_1可能采取intercept行为, 该情况下ISPL代码如下所示:

Agent r_1

  ...

  Evolution:

  ...

    state=intercept if Environment.state=y1_ball and ((Environment.y_1x-Environment.r_1x)

    *(Environment.y_1x-Environment.r_1x)+(Environment.y_1y-Environment.r_1y)

    *(Environment.y_1y-Environment.r_1y))≤((Environment.y_1x-Environment.r_2x)

    *(Environment.y_1x-Environment.r_2x)+(Environment.y_1y-Environment.r_2y)

    *(Environment.y_1y-Environment.r_2y));

  state=intercept if Environment.state=y2_ball and...)≤((Environment.y_2x-Environment.r_2x)...);

  ...

  end Evolution

end Agent

对于该系统, 原子命题集合AP={redscore, yellowscore}, redscore表示红队进球得分, yellowscore表示黄队进球得分; 代理分为两个组g₁={r_gk, r_1, r_2}和g₂={y_gk, y_1, y_2}.为了得到黄队进球得分的路径, 我们给出APTL公式$\neg {\diamondsuit _{\langle \langle {g_2}\rangle \rangle }}yellowscore$, 如果黄队能够进球, 会输出一条路径满足${\diamondsuit _{\langle \langle {g_2}\rangle \rangle }}yellowscore$.其中, 公式${\diamondsuit _{\langle \langle {g_2}\rangle \rangle }}yellowscore$的语义为代理集合g₂存在策略使得执行路径上存在状态满足原子命题公式yellowscore.如图 7所示为一条满足公式${\diamondsuit _{\langle \langle {g_2}\rangle \rangle }}yellowscore$的路径, 其中, 足球从中央点(15, 10)经由曲线到达点(0, 11), 球到点(0, 11)表明黄队已进球, 该曲线为比赛过程中足球的运动轨迹.

另外, 本文实现了一场每队有两名队员的机器人足球赛, 球队的策略与第3.1节介绍的策略类似.原子命题集合为AP={redscore, yellowscore}, redscore表示红队得分进球, yellowscore表示黄队得分进球.系统包含两支球队分别为g₁={red_gk, red_f}, g₂={yellow_gk, yellow_f}.

在球赛开始时, 代理red_f开球.如果想要得到红队进球得分的一条路径, 给出APTL公式$\neg {\diamondsuit _{\langle \langle {g_1}\rangle \rangle }}redscore{\rm{, }}$当红队进球得分时, MCMAS_APTL输出一条路径满足公式${\diamondsuit _{\langle \langle {g_1}\rangle \rangle }}redscore$, 如图 8所示.

另外, 本文实现了每个球队包含两个队员的实验, 其中, 模拟过程执行时间、可达状态数以及所用的BDD存储空间如表 1中2×2这一行所示.与每个球队有两个球员的比赛相比, 每个球队有3个球员的比赛所用时间明显增多, 状态空间爆发式增长.这两种实验都是在2.93GHZ Intel Core i7, 8GB RAM上完成的.实验结果表明, 工具MCMAS_APTL具有一定的实用性, 但是要高效地验证复杂的多智能体系统, 还需提高工具MCMAS_APTL的性能.

4 结论

本文根据APTL符号模型检测算法实现了模型检测器MCMAS_APTL, 将APTL模型检测算法实现并且融合到MCMAS中, 实现了一种基于APTL的多智能体系统模型检测器.在实现MCMAS_APTL时, 借助了MCMAS的符号化系统模块, 该部分可高效地符号化表示要验证的系统, 从而提高了模型检测的效率.在工具MCMAS_APTL中实现了利用APTL公式验证多智能体系统的时序性质.在未来的工作中, 将会研究系统的认知性质并且实现对多智能体系统认知性质的检测.