《解释系统中认知属性的描述与验证工具》

《理论计算机科学电子札记》85卷2004年第URL：http://www.elsevier.nl/locate/entcs/volume 85. 第16页解释系统中认知属性的描述与验证工具Franco Raimondi和Alessio Lomuscio1伦敦大学国王学院计算机科学系摘要我们提出了一个编译器，它将解释系统的形式主义中给出的多代理系统规范转换为SMV程序。我们展示了SMV模型检查器如何我们应用这种方法来验证一个通信协议-用餐密码。1介绍传统上，形式逻辑被视为分析、表示和解释交流的有力工具随着分布式系统的出现，逻辑和形式化方法为研究与通信相关的问题的研究者提供了两种具体的工具：规范语言和验证机制。在分析人工语言的协议和话语意义时，逻辑被用作通信的特定语言，例如最近将言语行为理论应用于多智能体系统中的通信基于形式逻辑的形式化方法被用来作为分布式系统通信协议性质分析的验证机制本文关注的是后者使用基于逻辑的机器。通信协议的验证通常由定理证明器或模型检查器执行。虽然定理证明器是已建立的技术，但模型检查[8]是一种用于验证分布式系统的相对较新的技术，允许对属性进行机械验证。1Email：{franco，alessio}@dcs.kcl. AC. 英国这项工作得到了努伊特菲尔德基金会NAL/00690/G号赠款的支持2004年由E lsevierScie nceB. V. 操作访问和C CB Y-NC-N D链接。RAIMONDI和 LOMUSCIO2用时间公式表示的误差时态逻辑是一种强大的形式主义，但它的表达能力不足以表示我们在多智能体系统中通常关注的典型属性：特别是智能体的知识和其他态度，如欲望和意图。Halpern和M.Vardi在1991年建议使用模型检查技术来验证多智能体系统（[10]），通过更丰富的语言，不仅包括时态算子，还包括认知算子，但直到最近才实现了这些结果（[1，15，18，22，2，17，14，11，12]）。不管最近的研究，验证一个具体的通信协议，col仍然是一个不平凡的任务。首先需要给出一个具体的系统计算模型-无论是通过Petri网，时间自动机等，一旦这是给定的，需要一个工具，自动建立系统的语义模型。这个语义模型，通常是一个时态模型，然后必须用来解释用于指定和验证系统属性的语言虽然有一些工具可用，但据我们所知，目前还没有统一的平台，可以帮助设计师从具体指定代理的不同自动机到通过模型检查器验证属性，该模型检查器能够检查比普通时态逻辑更丰富的逻辑提供一个包罗万象的平台的困难在于，有几个问题相互交织：• 什么形式主义-自动机，Petri网-是用来表示在组件中产生的通信协议的过渡？• 什么时间模型-解释系统，简单的Kripke语义-被用来表示由系统的低层描述定义的计算路径• 什么样的逻辑语言--时间的、认识的、道义的--被用来表示所考虑的协议的关键属性？• 什么特定的符号表示- OBDD• 应该使用什么特定的模型检查器（NuSMV、Spin等）来协助完成任务？上文列举了许多相互竞争的备选办法，目前没有“正确的着手方式”，但在我们看来，对这些问题感兴趣的鉴于对上述问题的贡献，在本文中，我们提出了一个工具，将传统的模型检查技术与解释系统语义[9]相结合。解释系统是解释MAS的认知和时态性质的一种有力的形式化方法这里介绍的工具允许验证解释系统的静态认知属性我们认为，这在许多情况下是足够的;为了支持这一主张，我们将该工具应用于通信协议的验证-用餐RAIMONDI和 LOMUSCIO3密码学家[6]。论文的其余部分组织如下。在第2节中，我们回顾了本文其余部分中使用的主要技术结构。在第3节中，我们提出并讨论了检查MAS的认知属性的方法。在第4节中，我们详细介绍了允许我们这样做的工具。在第5节中，我们将展示如何在一个广泛讨论的示例中实现这一点- 吃饭的密码学家。2概念和符号2.1模型检测技术给定一个程序P，以及一个在某些逻辑可以表示为逻辑公式的属性，模型检查技术允许自动验证表示程序P的模型MP是否满足公式。在过去的二十年里，由于数据处理技术的进步，这种方法的有效性有了很大的提高。基于二元决策图（BDD，[3]）的技术已被用于开发能够检查大量状态的模型检查器（[4]）。使用自动机的替代方法也已经开发出来[20]。软件工具起源于这些研究领域。SPIN（参见[13]）利用自动机理论和相关算法，而SMV [16]使用BDD来表示状态和转换。在本文中，我们将使用NuSMV，SMV的一种新实现（[7]）。NuSMV的输入语言允许指定具有不同抽象级别的有限在最简单的情况下，输入语言需要三个主要部分：1. 变量声明部分2. 变量初始化部分3. 用于描述转换关系的部分以下是NuSMV程序的示例第二章：MONITOR主VARreturn： boolean;状态：{ready，busy};ASSIGNinit（state）：= ready;next（state）：=情况state=readyrequest= 1：busy;1： {ready，busy};esac;2来自NuSMV教程，可在http://nusmv.irst.itc.it上获得RAIMONDI和 LOMUSCIO4E(the行“1： {ready，busy};”等同于传统编程语言中的else给定上面的程序，NuSMV可以用来创建一个与之相关的模型，然后对时态公式进行模型检查。例如，如果我们要向NuSMV检查器提供CTL公式AG（（请求=0）-> AF（状态=就绪））3NuSMV将产生一个反例。按照这种方法，从通信协议到硬件组件的大量系统都通过时态语言进行了验证。这些不是代理系统，而是标准的分布式过程。如果我们要研究是否可以将这种方法应用于代理验证，我们需要将这种技术与基于代理的语义结合起来，如解释系统。2.2解释系统解释系统[9]是[21]意义上的基于计算的语义，旨在表示分布式环境中的代理我们在这里介绍主要的定义，但更多的细节请参考文献。考虑系统中的n个代理和n个非空集合L1，. ..LE. L i的元素将由l，lJ，l，lJ，.。。 LE的元素将是表示为lE，LJ，. 。。1122一 个 系 统 的 全 局 状 态 的 n 个 代 理 S 是 一 个 非 空 子 集 的 Cartesian 积L1×…×Ln×LE。 当g =（l1，.，ln，lE）是系统S的全局状态，li（g）表示全局状态g中代理i的局部状态。lE（g）表示全局状态g中的环境的局部状态。我们假设，对于系统中的每个代理和环境，存在代理和环境可以执行的动作的集合Acti和ActE动作不是随机执行的，而是遵循我们称之为协议的特定规范。代理i的协议Pi是从局部状态集Li到非空动作集Acti的函数（注意，通过考虑动作集，我们允许协议中的非确定性Pi：Li→ 2 Acti.然后，我们可以通过从全局状态和联合作用到全局状态的过渡函数π来π：S×Act→S其中S = L1×. ×Ln×LE和Act = Act1×... ×Actn×ActE是系统的联合动作的集合。直觉上，这定义了全局状态集合上的时间流具体地，我们考虑一组在全局状态R={r：IN→S}上的运行，其中3在公式中AG是“在所有分支中永远在未来”的模态算子RAIMONDI和 LOMUSCIO5游程r被定义为从时间到全局状态的函数，并且时间范围超过自然数。运行是通过将函数π应用于全局状态和联合动作而获得的全局状态序列解释系统可以用来对时间和知识进行为了做到这一点，考虑一个对IS=（S，h），其中S是一组全局状态，h：S→2P是一组命题变量P的解释函数。CTL [16]类型的时间连接词可以在解释系统上进行评估。为了本文的目的，我们关注的是认知算子。这些可以通过认知模态Ki来解释，每个智能体一个，如下[9]：（IS，g）|= Ki如果对所有gJ，我们有li（g）=li（gJ）蕴涵（IS，gJ）|= 0。由此产生的逻辑为模态Ki是S5n;这模型代理与完整的内省能力和真实的知识。我们将使用解释系统作为语义基础来指定MAS。他们也将在NuSMV的验证过程中代表。3解释系统中认知属性的模型检验方法虽然MAS理论包括各种态度，在本文中，我们专注于知识。能够验证系统的时间认知属性将使我们能够根据知识的时间演化以及关于变化世界的知识进行推理。我们认为，在特定情况下，验证静态属性是足够的。在前提条件和后置条件可以用逻辑命题表述的所有情况下，情况都我们在第5节中给出了一个例子。为了指定和验证MAS的认知属性，我们确定以下过程：(i) 根据局部状态、原型和转换来指定解释系统。 我们在第5节中给出了一个具体的例子，关于用餐密码学家的协议。(ii) 将步骤1的规范转换为SMV程序。这可以自动完成;可以使用Java程序（如下所示）来执行此转换。(iii) 使用模型检查器计算可达状态集。 给定状态和转换的符号表示，如前一步所获得的，可达状态集可以计算为固定点运算符[16]。NuSMV从版本中提供此功能2.1.请注意，可以在此阶段检查MAS的时间属性。(iv) 从可达状态。 的RAIMONDI和 LOMUSCIO6XML编辑器Java编译器NuSMV解析器Akka软件工具Fig. 1. 方法模型检查器的输出被用作原始解释系统的认知模型的定义的起点认识关系是自动建立的，通过我们编写的软件解析NuSMV的输出(v) 模型检验认知公式。在本文中，我们使用Akka4，一个支持LexHen- driks模型测试的Kripke模型编辑器Akka接受模型和评估函数的描述并且允许针对该输入来检查公式Akka对公式的语法没有限制，因此公式可以包含多个模态运算符，并且模态可以嵌套。模型和求值函数（采用Akka语法）由解析器在前一步中提供方法总结见图1。4将解释系统转换为SMV代码在本节中，我们将介绍用于将解释系统转换为SMV的工具我们首先陈述我们对规范所做的一些假设，然后简要描述该工具。4.1口译系统我们将注意力限制在具有以下性质的解释系统类上• 有限系统：我们考虑具有有限个局部状态和作用的系统。这是一个限制，但对于状态集有限的许多例子来说是足够的。• 初始配置：我们需要在设置模型时指定代理的数量，本地状态和动作因此，最大4http://turing.wins.uva.nl/指定解释系统将规范转换为NuSMV程序模型检验认知公式建立认知模型使用NuSMV计算可达状态RAIMONDI和 LOMUSCIO7本地状态的数量在运行时不能改变• 局部状态：我们假设局部状态可以表示为变量列表，每个变量都有一个有限的值范围 更详细地，考虑代理i：局部状态Li是元组Li= l，i，.其中每个vn，i的范围都在一组有限的值上（参见第5节的示例）。• 演化函数：在下面的描述中，我们对π使用了稍微修改和简单的语法（见2.2节）;其思想是分解函数π的最终全局状态。 我们考虑n个演化函数，每个代理一个，πi：S×Act→Li（i= 1，...，n）从全局状态和动作到代理i的局部状态。在这个工具中，我们将只列出导致个体i的局部状态发生变化的全局状态和动作，并假设，如果一个全局状态没有在某个πi的定义中列出，那么这个全局状态在Li的演化中是不相关的。4.2Java翻译器解释系统的规范需要作为Java翻译器的输入。该规范必须至少包含以下信息：1. 代理人数量2. 每个座席的本地状态和操作数3. 每个代理的每个本地状态中的变量数;本地状态中每个变量的值。4. 协议作为从局部状态（即变量集）到动作的函数，每个代理一个。5. 初始状态。6. 将函数从局部状态和动作转换为单个局部状态（参见上一节）。这些参数从XML文件中读取下面是解释系统的规格的示意图，如由翻译器5读取的：<为><代理名称=“Agt1”>[.][...][.]5解释系统规范的DTD可以在以下网址找到：http://www.dcs.kcl.ac.uk/pg/franco/is/is.dtd网站。RAIMONDI和 LOMUSCIO8[...][.]<联系我们协议和演化函数被指定为（局部状态，动作）和（全局状态+动作，局部状态）对的集合对于演化函数，我们假设如果没有列出全局状态和/或动作，那么它不会影响代理的局部状态的变化我们选择使用XML来指定解释系统，原因如下：• 解释系统的描述需要对简单的数据结构（如列表和映射）进行规范，而XML允许对这种半结构化数据进行• 大多数编程语言都可以免费使用解析器和检查器，因此可以更容易地与现有工具集成。• 建议的DTD可以根据新的要求进行扩展编辑XML文件可能很麻烦，我们目前正在开发一个图形界面，使参数的输入更容易。给定上面的输入，翻译器生成一个SMV程序;每个代理有两个变量，一个用于本地状态列表，另一个用于动作列表。局部状态是根据局部变量列表自动计算的。本质上，解释系统中的协议给出了计算SMV代码中动作演变的规则来自解释系统规范的演化函数用于创建表示局部状态的变量之间的转换函数所需的SMV代码块执行翻译的Java软件可以从本文的作者那里获得。5一个沟通的例子：The Dining Cryptogra Pher众所周知，解释系统提供了一个很好的抽象模型来指定和验证系统的行为在第4节中介绍的工具，除了作为规范编译的练习之外，还允许我们从解释系统的抽象描述到它的执行轨迹，其格式与领先的模型检查器之一兼容。RAIMONDI和 LOMUSCIO9我们对通过解释系统来指定系统感兴趣，因为我们认为它们在通信协议的验证中很有前途我们通过使用Chaum提供的Dining Cryptographers的场景来测试这个信念[6]。在他的论文中，Chaum展示了如何匿名广播消息特别是，他表明，协议的存在，允许在知识的参与者的一些全球性的财产系统的变化，与-出他们能够检测到这些信息的来源5.1问题陈述在[6]中介绍了用餐密码学家场景，如下所示："三个密码学家在他们最喜欢的三星级餐厅里坐下来吃饭.他们的服务员告诉他们，已经和酒店领班安排好了匿名付账。其中一个密码编写者可能会为晚餐买单，也可能是NSA（美国国家安全局）。这三个密码学家尊重对方匿名付款的权利，但他们想知道国家安全局是否在付款。 他们通过执行以下协议来公平地重新解决他们的不确定性每个密码破译者都在他的菜单后面，在他和他右边的密码破译者之间，放一个公正的硬币，这样只有他们两个人才能看到结果。然后，每个密码破译者都会大声说出他看到的两枚硬币--他自己刻的那枚和他左手边的邻居刻的那枚--是否落在了同一侧或不同侧。 如果其中一个密码破译者是付款人，他说的与他所看到的相反。 在餐桌上说出的数字为奇数表示密码学家付钱;偶数表示NSA付钱（假设晚餐只付了一次钱）。 然而，如果一个密码学家付钱，其他两个人都不会从关于哪个密码学家的话语中学到任何东西。“〔六〕请注意，相同的协议适用于任何数量的密码学家，无论是大于或等于三（见[6]）。5.2餐饮密码我们通过解释系统语义学来分析上面的场景 我们引入三个代理Ci，i ={1，2，3}，以模拟三个密码，和一个代理E的环境。在我们的表述中，环境用于（非确定性地）选择付款人的初始配置和硬币投掷的结果。我们用一个元组来表示每个密码算法Ci的局部状态LCiRAIMONDI和 LOMUSCIO10123LCi=1，v 1，v2，v3，其中6：初始状态v1=NotPaid（如果座席没有支付晚餐费用）如果代理支付晚餐费用，λ初始状态如果没有，则会出现以下情况v2=Ci的无权硬币如果左边的硬币等于右边的硬币，则等于λ初始状态v3=发出的差异的奇数偶数偶数的数字表示环境的局部状态是以下形式的元组LE：其中ChA、ChB、ChC是密码学家之间的“通道”，在运行开始时随机选择的如果为C，则为1 付了饭钱如果C付了晚餐的钱，付款人=03如果C付了餐费2004年，如果国家安全局支付晚餐密码学家的行动是：ActC1=ActC2=ActC3={λ， say（equal），say（not equal）}其中λ表示空操作。我们假设环境没有执行任何操作：ActE=λ。因此，不存在用于环境7的协议。[6]从现在起，我们将用λ表示空的或未定义的状态。7等价地，我们可以考虑一个协议，将环境的每个局部状态映射到空操作λ。RAIMONDI和 LOMUSCIO11用于密码学家的协议PCi是：如果LCi的形式为PCi（LCi）=未支付、相等、*或已付，不相等，*已付比如说（不相等），如果LCi的形式是未支付、不相等、* 不相等或支付，平等，*在所有这些情况下，现在我们定义系统的初始状态我们为代表密码学家的代理采取以下init（LC1）= init（LC2）= init（LC3）=λ，λ，λλ环境的初始状态是从通道（头或尾）和付款人（密码学家或NSA之一）的值的可能组合集合中随机选择的系统的演化可用跃迁函数π：G×Act→G来描述，其中G=LC1×LC2×LC3×LE是全局态集，Act=ActC1×ActC2×ActC3×ActE.请注意，我们可以跳过LE的演变以及在π的定义中对ActE的依赖性，谢谢我们对环境的假设（没有动作，运行开始时即便如此，π的定义也太长了，无法报道;我们在这里只举两个例子：π（πλ，λ，π头，尾，头，1π，λ）=（已付，未付，未付，已付，λ未付，λ未付，未支付，迪埃雷伦特，λ头，尾，头，1个）上面表示了这样的事实，即在初始状态下，其中硬币投掷的结果分别是ChA、ChB和ChC的头、尾、头，并且其中第一个密码学家支付了晚餐，存在到这样一种状态的过渡，密码学家有NotP援助。在下一个时间步骤中，密码学家按照他们的协议说出适当的句子（相等或不相等）这将使过渡RAIMONDI和 LOMUSCIO12最后一个变量v3的求值：π（Paid，NotEqual，λ，， NotPaid，NotEqual，λ，未支付，不相等，λ头，尾，头，1英尺，说：说：（8年以前）=（已付，不相等，奇数，不支付，不相等，奇数，不支付，不相等，奇数，头，尾，头，1个）这是系统的最终状态可以对所有其他案件进行类似的分析5.3实践中的方法论根据上述考虑，我们将餐厅密码学家的解释系统编码为XML文件。具体地说，它包含四个代理，三个变量用于密码学家的局部状态，四个变量用于环境，两个动作用于密码学家。演化函数的定义是最繁琐的一步。然而，由于我们在4.1节中的假设，我们只能指定全局状态和实际导致局部状态变化的动作。例如，在这种假设下，第一个密码可以用以下形式的转换来建模：已付，相等，λ或（λ，，1，Tail，Tail，，），（）这代表了这样一个事实，即第一个密码学家只有在本地状态为λ，λ，λ且环境为1，Head，Head，或1，Tail，Tail，时，才会将其本地状态更改为Paid，Equal，λ。类似地，可以定义导致第一个密码学家转换的所有剩余条件;这些条件以及其他密码学家和环境的转换都被编码成XML，供Java翻译器使用。我们可以将这个规范输入到翻译器中，并生成示例8的SMV代码。NuSMV然后可以用于生成可达状态的集合。对于这个例子，这些是629856个本地状态和动作的可能组合中的96个，因为它们在NuSMV中表示两8.这份文件的内容见http：//www.dcs.kcl。AC. 英国/英国/法国/意大利2. smv.RAIMONDI和 LOMUSCIO13在具有256 MB RAM的500 MHz PC上，将规范转换为SMV代码和计算可达状态集所需时间可达状态存储在一个文本文件中，解析器可以处理该文本文件以产生Akka格式的认知模型ISd5.4公式的模型检验我们定义了一组原子命题{paid1，paid2，paid3，even，odd}，我们可以在通过上述过程获得的模型ISd中以自然的方式解释它们注意，在协议终止时，{even，odd}为真，从而给出了评估认识公式9所需的后置条件：（ ISd ， g ） |= paid1if lC1 （ g ） =Paid ， paid ， paid （ ISd ， g ） |=paid2if lC2 （ g ） = Paid ， paid ，paid，paid（IS d，g）|=已付3，如果lC2（g）=已付，已付（ISd，g）|= even if lCi（g）=，，even for every i（ISd，g）|=奇数如果lCi（g）=n，n， Oddn，对每个i使用Akka，我们可以很容易地检查以下命题：是d|=奇数→（€paid1→（KC1（paid2paid3）∧€KC1（paid2）€KC1（paid3）是d|=偶数→ KC1（<$paid1<$paid2<$paid3）这两个公式证实了第5.1节的陈述的正确性：如果第一个密码学家没有为晚餐买单，并且在话语中有奇数个不同，那么第一个密码学家知道第二个或第三个密码学家为晚餐买单;此外，在这种情况下，第一个密码学家不知道剩下的密码学家中哪一个是付款人。相反，如果话语中的差异数是偶数，那么第一个密码学家就知道没有人为晚餐买单。有趣的是，在我们的模型中，以下内容是无效的：ISd/=|<$paid1→（KC1（<$paid1<$paid2<$paid3））∨（KC1（已付2）KC1（已付2）KC1（已付2）9在下文中，g将表示全局状态;lCi（g）将表示全局状态g中的密码器i的局部状态; l C i（g）将是局部状态，其中第一个变量是Paid和所有其他变量都允许有任何值。RAIMONDI和 LOMUSCIO14此外，我们还有：ISd/=|<$paid1→（KC1（<$paid1<$paid2<$paid3））∨KC1（已付2人，已付3人）实际上，考虑一个全局状态，其中C1的局部状态是NotPaid，Di在这种状态下，支付1不成立;而且，在这种局部状态下，没有关于话语奇偶性的信息，并且C1考虑奇偶性为奇数的可能全局状态，以及奇偶性为偶数的其他全局状态。在第一种情况下，<$paid1<$paid2<$paid3在C1认为可能的全局状态下不成立。在第二种情况下，paid2=paid3是假的，因此KC1（paid2=paid3）无效6结论逻辑一直用于分析多智能体系统中的通信到目前为止，通信协议的验证仅限于使用定理证明器，模型检查器仅限于时态语言。虽然这适用于网络中使用的低级通信协议，但在精神上遵循意向立场的复杂多代理系统需要更丰富的语言。使用更丰富的语言来验证这些协议的问题是，目前的证明器和检查器不适合表示其他形式，如知识。在本文中，我们试图在这个方向上迈出一步，通过提供一条从多代理系统的具体规范到执行轨迹的构建和属性检查的路径具体来说，我们在这里提出了一个工具，用于多智能体系统中的模型检查我们使用解释系统作为MAS规范的框架，并建议如何使用时态模型的模型检查器（NuSMV）来验证认知属性。讨论了提供必要翻译的软件工具所提供的工具已经在通信中的一个众所周知的场景上进行了测试：用餐密码学家的协议。在未来，我们希望测试其他场景，特别是从安全文献。在这个练习中，检查静态分析是否足够（正如[5]在他们关于BAN逻辑的基本论文中所声称的那样），或者是否需要转移到时间认识论，这将是有益的在进行分析的同时，我们目前正计划为工具添加一个图形界面，以便可以图形化地给出解释系统的规格。这种方法的可扩展性问题也是我们想进一步研究的问题初步结果似乎表明，RAIMONDI和 LOMUSCIO15编译成SMV，构建全局状态集，以及测试认知公式都可以相当好地扩展。尽管如此，我们不期望这种方法在速度上与最快的方法进行比较。我们在这里发现的有趣之处在于，通过将一个规范自动编译为另一个规范，在协议的规范和模型检查之间建立了一座桥梁，从而允许验证认知属性引用[1] M. Benerecetti ， F. Giunchiglia 和 L. Sera fini. 多 智 能 体 系 统 模 型 检 验 。Journal of Logic and Computation，8（3）：401[2] R. H. Bordini，M.费希尔角Pardavila和M.伍尔德里奇模型检查AgentSpeak。第二届自治代理和多代理系统国际联合会议（AAMAS'03），2003年7月。[3] R. E. 布莱恩特基于图的布尔函数操作算法。IEEE计算机学报，第677-691页[4] J. R. Burch，E. M. Clarke，K. L. McMillan，D. L. Dill和L.黄哲伦符号模型检查：1020个状态及以上。Information and Computation，98（2）：142[5] M. Burrows，M. Abadi和R.李约瑟认证的逻辑。 ACM Transactions onComputer Systems，8（1）：18[6] D.乔姆用餐密码问题：无条件发送者和接收者不可追踪性。Journal ofCryptology，1：65[7] A. Cimatti，E.克拉克角，澳-地Giunchiglia和M.罗维里NuSMV：一个新的符号模型验证器。计算机科学讲义，1633，1999。[8] E. M. Clarke，O.Grumberg和D.A. 佩尔德。模型检查。麻省理工学院出版社，马萨诸塞州剑桥，1999年。[9] R. Fagin，J. Y. Halpern，Y. Moses和M. Y.瓦迪关于知识的推理麻省理工学院出版社，剑桥，1995年。[10] J. Halpern和M.Y. 瓦迪模型检查与定理证明：一个宣言。在j.艾伦河E. Fikes和 E.Sandewall， 编 辑 ， Proceedings 2nd Int. 知识表 示 和 推 理 的 原 则 ，KR'91，摩根考夫曼系列知识表示和推理，第325-334页。Morgan KaufmannPublishers，San Mateo，CA，1991.[11] W. van der Hoek 和 M. 伍 尔 德 里 奇 模 型 检 查 知 识 和 时 间 。 SPIN 2002-Proceedings of the Ninth International SPIN Workshop on ModelCheckingof Software，Grenoble，France，April 2002.RAIMONDI和 LOMUSCIO16[12] W. van der Hoek和M.伍尔德里奇认知目标的易处理多智能体规划。In M.Gini，T.石田角Castelfranchi和W. L. Johnson，editors，Proceedings of theFirstInternationalJointConferenceonAutonomousAgentsandMultiagent Systems（AAMASACM Press，2002.[13] G. J. Holzmann。模型检查器旋转。IEEE软件工程学报，23（5），1997年5月。[14] A. Lomuscio和W.彭切克解释系统的有界模型检查技术报告，波兰科学院计算机科学研究所，2002年。[15] A. Lomuscio，F.Raimondi和M.塞尔戈对解释系统进行模型MoChArt会议记录，法国里昂，2002年8月。[16] K. 麦克米兰符号模型检查：状态爆炸问题的一种方法。Kluwer AcademicPublishers，1993.[17] R.范德 梅登和 N.V.希洛 夫。完 美召回 系统中 的模型 检查知 识和时 间。FSTTCS：软件技术和理论计算机科学的基础，1999年。[18] R.范德迈登和苏凯尔。符号模型检验密码学中的用餐知识。2002年提交[19] Freek Stulp和Rineke Verbrugge。基于知识的互联网传输控制协议（TCP）（扩展版）算法。 Bulletin of Economic Research，54（1）：69BlackwellPublishers Ltd，Oxford，UK and Boston，USA.[20] M. Y. 瓦 迪 协 议 验 证 的 自 动 机 理 论 方 法 （ 摘 要 ） 。 在 国 际 并 发 会 议（CONCURRENCY斯普林格。[21] M.伍尔德里奇代理的计算基础理论。在大肠Durfee，编辑，ICMAS，多智能体系统国际会议论文集。IEEE Press，2000.[22] Michael Wooldridge ， Michael Fisher ， Marc-Philippe Huget 和 SimonParsons 。 使 用 MABLE 对 多 智 能 体 系 统 进 行 模 型 在 Maria Gini 、 ToruIshida、Cristiano Castelfranchi和W. 刘易斯·约翰逊，编辑，第一届自治代理和多代理系统国际联合会议（AAMAS'02），第952-959页。ACM Press，2002.