社会完整性约束下的逻辑化代理交互验证方法

《理论计算机科学电子札记》85卷2004年第URL：http://www.elsevier.nl/locate/entcs/volume 85. html23页s基于社会完整性约束马尔科·阿尔贝蒂a Marco GavanelliaPaolo TorronibaDipartimento diIngegneriaUniversit`adegliStudidiFerrar aaVia Saragat，1 - 44100 Ferrara（意大利）bDipartimento di Elettronica，Informatica eSistemisticaUniversit`adegliStudiBolognaVia del Rinascimento，2 - 40126 Bologna（Italy）摘要在本文中，我们提出了一种基于逻辑的社会方法来规范和验证代理交互。我们首先引入了关于社会行为的完整性约束（称为社会完整性约束）作为一种形式主义来表达交互协议，并为Agent的行为提供社会语义，重点是交际行为。然后，我们讨论了几种可能的代理交互验证，我们展示了如何社会完整性约束可以用来验证在这方面的一些属性我们把注意力集中在静态验证代理规范的遵守交互协议，并在运行时验证，基于代理的可观察的我们采用NetBill安全交易协议作为一个运行的例子，用于信息商品的销售和交付1介绍规格说明和验证是计算机系统设计和部署的两个重要步骤特别是，它们在开放系统的开发中发挥着关键作用，开放系统由我们希望在某种程度上可预测的自治实体组成，或者至少符合某些交互规则。这在多智能体系统中经常发生解决这个问题的一个可能的方法是依赖于一个正式的计算框架，该框架可以用于为代理交互提供正式的规范，并自动检查它们的在这样做的时候，有两种观点是可能的：一种是我们可以定义为个体的，旨在设计代理，使它们2004年由E lsevierScie nceB. V. 操作访问和C CB Y-NC-N D链接。MARCOALBERTI等.2称之为社会的，旨在验证主体的可观察行为的依从性，而不考虑其内部结构。这 两 种 方 法 之 间 的 差 异 在 Agent 通 信 语 言 （ Agent CommunicationLanguages，简称CCL）的语义定义中变得明显。心理学方法[6，7]从内部角度定义ACL语义在代理人的精神状态方面。例如，FIPA ACL [7]假设代理的BDI（信念，欲望，意图）模型，并依赖于它来定义可行性前提条件（即，要计划的交往行为必须满足的条件通信行为的预期效果FIPA ACL提供了一组全面的通信原语，其语义似乎足以从个体代理的角度解释通信行为的动机。然而，它的语义，作为其他mentalistic的语义，似乎并不完全满足开放环境中的异构代理相互作用的代理通信的要求[16]。特别是，当智能体的精神状态不可访问时，如在开放社会的情况下社会方法[17]根据其公共（社会）效果，而不是根据其内部（心理）动机来定义交际行为的语义。遵循这种方法，可以基于代理的可观察行为来验证对给定语义的遵从性，即使在代理的内部状态不可访问或没有根据心理类别描述的架构的情况下。重要的社会建议是基于承诺的概念[8，19]，计算对象跟踪代理之间的义务，并可以根据代理的 （ 可 扩 展 的 ） 通 信 和 非 通 信行 为 而 发 展 ， 并 最 终 解 决 实 现 或 违 反 。在本文中，我们提出了一种基于逻辑的方法来规范和验证代理交互。在这样做的时候，我们采用了社会的视角，从代理内部抽象出来。本文的贡献是双重的。在本文的第一部分，我们介绍了一个基于逻辑的形式主义（社会完整性约束），用于指定代理的预期行为。我们对个体代理的内部结构没有先验假设（特别是，我们既不假设也不拒绝个体代理的BDI内部结构），而是专注于公众对互动的观点我们的语义学是基于期望的概念，通过社会完整性约束与事件联系起来本文第一部分的目的不是提出一个新的ACL，作为一组通信原语，或一个特定的交互协议;相反，我们提出了一个基于逻辑的方法来定义给定ACL的社会语义，或交互协议。MARCOALBERTI等.3该规范基于计算逻辑框架，因此可以提供多智能体系统中交互的期望目标的声明性规范，以及通过形式证明过程对其进行自动为了解释我们的想法，我们采用NetBill协议作为一个运行的例子。NetBill是一种安全和交易协议，用于销售和交付低价信息商品，如软件或期刊文章。我们选择NetBill是因为我们相信它是与多代理系统中的信息交换相关的一类协议的很好的代表，并且它很适合讨论在这方面可能出现的问题本文第二部分研究了Agent交互的验证我们参考了Guerin和Pitt在[14]中介绍的不同类型的验证的分类，它区分了静态验证、通过观察的验证和协议属性的验证我们专注于前两种验证。对于第一种，我们提出了一种方法来验证代理规范对一组协议的遵从性至于第二种，我们通过约束处理规则[9]描绘了框架的原型实现，并展示了如何使用它来通过观察验证合规性本文件的结构如下。第二节通过引入社会诚信约束的概念，给出了必要的背景在第3节中，我们将展示如何利用它来指定通信行为和代理交互协议的社会语义第四节专门研究不同类型的核查。讨论和未来工作的方向结束的文件。2社会诚信制约在本节中，我们简要地描述了一个代理社会模型，这是一篇配套论文[1]中提出的模型的简化版本在我们的模型中，一个社会是由一个社会基础设施（其操作部分）和一个知识库，包含有关社会的结构和属性的信息。特别地，社会知识库包含关于进入、退出和角色分配的协议和规定的信息这些信息在一个（扩展的）逻辑程序中表示，我们称之为社会组织知识库（SOKB），社会诚信约束（SIC）1。此外，我们假设社会在“历史”文件HAP中记录社会中可观察到的和相关的事件（发生的事件，由函子H表示），包括社会中交换或执行的1在本文中，为了简单起见，我们假设SOKB是由基组成的事实在[1]中，为了捕获更多的结构化知识和目标导向的社会，我们将SOKB和SIC定义为溯因逻辑程序。MARCOALBERTI等.4例如，H（tell（thomas，yves，start））表示一个社会事件，其中一个智能体thomas告诉另一个智能体yves“这是一种沟通行为。 H（do（thomas，yves，buy（ticket）表示非交际行为：托马斯从yves那里买票的行为。从逻辑编程的角度来看，HAP可以被理解为定义由函子H指示的谓词的一组基础事实。一系列的事件HAP可能会引起社会对其成员未来行为的期望期望值被收集在一个集合EXP中。特别地，它将包含预期发生的事件（由函子E表示）和预期不发生的事件（由函子NE表示）。例如，E（do（thomas，yves，buy（ticket）表示对一个非交际行为的期望：托马斯被期望从yves那里买一张票。NE（tell（yves，thomas，reject（ticket）表示关于 一种沟通行为：希望伊夫不要拒绝托马斯社会基础设施记录事件;根据事件，更新EXP中的期望。此外，监控代理交互，例如，为了在违反预期的情况下启动适当的恢复程序协议根据社会完整性约束（SIC）进行形式化。SIC描述了社会期望的演变，基于当前的历史。SIC的语法如下：SIC：：= [icS]icS：：=χ→φx：：=ExtendedLiteral[扩展文字]φ：：=ExpectList[：ConstraintList]ExtendedLiteral：：=期望|事件|原子期望：：= E（项）|NE（术语）事件：：=H（术语）ExpectList：：=Expectation[Expectation]（一个）原子在SOKB中被定义（通过基础事实）。约束列表是CLP [12]约束的结合，例如-例如-可以在完整性约束的两个变量之间施加的≤社会完整性约束的主体χ中的所有变量都是普遍量化的，范围是整个完整性约束，除了那些只出现在χ的NE期望中的变量，这些变量都是普遍量化的范围它们所发生的NE期望MARCOALBERTI等.5所有其他变量都是存在性量化的，作用域是它们出现的完整性约束的头φ，除了那些出现在φ的NE期望中的变量，它们是普遍量化的，作用域是φ。社会诚信约束的一个简单例子如下：SIC={H（tell（X，Y，start））→E（pass（Y））}它的直观含义是：如果智能体X告诉智能体Y一个更详细的例子，包括CLP约束，是下面的社会完整性约束，我们将在下一节讨论的一个例子H（请求（B、A、P、D、Tr））H（accept（A，B，P，D，Ta））TrT（十二）r r aH（拒绝（B、A、P、D、Tr））→NE（accept（B，A，P，D，T））：T> T（十三）阿阿值得注意的是，在我们的框架中，我们对语义不同的事实上，在代理交互的规范中，我们可以区分调节性规则，例如：分析约束断言关于4相反，如果一个代理想要请求同一个商品的两个实例，它将启动两个不同的对话。5然而，如果我们希望防止代理人重复一个沟通行为，例如，接受，在同一个对话中，我们可以写以下约束：H（accept（B，A，P，D，Ta1））- NE（接受（B，A，P，D，Ta2））：Ta2> Ta1（11）在续集中，我们假设代理不能同时发送两个通信动作这可以通过适当的社会基础设施来实际执行，该基础设施使用细粒度的时间标记来“自动”标记消息的MARCOALBERTI等.11系统相对于模型，在“物理”规则方面它们不会产生期望，我们也没有将它们包括在本文中，但它们确实可以在框架中考虑并建模为完整性约束。在制裁和发生违反行为时应采取的反措施方面，管制/规范性规则与构成性规则之间的区别将变得特别明显，但我们还没有处理制裁问题。4基于社会完整性约束的Agent交互自动验证在本节中，我们将讨论两种方法来验证主体交互对通过社会完整性约束给出的规范的遵从性在[11，14]中，F.Guerin和J. Pitt提出了一种与电子商务系统相关的属性分类，特别是关于协议和交互的属性。他们提出了一个正式的框架，用于在开放的环境中验证“实现代理机制所需的低级计算理论”的属性，其中“开放”的作者意味着一般来说不可能观察或约束代理的精神状态。根据可用的信息以及验证是在设计时还是在运行时完成，属性的验证分为三种类型类型1：核实代理人将始终遵守;第2：通过观察核实遵守情况类型3：验证方案属性。至于类型1验证，作者建议使用模型检查算法，由有限状态程序实现的代理。至于第二类验证，作者提到了Singh [17]的工作，其中“可以根据他们的通信来测试代理人的合规性”，并建议对社会进行监管，至于类型3的验证，作者展示了如何仅使用ACL规范来证明协议的他们构建了一个公平的过渡系统，代表所有可能的可观察的状态序列，并证明了所需的属性在多智能体系统的所有计算。这种类型的验证是通过一个拍卖的例子来证明的。我们引入的基于社会诚信约束的正式框架很适合于类型2和类型3的验证，它们不依赖于代理人内部的表示此外，如果我们能够在基于逻辑编程的形式主义中指定代理的内部策略，类似于我们用于社会完整性约束的形式主义，那么它就成为可能。MARCOALBERTI等.12通过将社会和个人方面联系起来来解决第1类验证，我们将在下面看到。通过提出我们的框架，我们的目标是在计算逻辑环境中统一和自动地处理所有上述三种类型的验证一般来说，无法通过外部监控其行为来验证代理始终遵守。对于这种验证，我们需要至少访问代理的内部规范第4.1节介绍了一种机制，可以自动为一组受限的程序和协议获得这样的证明（或其失败）对于类型2的验证，我们需要能够观察代理人的社会行为，即，他们交换的交流行为。正如在[14]中，我们可以假设这可以通过监管社会来实现。特别是，第4.2节致力于介绍一种基于约束处理规则的运行时验证类型3的验证是关于协议属性的。为了证明它们，我们不需要访问代理的内部，也不需要了解系统的通信行为，因为这样的验证是在设计时静态完成的我们将不会在本文中介绍这方面的任何结果。4.1代理对协议的遵从性的静态验证在一个非常普遍的理解中，验证一个代理人“总是会遵守”会带来明显的可判定性问题。 出于这个原因，我们不会通过查看代理代码来进行这种验证，而是基于我们想要预测其遵守情况的代理的社会行为的某些规范。因此，我们将讨论代理的规范对一组表达交互协议的社会完整性约束的遵从性代理人社会行为的规范可以再次根据完整性约束给出我们称这种约束为icσ。它们具有以下语法：icσ：：=χ→φχ：：=事件[事件]φ：：=Event[Event]Event：：=H（Atom）（十四）完整性约束icσ的主体χ中的所有变量都是通用量化的，作用域为icσ。所有其他变量都是存在量化的，作用域是它们出现的H谓词完整性约束icσ表达了主体对以下行为的可能反应：MARCOALBERTI等.1322外部输入（通常是交流行为）。理解χ→φ类约束的方法如下：如果χ是这种情况，那么在某个时刻，施事会使φ为真。χ基于代理交互的可能历史，因此它是事件的合取一般来说，我们假设可以根据完整性约束icσ给出智能体社会行为的具体化。例如，如果代理实现了[15]中提出的操作模型，那么这确实是可能的：在这种情况下，代理规范可以通过适当的语法转换从代理程序（协商策略和对话周期）中自动导出。让我们举一个具体的例子来说明这种限制。让我们考虑一个消费者代理c和一个商人代理m，他们的任务是使用NetBill协议购买/销售我们可以假设c和m都是societys的成员，society s根据社会完整性约束定义了NetBill协议。cH（存在（M，c，（G，Q），D，T1））→H（accept（c，M，（G，Q），D，T））（15）H（deliver（M，c，（G，Q），D，T1））→H（epo（c，M，（G，Q），D，T2））m（十六）H（请求（C，m，（G，Q），D，T1））→H（存在（m，C，（G，Q），D，T））（17）H（接受（C，m，（G，Q），D，T1））→H（deliver（m，C，（G，Q），D，T2））H（epo（C，m，（G，Q），D，T1））→H（接收（m，C，（G，Q），D，T2））（十八）（十九）在这个简化的例子中，我们只考虑了确定性的代理指定。一般来说，这些规范将是非确定性的，它们需要表示为可能在头部有析取的约束。例如，[4]中定义的NetBill协议允许在需要时重复协商过程，在协商过程不成功后放弃交互，在交付的货物损坏的情况下不发送电子支付订单等。这使得协议不确定，并允许兼容的不确定代理规范。此类规范的示例如下：MARCOALBERTI等.14SSSSS• c可将（15）改为：H（存在（M，c，（G，Q），D，T1））→H（accept（c，M，（G，Q），D，T2））拒绝引用（c，M，（G，Q），D，T2）（二十）• m可用以下案文取代（17）H（请求（C，m，（G，Q），D，T1））→H（存在（m，C，（G，Q），D，T2））拒绝请求（C，m，（G，Q），D，T2）（二十一）接下来，我们将给出基于一类受限协议和规范的代理/规范遵从性的概念。这种简化使我们能够提供一些关于代理/规范的静态验证的初步结果让我们把自己限制在SIC以χ→φ的形式表达协议的情况下，其中φ：：=期望（没有对期望中的变量施加约束）。让我们考虑SIC的子集SIC（a），其仅包含其头部是关于代理a的行为的期望的约束（例如，由a发送的消息）。我们要检查a是否符合IC（a）。6设σ是a的在上面解释的意义上的确定性让ici∈SIC（a）是第i个社会SIC（a）中的完整性约束，ici=χi→E（αi）或ici=χi→NE（αi）。可能有不同的情况：(i) 阿利契奇岛(ii) 阿利契奇岛=χi→E（αi），σηχi<$H（αi）（正顺应性）;=χi→NE（αi），σηχi$H（αi）（负顺应性）;(iii) （i）和（ii）都成立（强遵约）;(iv) （i）和（ii）都不成立。如果代理实现遵守σ中给出的规范，那么，取决于它属于上面定义的四种遵从性类别中的哪一种，我们知道我们可以通过它与r.t.的交互来期望什么。SIC（a）中定义的协议。（i）可以被看作是活性属性，而（ii）可以被看作是安全属性。特别地，如果智能体是正顺应的（i），它将总是产生根据MARCOALBERTI等.15SIC（a）预期的移动（但我们不知道它是否也会产生违反某些协议的其他移动如果代理人是负顺应的（ii），它永远不会产生预期不会产生的移动如果代理是强顺应的（iii），它将始终遵守协议，满足所有期望，不违反任何社会规则。6由用户来选择与确定a是否合规相关的约束集合，尽管该过程可以容易地自动化，例如通过引入“角色”的概念（代理合规“作为商家”、“作为客户”、作为两者等）。MARCOALBERTI等.16完整性约束最后，如果代理人的规范属于最后一类（iv），我们不能先验地这些结果适用于一类有限的程序和协议。我们对遵守的概念作了说明性的描述由于这样的特征是基于一个概念的蕴涵，我们相信，它的操作对应不会是困难的，以获得作为一个适当的扩展经典演绎推理机。在 NetBill示 例 中 ， 我 们可 以看到 c 的确定 性版本强 兼容 SIC（ c）={（7）}，m的确定性版本强兼容SIC（m）={（6），（8）}。4.2使用约束处理规则的第二类验证旨在检查代理人我们已经在第二节中给出了这种顺从的声明性二、在操作上，必须通过适当的证明程序来核实显然，这种证明程序应随着代理人的互动而逐步运作，以便能够在违规行为发生时立即发现违规行为，并可能启动恢复程序。特别是，约束传播技术可以用于尽早检测期望是否永远不会被满足（见4.2.2节）。直觉上，期望应该是这样产生的，以满足社会诚信约束：当所有的事件和期望在身体的χ当社会在HAP和EXP集合中插入了社会诚信约束χ→φ时，头部φ中的期望值应该提高。期望将一直悬而未决，直到它们被满足或被违背，社会基础设施将监视它们，以检查发生的事件是否符合并满足它们或违反它们。从本质上讲，约束处理规则[9]（以下简称为“约束处理规则”）代表了一种提交选择语言，它由保护规则组成，这些规则将存储中的约束重写为更简单的约束，直到它们被解决为止。在用户定义的约束上定义简化（用更简单的约束替换约束，同时保留逻辑等价性）和传播（添加新的、逻辑冗余但在计算上有用的约束）JavaScript的主要用途是编写约束求解器，或者扩展现有的约束求解器。然而，虽然我们的不是一个经典的约束编程设置，计算模型中的ESTA提出的功能，使其成为一个有用的工具，我们的目标是实现的证明程序。在下文中，我们将通过验证来描述一个符合社会诚信约束的验证过程的原型实现，该过程将在未来的工作中得到扩展和完善。值得注意的是，下面描述了第2节中描述的声明性框架的操作对应物，以及第3.1节中描述的规范。MARCOALBERTI等.17实现的参数。这允许轻松实现规范的扩展4.2.1实体的表示我们假设类型2验证的证明过程是代理人生活的社会基础设施的一部分在社会的整个生命周期中，社会基础设施在一个循环中重复以下两个操作：(i) 记录事件;(ii) 根据社会的具体情况处理事件在本工作中描述的原型实现中，事件由程序员模拟。在开放式实现中，该任务可以通过合适的网络通信机制（诸如套接字监听过程）来完成。时间在当前实现中，时间由整数表示，在每个时钟节拍处递增1。当前时间由时间约束7current time/1表示，其参数是自社会开始以来的时钟滴答数当前时间通过简化时间表更新。简化的形式是H1，.，Hi G1，.，G j|B1，. ，Bk（22）其中i > 0，j≥ 0，k≥ 0，并且其中多头H1，.，H1是一个非空的约束序列，保护G1，.，Gj是内置约束的序列，并且主体B1，.，Bk是一个内建约束和非内建约束的序列。声明地说，简化规则是逻辑等价的，只要守卫为真。在操作上，当约束H1，.，Hi是在头部是在商店和警卫G1，.，Gj为真，则它们被约束B1，.，Bk在体内。通过以下简化规则，可以利用此操作行为在每个时钟周期更新当前时间clock，current_time（OldTime）<=>NewTime= OldTime +1|current_time（NewTime）。其中当需要时钟节拍时施加约束clock/07即，一个约束，它是通过约束定义的，不是内置的。MARCOALBERTI等.18事件Happened事件由一个约束happened/1表示，它的参数是描述事件的基础项例如，如果在对话d期间并且在时间10，代理1已经接受ed将钉子给代理2，则将存储以下约束：happened（accept（agent1，agent2，give（nail），d，10））.预期期望由expect/2约束表示第一个参数是与期望相关的事件，第二个参数是事件8中包含的变量的约束列表。例如，期望在对话D的上下文中，代理1在时间20之前将钉子给代理2将是代表如下：expect（do（agent1，agent2，give（nail），d，T），[tle（T，20）]），其中tle是事件时间之间的小于或等于的二元约束（需要与第4.2.2节中解释的数值变量之间的普通≤约束区分开来消极的期望。负期望由expectnot/2约束表示，具有与expect/2约束相同的结构。社会诚信制约。社会完整性约束由传播约束表示。一般来说，传播规则的形式为H1，.，Hi= Hgl，.，Gj|B1，. ，Bk（23）其中符号具有与简化规则（22）中的符号相同的含义和约束。从声明上讲，传播规则是一个隐含，前提是保护为真。在操作上，当head中的约束在存储中，并且guard为true时，body中的约束被添加到存储中。这种机制可以被利用来将期望发布到商店中，如社会完整性约束所规定的，如下所示：• 约束主体中的事件和期望由约束头部中的约束表示;• 约束体中的原子由约束体的保护中的内置约束表示;• 约束头部中的期望（具有相关联的约束）由约束主体中的约束来表示。8.在目前的实施中，期望不能共享受约束的变量。MARCOALBERTI等.19例如，约束（9）可以由以下传播规则9表示：happened（accept（Agent2，Agent1，Content，Dialog，AcceptTime））==>expect（request（Agent1，Agent2，Content，Dialog，RequestTime），[tlt（RequestTime，AcceptTime）]）.每当一个匹配10head的事件被添加到store中时，此规则将向store添加相应的期望。4.2.2程序满足和违背期望。在操作上，如果事件和期望的内容在Prolog意义上统一，并且期望中的约束为真，则事件满足期望在负面期望的情况下，事实上，我们没有一个完整的，但违反。这是通过以下传播函数实现的：happened（HEvent），expect（EEvent，Constraints）==>HEvent=EEvent，verify_constraints（约束）|fulfiled_expect（EEvent，Constraints）.一个已满足的期望被存储为一个已满足的expect/2约束。verify constraints/1是一个用户定义的谓词，用于检查具有基础参数的约束的真实性。例如，让我们假设商店中有以下期望expect（do（agent1，agent2，give（nail），d，T），[tle（T，20）]），并且在时间15发生以下事件happened（do（agent1，agent2，give（nail），d，15））.期望的内容和事件的统一成功，绑定T=15。因为tle（15，20）为真，所以期望被满足，并且在操作上，可以存储为已满足的expect/2约束。利用约束传播进行违规的早期检测上一段所描述的机制不足以满足所有类型的期望。让我们假设商店中有一个带有截止日期的期望。如果社会基础设施只是等待一个匹配的事件发生，[9]可以注意到，将社会完整性约束映射到一个规范是非常简单的，因此很容易实现对给定规范的扩展。10它是解释一个在下一个部门，通过PrologMARCOALBERTI等.20并且该事件从未发生，则对最后期限的违反将永远不会被检测到。显然，这不是我们想要的行为：我们希望在一段时间后就能检测到违规行为。更一般地说，需要在不等待某些事件发生的情况下检测对某些期望的违反。为了处理这种情况下，我们利用约束传播：当期望的变量受到某些约束（如tle/2）的约束时，在存储中插入新的约束，这意味着与其他表示可能改变的条件（如当前时间）的约束进行交互例如，让我们再次考虑最后期限如果T是表示具有相关联的最后期限的事件应该发生的时间的变量，并且T是未绑定的，则事件还没有发生，因为否则事件将被记录在存储中并且T将被实例化为一个特定的值11.因此，如果Tcurrent表示当前时间，我们可以推导出以下不等式：T电流≤T（24）它具有直观的含义，即如果一个事件还没有发生，那么它只可能在未来发生不等式（24），结合约束条件T≤T期限（25）意味Tcurrent≤T deadline（26）因此，如果当前时间超过了最后期限，而T是未绑定的，则相关的期望不能被满足，并且可以检测到违规（或者，双重地，相关的负期望不能被违反，并且其实现可以被检测到）。为了在我们的框架中实现这一行为，每当一个期望被施加，其中包含一个表示截止日期的约束（例如tle（T，20）），社会基础设施就会推断出一个tcurrent le/1约束（这意味着当前时间不得超过与截止日期统一的参数），并将其与原始期望相关联。如果违反了tcurrent le/1约束（这是通过检测器检测到的），则检测到原始期望的违反/实现;如果在截止日期之前实现了期望/违反了期望，则删除相关的tcurrent le/15讨论和今后的工作在本文中，我们把两个方面放在一起：代理交互的规范和形式验证。我们从社会的角度来探讨这两个问题，我们认为，[11]我们总是假定社会基础设施了解所有具有社会意义的事件。