责任政策描述了多Agent之间的交互策略，即Agent被允许或禁止保持某种状态或执行某些活动，并关联着一些条件集合，这些条件以环境的形式存在于责任描述中，描述系统状态以及政策的应用规则。因此，在定义责任政策语言前，先定义责任政策环境。与责任相关的环境主要有基于状态的环境和基于事件的环境。基于状态的环境声明政策中责任的状态环境，基于事件的环境声明责任被激活、失效、违反或履行的时刻。基于状态的责任环境表达式为：$Cs(\text{A}{{\text{g}}_{1}},\text{A}{{\text{g}}_{2}},\varphi )\leftarrow {{p}_{1}},{{p}_{2}},\cdots ,{{p}_{n}}$，其形式语义定义为当命题公式${{p}_{1}},{{p}_{2}},\cdots ,{{p}_{n}}$为真，Ag₁向Ag₂承诺$\varphi $时所在的环境$Cs$有效。基于事件的环境则描述了基于状态的环境开始有效和终止有效的时刻，其被声明为$\text{start}(Cs)$和$\text{end}(Cs)$。责任政策的环境表达式如下：

式中，$C$表示责任政策的环境表达式；$Cs$是基于状态的环境表达式；$Ce$是基于事件的环境表达式；$c$是用户定义的基于状态的环境标识符；$[C{{s}_{1}},C{{s}_{2}}]$表示一个区间，其声明基于状态的环境在$C{{s}_{1}}$为真时开始有效，在$C{{s}_{2}}$为真时终止有效。

定义 1  责任(Obligation)。责任是一个六元组$\text{Obligation=}(N,\text{debtor},\text{creditor},\varphi ,Ca,Cv)$，其中，N是责任标识符，debtor责任的发起方，debtor是责任的接收方，$\varphi $是声明责任内容的逻辑公式，Ca是责任的激活环境，Cv是责任的违反环境。责任被声明后，debtor将向creditor传递由$\varphi $表示的事实或需要执行的动作，Ca和Cv分别声明了责任被激活和违反的环境。

定义 2  责任政策语言(obligation policy language,OPL)。 $\text{OPL}=(A,O,C,\text{Action},R,\text{sta})$是一个六元组，其中，A是政策中所有Agent的集合，$\forall A{{g}_{i}}\in A$，$i\in N$，$A{{g}_{i}}$既可以是责任的$\text{debtor}$也可以是$\text{creditor}$；O是政策中所有责任的集合；C是政策环境的集合；$\text{Action}=\text{Ac}{{t}_{o}}\bigcup \text{Ac}{{t}_{c}}$是政策动作的集合，$\text{Ac}{{\text{t}}_{o}}=\{\text{create},\text{active},\text{fulfil},\text{violate},\text{deactivate}\}$是责任操作动作的集合，$\text{Ac}{{\text{t}}_{c}}$是责任内容中动作的集合，即责任内容中$\text{debtor}$承诺执行的动作；$R$是责任政策执行需满足的时序性质集合。$\text{sta}:O\to A$是一个责任分配函数，给出每个责任所归属的Agent。

责任政策语言通过责任状态模型描述交互策略的动态演化，基于操作语义可将交互策略的OPL模型转换为NuSMV的输入模型。

OPL模型中主要包含连续型责任和非连续型责任。连续型责任声明系统中有维持事物状态需求的责任，在系统中这种责任从环境起始直至环境结束都要求其保持激活状态，如考虑如下责任$\text{Obligation=}({{n}_{0}},A{{g}_{1}},A{{g}_{2}},{{\varphi }_{3}},\text{insuranced},\text{below }\!\!\_\!\!\text{ limit }\!\!\_\!\!\text{ payment})$，责任${{n}_{0}}$声明参加养老保险的职工$A{{g}_{1}}$向管理机构$A{{g}_{2}}$缴费不能低于缴费下限。其中，$A{{g}_{1}}$是养老保险参保人员，$A{{g}_{2}}$是养老保险管理机构，${{\varphi }_{3}}\text{=pay }\!\!\_\!\!\text{ fees}(A{{g}_{1}},A{{g}_{2}})$声明$A{{g}_{1}}$向$A{{g}_{2}}$执行缴费行为，激活环境声明责任在$\text{insuranced}$为真的情况下有效，违反环境低于费款下限$\text{below }\!\!\_\!\!\text{ limit }\!\!\_\!\!\text{ fees}$被定义为below_limit_payment$(A{{g}_{1}},\_,\_)\leftarrow $limit_payment $(A{{g}_{1}},{{x}_{1}}),\text{current }\!\!\_\!\!\text{ payment}(A{{g}_{1}},{{x}_{2}}),{{x}_{2}}\prec {{x}_{1}}$，其声明参保人员缴纳保险费低于政策规定的缴费下限的情况。

非连续型责任是被激活后可能发生失效的责任，其定义条件可表示为$\text{end}(Ca)\ne \text{false}$。

责任的状态模型描述责任政策的动态演化过程，根据责任类型的定义，责任状态模型被分为两种：连续型责任状态模型和非连续型责任状态模型，分别如图 1和图 2所示。

图  1  连续型责任的状态模型

图  2  非连续型责任的状态模型

在责任状态模型中，责任$\text{Obligation=}(N,\text{debtor},\text{creditor},\varphi ,Ca,Cv)$的状态主要包括：

1) 初始状态$\bullet $，该状态表示责任未被创建。

2) 非活跃状态$\text{inactive}$，其可被形式化声明为$\text{inactive}(\text{obligation})\leftarrow (\text{create(debtor,obligation})\wedge (\neg \text{start}(Ca))\vee \text{end}(Ca)))$。责任处于非活跃状态主要有两种可能，一种是责任创建后未被要求履行，即$\text{create}(\text{debtor},\text{obligation})\wedge \neg \text{start}(Ca)$；另一种是责任在创建后曾被激活过，但现已不被要求履行，即环境$\text{end}(Ca)$有效，此时责任同样处于非活跃状态。

3) 活跃状态$\text{active}$，其可被形式化声明为active $\text{(obligation)}\leftarrow \text{active}(\text{debtor},\text{obligation})\wedge \text{start}(Ca)$。当责任被要求履行时，即环境$\text{start}(Ca)$有效，由$\text{debtor}$激活责任使其处于活跃状态。

4) 履行状态$\text{fulfilled}$，其可被形式化声明为$\text{fulfilled}(\text{obligation})\leftarrow \text{fulfil}(\text{debtor},\text{obligation})\wedge \text{start}(Ca)$。责任在激活环境下被$\text{start}(Ca)$履行后，责任处于履行状态。

5) 违反状态$\text{violated}$，其可被形式化声明为$\text{violated}(\text{obligation})\leftarrow \text{violate}(\text{debtor},\text{obligation})\wedge \text{start}(Ca)\wedge \text{start}(Cv)$。责任在激活环境和违反环境有效的条件下被$\text{debtor}$违反，则其处于违反状态。

6) 违反/非活跃状态$\text{violated}/\text{inactive}$，$\text{violated}/\text{inactive}(\text{obligation})\leftarrow (\text{violated}(\text{obligation})\wedge \text{end}(Ca)\wedge \text{deactivate}(\text{debtor},\text{obligation})$。责任被$\text{debtor}$违反后，在激活环境终止有效的条件下，$\text{debtor}$执行$\text{deactivate}$行为，使责任处于违反/非活跃状态。

7) 违反/履行状态$\text{violated}/\text{fulfilled}$，可被声明为$\text{violated}/\text{fulfilled}(\text{obligation})\leftarrow (\text{violated}(\text{obligation})\wedge \text{start}(Ca)\wedge \text{fulfil}(\text{debtor},\text{obligation})$。责任被违反后，且在激活环境有效的条件下被$\text{debtor}$履行，则责任处于违反/履行状态。

责任状态模型中的违反状态被定义为持久状态，即一旦责任的违反环境为真且$\text{debtor}$执行违反操作，则责任处于违反状态并在后续的状态演化中保持违反状态。

为了将OPL模型转换为NUSMV的输入模型，本文将OPL的操作语义定义为具有Kripke结构的状态迁移系统。

定义 3  迁移系统(transition system,TS)^[14]。迁移系统是一个六元组：$\text{TS}=(S,\text{Act},\to ,I,\text{AP},L)$，其中，S是系统状态的有穷集合，Act是系统动作的有穷集合，$\to \subseteq S\times \text{Act}\times S$表示状态迁移关系集合，$I\subseteq S$是系统初始状态的有穷集合，AP是原子命题的有穷集合，$L:S\to {{2}^{\text{AP}}}$是一个标签函数。

迁移系统中，系统状态由一组取值为真的原子命题集合表示，标签函数可以将一个原子命题集合$L(s)\in {{2}^{\text{AP}}}$关联到任意状态s∈S。对于一个给定的逻辑公式Φ，如果L(s)包含的原子命题使公式Φ成立，则称状态s满足公式Φ，即s |=Φ iff L(s) |=Φ。

定义 4  责任政策语言OPL的操作语义。$\text{OPL}=(A,O,C,\text{Action},R,\text{sta})$的操作语义是一个六元组：$\text{T}{{\text{S}}_{\text{OPL}}}=(S,\text{Act},\to ,I,\text{AP},L)$，其中，$S\subseteq (\text{sta}({{o}_{1}})\times \cdots \times \text{sta}({{o}_{n}}))\times C$是系统状态的有穷集合，$\text{Act=Action}$是动作的有穷集合，$\to \subseteq S\times \text{Act}\times S$表示状态迁移关系集合，$I\subseteq ({{\bullet }_{1}}\times \cdots \times {{\bullet }_{n}})\times C$是系统初始状态的有穷集合，AP是原子命题的有穷集合，$L:S\to {{2}^{\text{AP}}}$是标签函数。

在状态迁移系统$\text{T}{{\text{S}}_{\text{OPL}}}$中，系统状态集合S中的状态由当前时刻每个责任所处状态和责任政策的当前环境组成。系统初始状态由每个责任的初始状态和系统初始时刻的责任环境组成。$\text{T}{{\text{S}}_{\text{OPL}}}$的动作集合Act与OPL的动作集合$\text{Action}$定义相同，即$\text{Act}=\text{Ac}{{\text{t}}_{o}}\bigcup \text{Ac}{{\text{t}}_{c}},\text{Ac}{{\text{t}}_{o}}$是责任操作动作的集合，$\text{Ac}{{\text{t}}_{c}}$是责任内容中所执行动作的集合。在OPL中，$\text{Ac}{{\text{t}}_{c}}$中动作的发生导致责任政策环境发生变化，而$\text{Ac}{{\text{t}}_{c}}$中动作的发生导致责任状态发生变化，所以基于Act中的状态、动作执行序列可描述责任政策规则的执行以及责任状态的演变。AP集合中的元素是政策环境表达式与责任内容公式$\varphi $中的命题。

模型检测(model checking)^[14] 是一种自动验证有穷状态并发系统的形式化技术。在验证过程中，系统被建模为具有Kripke语义结构的状态迁移系统，系统规范被声明为模态/时序逻辑公式，当模型满足规范时验证算法给出肯定答案，否则算法会将导致错误结果的事件序列作为反例返回给用户，为系统漏洞定位和改进提供帮助。基于模型检测技术验证多Agent交互策略，首先要将交互策略模型转换为模型检测器的输入模型，本文选用基于Kripke结构作为输入的NuSMV作为模型检测工具验证交互策略。

NuSMV以模型描述程序和时态逻辑规范文本作为输入。若规范成立，则输出为真，否则显示一个轨迹，该轨迹解释规范为假的原因。NuSMV输入模型由一个或多个模块组成，其中一个模块必须被声明为主模块，每个模块都可由三部分组成：变量的声明、变量赋值以及性质声明。模块内部声明变量并对变量赋值，赋值操作通常给出变量的初始值，而变量下一个值是关于变量当前值的表达式。NuSMV建模语言的具体语法可参照文献^[14]。

本文基于OPL的操作语义，将其转换为NuSMV 的输入模型，转换过程中每个Agent被转换为输入模型的一个独立模块，并在主模块中初始化。各Agent的责任被建模为对应模块中的枚举变量，枚举值为责任的各个状态。各Agent的责任所关联的环境变量被转换为模块参数变量及其内部中的枚举变量和布尔变量，与责任状态相关的责任操作则被转换为状态演化的推理规则，这种迁移关系定义在各模块的ASSIGN部分，责任的内容动作被转换为迁移条件定义在模块的NEXT语句部分。

本文采用计算树逻辑CTL声明系统应满足的关键性质，CTL的语法定义如下：

定义 5  令p为原子命题，通过Backs-Naur范式定义CTL公式$\phi $为：

式中，路径量词A表示沿着所有路径(无一例外)；E表示沿着至少(存在)一条路径(可能)；时态算子X、F、G、U分别为下一个状态、未来某个状态、所有未来状态和直到。

系统被期望满足的性质主要包括安全性和活性性质，系统的安全性被描述为坏事$\phi $一定不会发生，其CTL公式形式为AG$\neg \phi $，系统的活性被描述为前提$\psi $成立时好事$\varphi $会经常发生，其CTL公式的形式为AG($\psi \to $AF$\varphi $)。

本文以《城镇企业职工基本养老保险关系转移接续暂行办法》为例(简称《暂行办法》)，作为多Agent交互策略，创建该策略的OPL模型。《暂行办法》对指导养老保险领域多Agent交互行为建模具有重要意义，限于篇幅，本文不对《暂行办法》的内容一一介绍，仅介绍与验证有关的重要内容，具体如下：

第三条给出了跨省流动参保人员达到基本养老保险待遇领取条件和未达到待遇领取年龄前，基本养老保险关系和个人账户的具体处理办法，特别强调了不得办理退保手续。

第四条规定了如何计算转移基金，增加了按照实际缴费工资的12%转移统筹基金，更好地平衡地方利益。

第六条规定了参保人保险关系不在户籍所在地，则累计缴费年限必须满10年，才可在保险关系所在地享受基本养老保险待遇。

第七条规定了参保人员转移接续后，符合待遇领取条件的按照国发2005年38号文的规定享受基本养老金，确保转移人员的基本养老金计算办法与其他参保人员的一致性。

《暂行办法》的OPL模型中，Agent集合A主要包括：社保经办机构PB和参保人GR。Agent GR的责任主要包括：参加保险${{n}_{1}}$，向管理机构登记${{n}_{2}}$，缴纳保险费${{n}_{3}}$，申请参保关系转移${{n}_{4}}$，领取保险待遇${{n}_{5}}$，退出保险${{n}_{6}}$。Agent PB的责任主要包括：同意转移参保关系${{n}_{7}}$，支付保险待遇${{n}_{8}}$，同意退保${{n}_{9}}$。各责任的形式化定义如下：

$\text{Obligation}=({{n}_{1}},\text{GR},\text{PB},{{\varphi }_{1}},\text{want }\!\!\_\!\!\text{ insured},\text{over }\!\!\_\!\!\text{ age }\!\!\_\!\!\text{ limit})$声明50周岁以下的参保人GR可以参加城镇基本养老保险，其中${{\varphi }_{1}}=\text{participating(GR},\text{endowment }\!\!\_\!\!\text{ insurance)}$声明参保人参加养老保险的行为，布尔型的环境$\text{want }\!\!\_\!\!\text{ insured}$声明参保人是否要参保，环境$\text{over }\!\!\_\!\!\text{ age }\!\!\_\!\!\text{ limit}\leftarrow \text{age}(\text{GR})>50$声明参保人年龄下限为50周岁。

$\text{Obligation}=({{n}_{2}},\text{GR},\text{PB},{{\varphi }_{2}},\text{insuranced},\text{not }\!\!\_\!\!\text{ alive})$声明参保人GR在社保经办机构PB登记注册，由PB管理GR，其中${{\varphi }_{2}}=\text{register}(\text{PB},\text{GR})$，环境$\text{insuranced}(\text{GR},\_,\_)\leftarrow \text{participating(GR},\text{endowment }\!\!\_\!\!\text{ insurance)}$声明GR处于参保状态，简写为$\text{insuranced}$。布尔型的环境$\text{not }\!\!\_\!\!\text{ alive}$声明GR已死亡。

$\text{Obligation}=({{n}_{3}},\text{GR},\text{PB},{{\varphi }_{3}},\text{insuranced},\text{retired})$声明未退休参保人GR在退休前向PB缴纳养老金，其中${{\varphi }_{3}}\text{=pay }\!\!\_\!\!\text{ fees}(\text{GR},\text{PB})$，布尔型环境$\text{retired}$声明GR是否处于退休状态。

$\text{Obligation}=({{n}_{4}},\text{GR},\text{PB},{{\varphi }_{4}},\text{insuranced}\wedge \text{want }\!\!\_\!\!\text{ transfer,retired})$声明未退休参保人GR向PB申请转移参保关系，其中${{\varphi }_{4}}\text{=apply }\!\!\_\!\!\text{ transfer}(\text{GR,PB})$，布尔型环境＜$\text{want }\!\!\_\!\!\text{ transfer}$声明GR是否要转移参保关系。

$\text{Obligation}=({{n}_{5}},\text{GR},\text{PB},{{\varphi }_{5}},\text{insuranced}\wedge \text{retired}\wedge \text{acc }\!\!\_\!\!\text{ payment }\!\!\_\!\!\text{ year,not }\!\!\_\!\!\text{ alive})$声明活着的已退休参保人达到缴费年限可领取社保机构支付的基本养老保险待遇，其中${{\varphi }_{5}}\text{=get }\!\!\_\!\!\text{ money}(\text{GR},\text{PB})$，布尔型环境变量$\text{acc }\!\!\_\!\!\text{ payment }\!\!\_\!\!\text{ year}$声明GR是否达到缴纳养老保险的累计年限。

$\text{Obligation}=({{n}_{6}},\text{GR},\text{PB},{{\varphi }_{6}},\text{insuranced}\wedge \neg \text{retired,not }\!\!\_\!\!\text{ alive})$声明未退休参保人退出养老保险，${{\varphi }_{6}}\text{=apply }\!\!\_\!\!\text{ quit}(\text{GR},\text{endowment }\!\!\_\!\!\text{ insurance})$。

$\text{Obligation}=({{n}_{7}},\text{PB},\text{GR},{{\varphi }_{7}},\text{insuranced}\wedge \text{want }\!\!\_\!\!\text{ transfer}\wedge \neg \text{retired},\text{not }\!\!\_\!\!\text{ alive})$声明PB同意未退休参保人GR转移参保关系，其中${{\varphi }_{7}}\text{=agree }\!\!\_\!\!\text{ transfer}(\text{PB},\text{GR})$。

$\text{Obligation}=({{n}_{8}},\text{PB},\text{GR},{{\varphi }_{8}},\text{insuranced}\wedge \text{retired}\wedge \text{achieve }\!\!\_\!\!\text{ payment }\!\!\_\!\!\text{ year},\text{not }\!\!\_\!\!\text{ alive})$声明PB支付已退休参保人GR养老保险待遇，其中${{\varphi }_{8}}\text{=pay}(\text{PB},\text{GR})$，布尔型环境变量$\text{achieve }\!\!\_\!\!\text{ payment }\!\!\_\!\!\text{ year}$声明参保人的累计缴费年限是否达到10年。

$\text{Obligation}=({{n}_{9}},\text{PB},\text{GR},{{\varphi }_{9}},\text{insuranced}\wedge \text{achieve }\!\!\_\!\!\text{ payment }\!\!\_\!\!\text{ year,retired})$声明PB同意撤销未退休但是已达到累计缴费年限的GR的参保关系，其中${{\varphi }_{9}}\text{=agree }\!\!\_\!\!\text{ quit}(\text{PB},\text{GR})$>。

根据OPL模型的操作语义及前文定义的转换关系，与《暂行办法》的OPL模型对应的NUSMV部分代码如图 3所示。

图  3  《暂行办法》的部分NUSMV代码型

该模型被期望满足性质的CTL公式为：AG((g.n₁=fufilled)->AF(g.n₅=fufilled))，其含义为如果Agent g履行参保责任，则其退休一定可以享受养老保险待遇。将该性质输入NuSMV执行验证，检测结果如图 4所示。

图  4  模型检测结果

图中，CTL公式的断言为False，表示《暂行办法》的NuSMV模型不满足该公式，即在《暂行办法》中存在参保人正常参保，退休后却不能享受养老保险待遇的情况，通过模型检测器的反例展示功能可获得验证反例的轨迹，如图 5所示。

图  5  验证反例的轨迹

分析验证反例可发现错误的原因在于《暂行办法》第六条规定参保人累计缴费年限必须满10年才可享受基本养老保险待遇。如果当前年龄在50岁以上的参保人，此前由于种种原因未能积累缴费年限，则不能享受保险待遇。《暂行办法》第三条又规定参保人员不能提前退保，因此这类参保人员面临着退休后既不能享受待遇又不能提前退保的尴尬境遇。

文献^[15]给出了一种基于RAISE建模语言和模型检测技术的领域政策形式化分析方法，该方法首先用RAISE建模语言构建领域政策的形式化描述，再将这种形式化描述转换为模型检测器SPIN的输入模型，同时将被验证性质声明为线性时序逻辑公式，最后使用SPIN自动验证政策模型对被验证性质的可满足性。文献^[15]同样以《暂行办法》为研究实例，并验证了政策的RAISE模型对线性时序逻辑公式声明性质的可满足性。本文的研究方法与文献^[15]对比，主要有以下不同：1) RAISE建模语言是一种软件工程领域通用的形式化语言，而本文设计的责任政策语言OPL是一种面向领域政策的专用建模语言，OPL相比RAISE建模语言更具备政策建模特质，且易于理解和使用。2) 文献^[15]将RAISE政策模型转换为模型检测器SPIN的输入模型。本文将OPL政策转换为模型检测器NuSMV的输入模型，文献^[15]只能验证线性时序逻辑公式声明的性质，而本文既能够验证线性时序逻辑公式声明的性质，又能验证计算树逻辑声明的政策性质，所以本文的方法可以验证比文献^[15]的方法更为广 泛的政策性质。

基于模型检测技术，本文提出一种多Agent交互策略形式化验证方法，用于验证多Agent系统中交互行为设计的正确性，该方法既使交互策略模型具备易于理解和使用形式语义，又能够自动验证设计模型的正确性。实验结果表明，该方法可有效地发现并解释策略模型中存在的错误，降低验证过程中的人工参与程度，提高验证效率。