理论计算机科学电子笔记126（2005）93-114www.elsevier.com/locate/entcs道义解释系统BozstecenaWo′znaa，1，2AlessioLomuscioa，1，3WojciechPenczekb，4一计算机科学伦敦大学学院Gower Street，London WC1E 6BT，英国b计算机科学研究所，PAS Ordona21，01-237 Warsaw，Poland摘要我们提出了一个框架，验证多智能体系统的规范的符号模型检查。语言CTLKD（CTL的扩展）允许代理的认知状态的时间演变的表示，以及他们的正确和不正确的功能行为。我们的地面上的道义解释系统的语义分析。验证方法基于有界模型检查技术的改编，这是反应系统验证的主流方法。我们测试我们的结果在一个典型的通信场景：故障位传输问题。保留字：有界模型检验，认知逻辑。1介绍软件工程师的任务是设计和部署符合特定规范的计算机系统。 这绝不是一项微不足道的任务。仅仅在过去的几个月里，美国宇航局1作者感谢EPSRC（grant GR/S49353）和Nu Pield基金会（grant NAL/690/G）的支持。2 电子邮件地址：bozena@dcs.kcl.ac.uk3电子邮件：A. ucl.ac.uk4 电子邮件地址：penczek@ipipan.waw.pl1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.11.01594B. Woz 'na等人理论计算机科学电子笔记126（2005）93即使是完全设计的分布式系统也可能遇到。在关键任务软件以及特别敏感的应用程序中，如互联网协议、全球电子银行系统等，软件工程师感兴趣的是分析软件的属性，特别是检查特定的条件，从基本的死锁到更复杂的条件，是否适用于特定的系统。多智能体系统领域也对类似的问题集感兴趣。多智能体系统[17]是分布式系统，其中各个进程或智能体是参与协调，谈判，合作等社会活动的自治实体。由于多智能体系统是自治的和社会的，它们可能的行为范围甚至比传统的分布式系统更大。由此可见，验证系统满足的属性在多智能体系统中同样重要。软件确认，即，检查一个软件是否满足某些特性的过程目前主要通过三种技术进行测试包括搜索程序可能输入的状态空间，寻找可能有问题的输出。定理证明技术基于通过形式逻辑系统来表示程序;在最简单的情况下，检查一个属性是否满足相当于检查一个公式是否是表示程序的逻辑的定理模型检查在其主流方法中涉及通过时间模型（适当地表示）表示程序的所有可能的计算痕迹，并检查表示要验证的属性的时间公式是否在该模型中成立换句话说，软件验证具有内在的“道义内涵”。它相当于检查所考虑的系统是否按照其规范所规定的那样运行但应该注意的是，在这种方法中，这是一个外部于逻辑系统的属性。有人会说，系统的正确功能行为是表示程序的逻辑系统的元逻辑属性。 与道义逻辑中发生的事情不同，道义概念在这里并没有明确地用在逻辑中来表示系统，但它们被构建在对用于检查系统的逻辑进行操作的过程中。虽然已经通过标准验证技术验证了一系列系统，但多智能体系统应用需要改进的方法。例如，考虑在电子拍卖中为货物投标的若干自动代理这些代理人如何进行投标可能有规则，但通常不可行和/或适得其反，B. Woz 'na等人理论计算机科学电子笔记126（2005）9395这些规则中的许多规则在拍卖协议本身中是硬连线的。作为拍卖的设计者，我们可能会认为代理商不会在同一商品上每秒多次出价，从而不会在服务器级别产生拒绝服务问题，这是有益的，但当代理商由各种软件公司编程时，我们似乎很难强制执行。从传统的联邦数据库到最近的关键任务软件中的故障控制模块，其他例子都指向类似的结论：当程序按照它们的规范运行时，推理系统中的属性是很重要的，但有时甚至更重要的是，即使它们没有。 换句话说，我们不仅希望 检查一个系统是否满足其规范，但我们也想推导出系统不按预期运行所导致的后果。不同的道义逻辑已经被用来把正确的（或理想的，规范的，等等） 不正确的国家。 在本文中，我们想把这些想法更进一步，并提供一种技术，通过这种技术，我们不能指定，但也可以自动验证表示多代理系统对规范的遵从性的属性。为了进行这种分析，我们使用了通过模型检查进行验证的形式化机制[4]，特别是通过SAT翻译的有界模型检查[3]。在通过模型检验进行验证时，人们通常通过SMV[12]等语言的程序来描述系统S然后将该描述提供给模型检查器，该模型检查器产生表示系统S的所有可能执行的（适当编码的）时间模型MS。 要检查属性P是否满足S，需要检查时间模型MS满足表示P的公式φP，即，MS|= φP。这种方法的关键问题是管理结果模型MS.保持方法可行的技术之一是有界模型检查。这种技术的重点是试图发现系统规范中的错误。在有界模型检验中，不是检查整个状态空间来验证属性，而是检查属性的否定是否实际上在模型的一部分上得到满足，从而产生一个反例。此外，通过将适当的翻译计算为代表截断模型和待检查公式的命题公式，将实际检查转换为标准的命题满足性问题通过这种方法，发现了反应式系统协议中的一些细微缺陷我们参考[1，3，5，14]了解更多细节。虽然在反应式系统中，通过纯粹的时间语言来建模系统就足够了，但多代理系统的定义如下：96B. Woz 'na等人理论计算机科学电子笔记126（2005）93这通常被称为换句话说，它是有用的描述自主代理在他们的知识，信仰，意图，社会背景等。这意味着，多智能体系统的模型检测问题不能简单地说，作为一个时间逻辑，但更丰富的形式主义需要使用。在过去的研究中，我们已经为分支时间时间认知逻辑（CTLK）提供了一个模型检查算法[13]。在本文中，我们扩展这项工作提供了一个有界的模型检查算法的逻辑，包括知识和道义组件代表正确的功能行为的系统。本文的组织结构如下。在第二节中，我们修正了道义解释系统的语义。在第3节中，我们提出了CTLKD的语言，CTLK的扩展，代表代理的正确/不正确的功能- ING行为。在第4节中，我们提出了一个满足的有界语义定义，我们在第5节中使用它来定义有界模型检查的算法。在第6节中，我们将形式主义应用于一个与多智能体系统文献相似的例子：带故障的比特传输问题。2道义解释系统在本节中，我们将介绍道义解释系统。这些在[10]中被定义为表示和推理多智能体系统的正确功能行为它们提供了一种基于代理的计算状态的语义，在此基础上可以解释模态Oiφ，表示“在代理i的所有正确功能执行中，φ保持”的事实，以及传统的认知模态K i φ，表示代理i对φ的知识，道义解释 系 统 的公理化已经为语言的非时间片段提供了;我们请感兴趣的读者参考[11]以获得更多细节。下面的报告只是为了固定符号;更多细节可以在[10，13]中找到。 设PV是命题变量的集合，A ={1，.，n}是一组特工考虑n个非空集合L1，. ..对于每个代理i∈ A，考虑一组可能的动作Acti，n个协议Pi：Li→2Acti代表每个代理的功能行为，Pe：Le→2Acte代表环境。进一步假设，对于每个代理，其局部状态集可以划分为允许和不允许的状态。我们分别称这些状态为绿色和红色。对于n个主体和n+ 1个互不相交的非空集[10]中实际上没有使用时间运算符，但这是一个简单的扩展。B. Woz 'na等人理论计算机科学电子笔记126（2005）9397R我我我G1，.，Gn，Ge我们将所有可能的全局状态的集合S定义为笛卡尔积L1×...×Ln×Le，使得L1≠G1，.，LnGn，LeGe. Ge被称为环境的绿色状态集合，对于任何代理i，Gi被称为代理i的绿色状态集合。Ge相对于Le的补集（用Re表示）称为环境的红色状态集，类似地，Gi相对于Li的补集（用Ri表示）称为智能体i的红色状态集。我们可以通过一个转移函数t：S×Act→S来模拟系统中发生的计算，其中Act=Act1×... × Act n × Act e是联合动作的集合。直觉上，给定初始状态i∈S，协议集和转移函数，我们可以构建一个（可能无限）结构，它代表了系统所有可能的计算。实际上，我们将处理状态空间仅由可达全局状态组成的系统 一个状态s∈S是可达的，如果存在一个状态序列（s0，.，sn）使得s0，.，sn∈S，s0= 1，sn= s，并且对于所有i∈ {0，.，n-1}在存在动作acti∈Act使得t（si，acti）=si+1，即， si+1是将转换函数t应用于全局状态si的结果，并且联合动作acti。如果动作i的每个组成部分都由代理j在s i处的本地状态处的相应协议Pj包含绿色的局部状态，否则它可能包含一些红色的局部状态。关于这方面的进一步考虑，见[10]。在下文中，我们从转换函数、动作和协议中抽象出来，并简单地使用关系T，但应该清楚的是，这是由所考虑的解释系统唯一确定的。设li：S→Li是一个从全局状态返回代理i的局部状态的函数道义解释系统的定义如下：定义2.1[道义干预系统]给定一组代理A ={1，.，n}，一组全局状态S，协议和转换函数，道义执行系统（或简单地说是模型）是一个元组M=（DS，1，T，R，0，...，RO，RK，.，R，K，V），其中1n1n• DS是A的可达全局状态的有限集合，• i∈ DS是初始状态，• TDS × DS是DS上的串行6二进制关系，•ODS × DS是每个代理i∈ A的关系，定义为：li（sJ）∈ Gi7，[6]关系R<$X×X是串行的，如果对所有x∈X，存在y∈X使得xRy。[7]由于每个R O仅取决于目标状态，对于与此组件相关的内容，我们可以通过智能体i的绿色局部状态来定义一个模型。98B. Woz 'na等人理论计算机科学电子笔记126（2005）93R我我•K<$DS × DS是每个代理i∈ A的关系，定义为：li（s，J）=li（s），• V：DS −→2PV是一个赋值函数，使得对所有s∈ DS，true∈ V（s）。 V为每个状态分配一组假设在该状态为真的命题变量。通过|M|我们表示M的状态数，而N ={0，1，2，.. . }表示自然数的选择，并且N+={1，2， . . . }posi ve自然数的集合。M中的计算是无限序列π =（s0，s1，. . ）的状态，使得（si，si+1）∈T，对于每个i∈N。对于计算π =（s0，s1，. . ），设π（k）= sk，且πk=（s0，.，sk），对每个k∈N.在本文的其余部分，我们将把πk称为k-计算。此外，一个k−计算πk是一个（k，l）-循环，如果（πk（k），πk（l））∈T，其中0≤l≤k。 我们称πk为环，如果存在l∈N且l≤k，其中πk是（k，l）-环。我们用（s）表示从状态s开始的所有无限计算的集合，而用k（s）表示从s开始的所有k−计算的集合。3逻辑CTLKD在这里，我们固定CTLKD的语法和语义，CTL的扩展[7]，由Emerson和Clarke介绍，丰富了代表正确功能行为的模态算子[11]和标准认知算子[8]。[13]中分析了语言的时间认知片段的有界模型检验问题定义3.1[CTLKD的定义]设PV是一组命题变量，也包含符号真。CTLKD公式FORM的集合归纳定义如下：• PV的每个成员p都是一个公式，• 如果α和β是公式，那么<$α、α<$β和α<$β也是公式，• 如果α是公式，则EXα、EGα和EU（α，β）也是公式，• 如果α是公式，则Oiα和Kiα也是公式，对i∈ A。直觉上，E表示存在一个计算，如果α在计算的第二状态为真，则Xα在计算中为真，如果β在计算的某个状态为真且总是较早的α成立，则U（α，β）在计算中为真，如果α在计算的所有状态为真，则Gα在计算中为真。计算我们使用索引模态算子Oi来表示代理i的正确运行情况。 公式Oiα代表我们B. Woz 'na等人理论计算机科学电子笔记126（2005）9399关于这个概念的讨论，请参考[10，11]。此外，我们使用索引模态Ki来表示智能体i的认知算子的菱形[8]：Kiα代表“智能体i认为α是可能的“。导出的基本模态定义如下：def= EU（真，α），AXαdef=<$ EX<$α，AFαdefdef=<$EG <$α，AR（α，β）defdef=<$EU（<$α，<$β），AGαdef=<$EF <$α，Oiα=<$Oi<$α，其中i∈A，Kiαdef=<$ Ki<$α，其中i∈ A。此外，委员会认为，α→β=<$α<$β。逻辑ECTLKD是CTLKD的限制，使得否定只能应用于PV的元素，即，在定义3.1中，<$a被<$p取代。逻辑ACTLKD是CTLKD的限制，使得它的语言被定义为{<$LKD|∈ ECTLKD}。很容易看出，ACTLKD由时间公式的形式：AXα，AR（α，β），AFα，Kiα和Oiα。定义3.2[CTLKD的语义]设M为模型，s为状态，α，β为CTLKD公式. M，s| = α表示α在模型M中的状态s处为真。如果隐含地理解，则省略M 的关系|=归纳定义如下：S| = pS|=<$αS|= α β s|= α β我的我的伊鲁伊河p∈ V（s），S| = α，S| = α或s| = β，S| = α和s| = β，S| = EX α我的（<$π∈ <$（s））π（1）|= α，S| = EG α我的（<$π∈ <$（s））（<$m≥ 0）π（m）|= α，S| = EU（α，β）我的（<$π∈ <$（s））（<$m≥ 0）[π（m）|= β和（πj）通过结构归纳法，得到了一个新的结论。 引理直接针对命题变量及其否定。假设这个假设对所有的真子公式都成立。• = α |α β。直截了当。• X=EX α|EG α| EU（α，β）。通过归纳假设-参见[14]第143页。• 令α=Oiα. 如果Mk，s| = Oiα，则通过定义：（π∈Pk）（π（0）= i且n0≤j≤k（s ROπ（j））和π（j）|=α））。通过感应电流，子模型MJ=（DSJ，i，PkJ，RJ，0，.、RJO、RJK、.，RJK，VJ），k1n1n的|PKJ| ≤fk（α）和MJ，π（j） |= α.考虑子模型MJ J=（DSJ J，PkJ，RJ，0，.，RJJO，RJJK，.，RJJK，i，VJJ）k1n1n其中PkJJ= PkJ <${π}且DSJJ=状态（PkJJ）<${s}。由于π是Pkjj，通过构造MJJ和定义有界语义，我们得到MJJ，s| = Oiα且|P·K·JJ| ≤ fk（α）=fk（α）+1.• 令α=Kiα。 如果Mk，s| = K iα，则根据定义：（π∈Pk）（π（0）=i且π0≤j≤k（s RKπ（j）和π（j）|=α））。通过感应存在子模型MJ=（DSJ，i，PkJ，RJ，0，.、RJO、RJK、.，RJ，K，VJ），k1n1nMk使得|PKJ| ≤fk（α）和MJ，π（j） |=α.考虑子模型MJ J=（DSJ J，i，PkJ，RJ，0，.，RJJO，RJJK，.，RJJK，VJJ）k1n1n其中PkJJ= PkJ <${π}且DSJJ=状态（PkJJ）<${s}。由于π是Pkjj，通过构造MJJ和定义有界语义，我们得到MJJ，s| =K iα，|P·K·JJ| ≤fk（α）=fk（α）+1.（=）证明是直截了当的。Q从引理6.1，我们现在可以得出以下结论。推论6.2M|= k<$i <$存在M k的子模型MJ，其中|PKJ| ≤ fk（k）使得MJ，i|= 0。证据它由定义4.4和引理6.1通过使用s=i得出。Q引理6.3对于M的每个状态s，以下条件成立：[]Mk如果存在一个子模型MJ，Mk，|PKJ| ≤fk（k），即，MJ，s|= 0。证据（=>）设[M，s] k<$[] Mk是可满足的。通过对平移的定义，命题公式Mk对所有满足公式fk（k）的k −计算集进行编码。通过定义转移关系的展开，命题公式[M，s]k将fk（）个符号k-路编码为Mk的有效k-计算。因此，在Mk中有一组k−计算，满足公式k，其大小小于或等于等于fk（k）。 因此，我们得出结论，存在Mk的子模型MJ，110B. Woz 'na等人理论计算机科学电子笔记126（2005）93KKKKKK|≤fk（k）和Mj，S| = 0。|= ϕ. MJ的实际定义可以重建K K定义5.5和定义5.4。（=）证明是通过归纳法的长度。引理直接针对命题变量及其否定。考虑以下情况：• 对于α=α<$β，α<$β或时间算子，证明类似于[14]。• 令α=Olα.如果MJ，s| = Olα，|PKJ| ≤fk（Olα），则通过定义4.3，我们有一个k−计算π，使得π（0）= i且（πj≤k）sROπ（j）且MJ，π（j）|=α。因此，通过归纳，我们得到：L k对于某些j≤k，m[α][0，0]∈[M α，π（j）]k的概率是稳定的。 设ii = fk（α）+1是一个新的符号k-路的指数，满足式Ii（w0，ii）。因此，通过上述结构，可以得出：k[j，ii]命题式I（w）<$（[α]<$HO（w））<$[MOlα，s]i0，iij=0klj，ii k这是令人满意的。. 因此，以下各项符合多项要求：k[j，i]I（w）（[α]H O（w ））n [M01α，s] .1≤i≤fk（Olα）i0，ij=0klj，i k因此，通过定义ECTLKD公式的平移，上述公式等于命题公式[Olα][0，0]<$[MOlα，s]k。• 令α=Klα。如果MJ，s| = K lα，|PKJ| ≤fk（K lα），则通过定义4.3，我们有一个k−计算π，使得π（0）= i且（kj≤k）sRKπ（j）和MJ，π（j）|=α。因此，通过归纳，我们得到：L k对于某些j≤k，m[α][0，0]∈[M α，π（j）]k的概率是稳定的。 设ii = fk（α）+1是一个新的符号k-路的指数，满足-求出公式Ii（w0，ii）。因此，通过上述结构，k[j，ii]命题公式I（w）<$（[α]<$ HK（w，w ））<$i0，iij=0kl0，0j，ii[M Klα，s]k是可满足的。因此，对穆拉来说，可确认：.KIi（w0，i）（[α][j，i]Σ<$HK（w0，0，wj，i））<$[M Klα，s]k.1≤i≤fk（Klα）j=0kl因此，通过对ECTLKD公式的平移的定义，a bovefor mula等于比例formula[Klα][0，0]k[M Klα，s]k。Q定理6.4设M是一个模型，Mk是M的一个k−模型，且M是一个ECTLKD公式。 然后，M| = k<$i <$[k] Mk<$[M <$，i] k是令人满意的。证据 由引理6.1和6.3推出。Q推论6.5M| = k<$i <$[k] Mk<$[M <$，i] k不满足k = |M|.这就是我们对翻译技巧的分析。我们现在举一个例子来说明如何将其付诸实践。B. Woz 'na等人理论计算机科学电子笔记126（2005）931117带故障位传输问题的模型检验比特传输问题[8]涉及两个代理，发送者S和接收者R，通过可能有故障的通信信道进行通信。S想要向R传递一些信息--例如一个比特的值。实现这一点的一个协议如下[8]。S立即开始向R发送比特，并继续这样做，直到它收到来自R的确认。R什么也不做，直到它收到比特;从那时起，它向S发送收到的应答。S在收到确认时停止向R发送比特。请注意，即使在S收到其确认之后，R也会继续发送确认直觉上，当S从R得到确认时，它将肯定地知道R收到了该位。另一方面，R将永远不能够知道它的确认是否已经被接收，因为S不应答确认。我们参考[9]作进一步讨论。在本节中，我们感兴趣的是应用有界模型检查的机制来验证上述场景的一个版本，其中一个代理不像它应该的那样运行。这个版本的场景首先在[10
