BDI体系结构的验证承诺策略问题及解决方法

126理论计算机科学电子笔记70第5期（2002）网址：http://www.elsevier.nl/locate/entcs/volume70.html14页BDI体系结构Tadashi ARARAGIa，1 Shiro Takatab，2 NIDE Naoyukic，3aNTT通信科学实验室Hikaridai 2-bATR媒体信息科学实验室Hikaridai 2 - 2奈良女子日本奈良县奈良市北宇屋西町630-8506摘要我们提出了一种方法来解决在实现中出现的验证问题，BDI架构的承诺策略。这个问题引入了验证的一个新方面，使得状态转换依赖于完成的验证在每个州。我们形式化这个问题，并给出一个验证的决策过程。1介绍在本文中，我们提出了一种方法来解决一个新的验证问题时出现的承诺策略[6]的BDI架构[8，9]。BDI体系结构是一个代理系统的模型，并引入了信念，愿望和意图的概念，实现灵活的计划描述的代理。BDI架构中的一个重要概念是其承诺策略。承诺策略要求代理人保持他们的意图，只要预期的目标在未来被认为是可能的。换句话说，如果代理人发现他们的意图在未来无法实现，他们就会放弃当前的意图。该策略使Agent为了实施承诺策略，特别是所谓的一心一意[6]类型，我们需要一种方法来预测一个或多个意图的可行性1电子邮件地址：araragi@cslab.kecl.ntt.co.jp2电子邮件地址：shiro@atr.co.jp3电邮地址： nide@ics.nara-wu.ac.jp2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。阿拉拉吉127已经有许多实现反映了信念、欲望和意图的演绎过程。利用BDI逻辑[7，5]的演绎机制，我们可以令人满意地实现这些过程，从而执行计划。不幸的是，一心一意的承诺战略没有得到充分执行。还有其他的作品，处理承诺的时间逻辑和动态逻辑的框架内。但是，目前，这些工作的AD-Dress，行为的BDI代理的分析，并提供没有实际的指导，以实现承诺战略的BDI架构。本文的目的是全面实施一心一意型的承诺战略。我们将预测意图的可行性问题作为代理程序的验证问题来处理。这个验证问题具有复杂的递归结构，因为智能体未来的行为也取决于对当时意图的评估。因此，这个验证问题与传统的验证问题完全不同[4，1，2]。在本文中，我们称这种类型的验证承诺验证。本文第2节非正式地介绍了这个问题，然后通过将连接/断开赋值的概念引入到Agent程序的状态转移树中来将其形式化。在本节之后，第3节给出了一些典型的估值例子，我们讨论了估值。第4节描述了一个基于表格方法的决策过程，该过程的正确性在第5节中显示2承诺验证2.1非正式介绍承诺验证已经提出了BDI架构的许多实现。我们可以通过忽略每个实现的特征，以下面的形式总结这些实现的本质。• BDI代理的状态是一组BDI公式• BDI代理的程序是一组计划规则，其中每个规则都有一个先决条件来检查代理的当前状态，以及如果检查结果成功则执行我们在下面给出一个计划规则的例子。BEL（realize（agent1，φ1））&INTEND（φ1）=send（agent1：reuest（φ1）），add（INTEND（φ2））这条规则的含义如下。如果持有这一规则的代理人，我们称之为代理人0，相信代理人1可以实现φ1，并打算执行φ1，那么代理人0向代理人1发送消息，要求代理人1代表阿拉拉吉128代理0创建一个新的意图φ2，以支持代理1实现φ1。例如，如果代理0{BE L（reIiable（a gent1）），BEL（reIi a b le（x）→reIi ze（x，φ1）），INTEND（φ1）}，则规则被启用。每个代理选择一个启用的规则并执行it。如果座席0选择此启用的规则，则状态变为{BEL（reliable（agent1））， BEL（reliable（x）→realize（x，φ1）），INTEND（φ1），INTEND（φ2）}。通过使用BDI逻辑的一个定理证明器[5]，我们可以在这个框架中实现信念、愿望和意图的那么，承诺呢？在这个例子中，如果我们考虑一个承诺策略，特别是一心一意的承诺，我们必须判断φ1在未来是否可能。可以有各种标准来判断这种可能性。 在本文中，我们采取了一个形式化的标准。 也就是说，我们计算状态转移图从给定的程序和当前状态中获取代理，并检查φ1在未来是否可能。这被简化为程序验证的问题。然而，这种验证与普通的程序验证之间存在着巨大而重要的区别。在BDI代理的状态转换中，承诺策略被应用于每个转换，在这个应用中，我们需要另一个抢先验证。也就是说，每个转换都取决于另一个验证的结果。很明显，验证对承诺的应用具有递归结构。实现这种验证的第一个问题是如何将其形式化。2.2承诺验证2.2.1代理状态和代理程序• 代理状态是BDI逻辑公式的有限集合• 代理程序是一组有限的计划规则。计划规则具有以下形式：前提条件1，前提条件2=条件动作1，动作2，···前提1和前提2是命题BDI逻辑公式。这些公式的有效性wrt检查的代理的当前状态。如果preconditon1是有效的，而preconditon2不是，那么我们说规则在所讨论的状态下被启用前提条件2在计划规则的前提条件中起到表示否定的作用以下是使用前提条件2的计划规则的示例。BEL（φ1），INTEND（φ2）=add（INTEND（φ3））阿拉拉吉129¬···这个规则意味着φ2和φ3作为意图是互斥的有两种类型的行动。第一个动作修改其主体第二个与外部世界交互，例如向其他代理发送消息，并改变代理通常可观察到的世界状态。[简化约定]为了简单起见，我们对计划规则施加了两个限制。(1) 每个前提条件是一个正BD公式或一个正BD公式与一个I-主公式的结合。在这里，正BD公式是由BEL、BELRE、或和命题变量构造的公式，I-主公式是INTEND（正BD）形式的公式公式）。为了使关于承诺验证的讨论更简单，我们还假设I公式最多出现在前提条件1中的一个中在给定的规则中，前提条件2如果INTEND（φ）作为合取的一部分出现在前提1或前提2中，我们分别称[φ]或[φ]为规则的支持公式(2) 计划规则不包括涉及与外部世界交互的操作处理这样的相互作用会给智能体的状态转移带来非确定性。我们可以在验证中处理这种非决定论，但它使论证变得复杂。因此，本文将省略这一部分。2.2.2抢占式状态转移图和树定义：我们首先定义规则r和状态s的抢占式状态转换图（简称pe图），换句话说，我们将展示如何构建pe图。我们首先使初始节点n对应于s，初始边e对应于r。对于e的结束节点NJ，我们将r的动作应用于s所产生的状态。接下来，让规则r1，我们创建p条边，nJ对应于每个ri，并且将通过将边的规则应用于nJ而得到的状态附加到结束节点。 我们反复应用这个程序到新创建的节点。在这里，如果两个节点的连接状态相同，我们就可以识别它们;这就产生了一个有限图。规则r和状态s的抢占式状态转移树（简称pe树）是通过将r和s的pe图扩展为树的形式而获得的。见图1.一、给树T的每条边赋值“C“或“D“的映射对于边，C表示C也意味着对应于边的规则在该状态下执行。我们为pe树准备了一些符号。 设e是pe树的边，n、n1和n2是PE树的节点。 end（e）是e的结束节点。 spf（e）是指阿拉拉吉130n1[2011 -[2014 -n[2012 -02 -025n 3[2014 -04 -n1[2011 - 01 - 21n2n2n4n4n1[2011 - 01 - 21n2[2012 -02 -02n3[2013 -03 -23n5n2n4[2012 - 02 - 02n3[2012 - 02 -02n4n3[2013 - 03 - 23[2013 - 03 - 23Fig. 1. pe图和pe树e对应的计划规则的支持公式。g_id（n）和g_id（e）分别是原始PE图中n的图节点id和e的图边id。 [n1，···，n2]是pe树中从n1到n2 （n1，···，n2]是不包括n1的，[n1，···，n2）是不包括n2的.我们直观地解释了价值C和D的作用，以及为什么这种承诺验证与传统验证非常不同。设一个智能体处于状态st，并想执行一个计划规则，该规则在其预测1中包含一个意图I（φ1）。设相应的跃迁为e1，即spf（e1）=[φ1]。 如果智能体服从承诺策略，它必须判断如果φ1是可能的或不是在未来从st.然后根据代理程序，从st扩展pe树。让智能体认为φ1在未来是可能的吗？ 在这个时刻，我们不能说让，其对应的规划规则依赖于另一个意图I（φ2）。如果智能体判断从st2到φ2在未来是可能的，那么转移e2被连接（标记为C），并且从st到φ1在未来是可能的，假设在st和st1之间没有取决于意图的其他转移。否则，e2是不连通的（标记为D），并且φ1在未来不可能从st。使验证更加复杂的是，在st2的判断还取决于包括inten在内的转换的连接和断开，并且连接和断开再次涉及对来自这些状态的未来的判断。阿拉拉吉131¬|为了形式化连接/断开和判断之间的关系，我们在下面引入一致赋值的概念定义：设T是一棵pe树，V是T的一个赋值。 边ewrtV的子树是T的子树，其根是e的结束节点，并且其节点是T的那些可以从根通过值为C的边由V到达的节点。我们用T（e，V）表示子树。定义：设T是一棵pe树，e是T的一条边，V是T.设[φ]或<$[φ]为e的支撑公式。 我们写T（e，V）|= EFφ如果对于T（e，V）中的某个节点n，n<$φ成立。这里n<$φ表示与n相连的代理状态逻辑地导出φ。 我们也写T（e，V）|否则=<$EFφ。定义：设T、V和e为上述定义中的给定我们说e如果满足以下条件之一，则V满足• spf（e）=[φ]V（e）= C和T（e，V）|= EFφ，或V（e）= D和T（e，V）|=<$EFφ• spf（e）=<$[φ]的情况V（e）= D和T（e，V）|= EFφ，或V（e）= C和T（e，V）|=<$EFφ注意spf（e）= [φ]和V（e）=D的组合给出了最终性质。我们说V是T的相容赋值，如果T的每条边都满足V。现在，我们来正式定义承诺验证。定义：计划规则r在状态s启用承诺，如果r在s上有一个一致的赋值，它对于T的初始边的值是C。3示例和讨论在本节中，我们给出了pe图、pe树及其赋值的一些典型例子。图2中的示例（a）示出了具有不同估值的pe图和相关联的pe树。在这种情况下，PE树是有限的。pe图表明φ1在end（e2）有效，φ2和φ3在end（e3）有效，以及spf（e1）= [φ1]，spf（e2）=<$[φ2]和spf（e3）= [φ3]。 在左PE树中，我们对于初始边e1，第一个集合V（e1）=C。因此，要使赋值一致，V（e2）必须是C，因为V（e1）= C和spf（e1）= [φ1]要求T（e1，V）|= EFφ1，且end（e2）<$φ1。接下来，为了在一致赋值中设置V（e2）= C，V（e3）必须是D，因为V（e2）= C和spf（e2）=<$[φ2]需要T（e2，V）|=<$EFφ2，且end（e3）<$φ2。另一方面，end（e3）<$φ3意味着T（e3，V）= EFφ3和spf（e3）=[φ3]。这些事实产生V（e3）=C，并与上面的结果相因此，没有一致的估值其中V（e1）=C。 在右边的pe树中描述的估值很容易被检查，阿拉拉吉132123（一）42（b）第（1）款e1[2011年1月1日]e1 C鄂e1[2011年1月1日]2 2Ce[]e2[2012 - 02 - 02]（c）第（1）款e3De4 De5 C2e3e4（d）其他事项2[2013年12月3日][2014年10月4日]图二、pe图，pe树和赋值的例子保持一致。因此，对应于边e1的计划规则不是启用提交的，并且代理在此时不执行它例子（b）显示了一个pe图，其关联的pe树是无限的。该pe树示出gid（eJ1）= e1，g id（eJ2）= e2，. . .和end（e1）φ2和end（e2）φ1，以及spf（e1）=<$[φ1]和spf（e2）=<$[φ2]。在这个例子中，我们可以通过设置V（eJi）=C来获得与V（eJ1）= C一致的赋值，如果如果g id（eJi）=e 2，则g id（eJi）=e1和V（eji）=D是一致的，而在例子（c）中我们不能。在例子（c）中，如果我们设置V（eJ1）=C，则V（eJ2）=C是上述相同讨论所要求的。同样，V（EJ2）=C需要V（ej3）=D，V（EJ3）=D需要V（ej4）=D，V（EJ4）=D需要V（EJ5）=D。在此之后，我们通过定期执行剩余的设置来获得一致的估值这例子说明了为什么我们必须引入PE树，除了PE图，以适当地讨论抢占式决策。即使两个代理状态是相同的，我们可以对他们采取不同的行动，如果他们被认为是发生在不同的时间在未来。在例子（d）中，我们可以给出一个一致的赋值，它给初始边赋值D，但不给C赋值。在例子（c）中，我们提到了估值的周期性。一般来说，每个一致赋值都有一定的周期性，但它有点复杂，我们需要更多的概念来形式化它，我们将在第二节介绍4. 在第5节中，我们还将展示如何在pe树中定位周期性。正如我们在引言中指出的，承诺核查与传统核查有很大的不同。1231 42e1 e1Ce1 [2011年1月1日]e1Ce1D1e2 e2De1[2001]e3 e1Ce2e3[2012 - 02- 02][2013年12月3日]e2e3CD Ce2e3DC2e2[2012 -02 -02]e'e5ee1DC阿拉拉吉133¬¬¬∗¬4承诺验证的决策程序我们准备了一些定义来引入一个用于承诺验证的决策过程。定义：设T是一棵树，n是T的一个节点。n的周期是从n到具有与n相同的pe图节点id的n的后继节点的最小距离。T的周期是当n在T中的所有节点之间变化时n的周期的最大值。 显然，T的周期是有限的。定义：对于pe树T的边的请求集合是一对集合：EF-集合和EF-集合。EF-集是一个公式集，它的元素是φ，对于某个支撑公式[φ]或[φ]. EF-set是长度不超过T的周期的pe图节点id的列表。很明显，可能的请求集的数量是当T被给定时，定义：边e的抢占索引（简称pe索引）是end（e）的图节点id、附加到e的请求集和给定的值C或D的三元组与大肠我们用M表示可能的pe索引的数量的上界。在下文中，我们将介绍承诺验证的决策程序。我们以后称这个过程为CM验证。当一个代理程序，代理的当前状态，以及一个寻址的计划规则被给定用于CM验证时，我们可以以规范的方式创建一个pe图。然后我们可以从pe图扩展pe树T。在决策过程中，我们给T的每条边一个值C或D，从根到它的后继者递增。我们使用表格法有效地并行定位了一致赋值。表中的分支是T的部分赋值，并且为每条边携带请求集以保证赋值的一致性。这些计算有两点第一，要保证公平，我们只在一些固定的地方寻找见证人（以EF距离：T的周期，用L表示。 第二，为了保证不可避免的属性（用EF-集表示），我们检查树的固定深度：深度等于一种估值周期，作为值LM。我们在第5节中给出了这些观点的理由步骤1：tableautab：=[br0]，其中br0是T的初始边，其值为C，它的EF-集和<$EF-集都是空的.步骤2：如果选项卡为空，则返回从标签中取出一个分支从br中选择一个叶子边e。阿拉拉吉134¬¬···¬¬►\···¬¬步骤3：让tmp tab1为空列表。如果e的值为C且spf（e）=[φ]，或者e的值为D且spf（e）=[φ]，则找到满足以下条件的节点n。• n是e的后继者，并且从end（e）到n的距离不大于L。• n∈φ，并且对于[end（e），·· ·，n）中的每一个n∈ nJ，nj满足nJ∈φ• 对于每个nJin（end（e），···，n]和每个φJin <$EF-set（e），nJ满足nJ\φJ设n1，，np是满足这个条件的节点。如果没有这样的节点，请从选项卡中删除br并转到步骤2。制作br：br1、···、brp的p个副本。对于每个bri，将列表[g id（end（e）），···，g id（ni）]添加到EF-set（e）。将所有bri添加到tmp选项卡1。如果e具有值C且spf（e）=[φ]，或者e具有值D且spf（e）=[φ]，则将φ添加到EF-set（e）。将br添加到tmp选项卡1。第4步：将步骤（1）和（2）应用于tmp tab1中的每个元素。(1) 检查是否对于EF-set（e）中的每个φJ，end（e）满足end（e）φJ。如果此检查失败，请从tmp选项卡1中删除br(2)删除EF-set（e）中每个列表的head元素。如果一个列表是空的，我们从EF-set（e）中删除这个列表如果tmp选项卡1变为空，请转到步骤2。步骤5：5.1让tmp tab2为空列表。对tmp tab1中的每个元素应用以下过程对于T中从end（e）开始的每个边eJ，如果end（eJ）具有与EF-set（e）中的列表的某个头元素相同的图id，则将值C赋予eJ。设e1，，eq是T中从end（e）开始的不满足上述条件的边。 接下来，制作br的2q个副本，并为每个ei赋予值C或D，以便用尽所有可能性然后将所有新创建的分支添加到tmp tab2。5.2将以下过程应用于tmp选项卡2中的每个元素对于在T中的结束（e）处开始的每个边EJ，如果它的值是C，我们将EF-set（eJ）设置为EF-set（e），并将EF-set（eJ）设置为EF-set（e）中的列表集合，其头部元素与end（eJ）的g id否则，如果其值为D，则将EF-set（eJ）和<$EF-set（eJ）设置为空。阿拉拉吉135∗¬en2n1n 2n1图三.（nj1，n1）第6步：如果第2步的br在第2步到第5步的过程中没有变化，即br完全展开，则返回如果对于tmp tab2中的某个分支，br的根节点到叶节点的最短长度大于L M，则返回否则，将tmp tab2附加到tab并转到步骤2。在这个过程中，我们假设每条边都有一个支撑公式。实际上，某些规则可能不依赖于任何意图。在这种情况下，相应的边没有支撑公式，我们给边赋值C。由于出现在此过程中的分支的大小受步骤6中的终止条件的限制，因此此过程最终终止。5CM验证的正确性定义：设T是一棵pe树，e是T的一条边，n1是e的后继，L是T的周期。如果n1到e的端节点的距离大于L，则存在满足以下条件的节点n2，nJ1，nJ2(1) n1和n2具有相同的图id，并且n2到e的端节点的距离等于或小于L。(2)NJ1和NJ2具有相同的图id，NJ2在从e的端节点到n 1的路径上，并且对于从NJ1到n1的路径：[nJ1，···，n1]和从nJ2到n2的路径：[nJ2，···，n2]，[gid（nJ1），···，gid（n1）]等于[gid（nJ2），···，gid（n2）]，其中gid（n）是n的图id。我们称（nj2，n2）为e的（nj1，n1）的邻路. 见图3.第三章。定义：设T是一棵pe树，V是T的一致赋值。对于T的任意边e，如果e具有支撑公式[φ]或[φ]，且e分别由V给定值C或D，则根据V的相容性，存在节点n使得n可以从e的结束节点仅通过其值为C的边到达在V中，n满足nφ。设n1是离e最近的节点，满足阿拉拉吉136►¬en2e2De1Cn2n1n1en2e2Ce1Cn2n1n1图四、边赋值的修正以上条件。如果e的端点到n1的距离大于T的周期，则取n2，nj2和nj1，使得（NJ2，n2）是e的（nj1，n1）的邻路.设e2是从nJ2到n2的路径中具有值D的第一条边。设e1是相应的边，换句话说，在从NJ1到n1的路径中的相同位置。然后，我们用边e1下的值替换边e2下的值（见图2）。4）.我们称这种替换为e对V的修改。引理：设T是一棵pe树，e是T的一条边，V是T的一个一致值。由e修正V所得到的赋值也是T的相容赋值。证明：我们使用上述定义中的符号。让我们假设修改给出了一个不一致的估值。然后有一条边EJ是e2的祖先，它不满足修改后的赋值VJ。我们只考虑spf（EJ）= [φ]的情况。另一个案例也是类似的。 如果V对EJ的取值是C，这种情况不会产生任何不一致，因为修改扩展了连接到EJ的节点集。如果值为D，则在e2下的子树中存在满足n φ的节点n，并且n连接到EJ。而且，EJ是e的祖先，因为e和e2是相连的，也就是说它们之间的所有边都具有值C。设NJ是e1下的子树中对应于n的节点。因为eJ连接到n，所以e1连接到nJ，从而连接到e。这意味着V已经不一致了。定义：pe树T的赋值V是L-相容的，如果V是T的相容赋值，并且对于T中的每条边e，如果e具有V的值C或D，并且 spf（e）=[φ]或[φ]，则存在e的后继节点n使得n在V中连接到e，e的结束节点与n之间的距离不大于L，且n满足n≠φ。断言：如果树T有一致赋值，它就有L-一致赋值.阿拉拉吉137⇐∪ ···∪LLM1M2M2S1DS 1S2MS3m3m 1M2M33M3S4图五、分支中pe索引的出现证明：当给出一致的赋值时，我们反复修改它从根到后继的边。期望的L-相容赋值是这个操作的极限.定理：计划规则是启用承诺的，当且仅当CM验证的决策过程返回校样：（）如果过程返回“no”，则pe树不具有一致的值：不难看出，如果过程返回那么，根据上面的说法，T（1）如果过程返回在下面，我们构造一个一致的估值。当过程返回“ok”时，它的画面不是空的。我们从画面中截取一个分支。设S1是br的节点集，其到根的距离不大于L.设dS1是通常意义下S1设S2是br的节点集，其到dS1中的节点的距离不大于L.设dS2是S2的叶节点集.同样，我们定义S3，S4，···和dS3，dS4，···。引理：对于某个k，以下是有效的。{m|m是dS k }{ m}中节点的pe索引|m是节点的pe索引，S1<$···<$Sk−1}-在这里，我们将边的每个pe索引都归因于其结束节点。证明：我们检查（*）是否有效，顺序为k = 2，3，4，···。如果（*）对k无效，这意味着Sk包含一个节点，其pe索引与S1Sk−1 中 的 索 引 不同。换句话说，一个新的pe指数必须出现在Sk中。但可能的pe指数的数量是有限的。则（*）对于k小于M有效，M是决策过程中使用的数字。参见图5，k= 4。阿拉拉吉138∪···∪L图六、从一个分支构造一个相容赋值我们使用图6来解释如何构建一致的估值。 图6中左边的树显示了满足引理中条件（*）的分支br的一部分。在这种情况下，我们假设出现在dSk中的pe索引是m1和m2。由于（*），在S1<$···<$Sk−1中有pe索引为m1和m2的节点。设节点分别为n1和n2n1和n2在S1<$···<$Sk中产生两个子树，它们的根分别是n1和n2，并使这两个子树分别是sT1和sT2我们复制sT1和sT2，并通过将dSk中的节点粘到子树的相应根来将它们连接到S1 Sk我们反复将这些子树粘到操作过的树的叶子上：见图的右边。六、不难看出，这种重复给出了一致的估值。6结论和今后的工作在本文中，我们已经形式化了一个验证问题，这个问题是在为BDI架构实现一个单一的承诺策略时出现的。我们还提供了验证的决策程序。虽然有其他方法来实施一个一心一意的承诺战略，我们采取了一个相当正式的方法。这种方法为程序验证提出了一个有趣的问题，例如正在考虑验证的状态转换取决于其他状态的验证。我们只是在这个独特问题的起点，必须更充分地阐述形成和决策程序。我们还希望给出我们的方法与[6，3]中给出的时态逻辑中的承诺策略的形式化的明确联系，以便我们可以在逻辑框架中讨论我们的承诺策略致谢sT1M1n12mn2M1m1m2M2sT2阿拉拉吉139我们要感谢Yoshifumi Ooyama，Norihiro Hagita和Kenji Mase对这项工作的支持。这项研究也得到了电信促进组织的部分支持。引用[1] T. 阿拉吉山口阿蒂岛凯达尔湾小固河谷Luchangco，N.Lynch和K.马诺Agent计算的形式化建模 Proc. 第一次戈达德研讨会的正式方法基于代理的系统，第48-62页，2000年。[2] T.阿拉吉湾小暮使用基于逻辑的代理系统动态下载通信协议。Proc. ofCLIMA-00，第27-34页[3] P. R. Cohen和H. J.Levesque人工代理人的沟通行为。软件代理，第419MITPress，1997.[4] Jr. E. M. Clarke，O. Grumberg和D. A.佩尔德。模型检查。MIT Press，1999.[5] N. Nide和S.高田使用序列演算的BDI逻辑的演绎系统。在AAMAS 2002，2002的Proc.中。[6] A. S. Rao 和 M. P. George ， 在 BDI 架 构 中 建 模 Rational Agent 。 在 Proc. ofInternational ConferenceonPrinciplesofKnowlegdeRepresentationandReasoning，第473-484页[7] A. S. Rao 和 M. P. George ， BDI 逻 辑 的 决 策 过 程 。 Journal of Logic andComputation，8（3）：292[8] M. P. Singh，A. S. Rao和M. P. George，DAI中的形式化方法：基于逻辑的表示与推理.在Multiagent Systems中，第331-376页。MIT Press，1999.[9] S.高田湾Igarashi，N. Nide，M. Enomoto，K. Mase和R.中津 在多智能体环境中有意识地执行言语行为的理性智能体设计（日语）。电子信息通信工程师学会学报，J84-D-I（8）：1191