（计算机软件与理论专业论文）基于知识的协议验证方法及工具.pdf

中山大学硕士研究生毕业论文 唐辉0 1 0 1 8 2 0 0 4 论文题目：基于知识的协议验证方法及工具 专业：计算机软件与理论 硕士生：唐辉 指导老师：苏开乐 摘要 本文主要研究利用知识逻辑进行协议验证的问题。一直以来，高效无二意的 通信协议是人们进行有效的远距离通信交流的基础，设计高效无二意的通信协议 是一项极具挑战性的工作。通信协议的效率可以通过设计高效的编码方案或发明 新型高速传输媒质来提高；而无二意的通信协议必须满足在一定的执行环境中， 所有可能发生的情况下，协议执行的结果唯一确定。本文集中讨论了如何验证一 个设计好的通信协议是无二意的，即协议验证问题。这一问题也是一个极具挑战 性的问题，并且至今还没有一个完美的解决方案。 传统的协议验证方法多基于时态逻辑，主要考察系统在执行协议时在时间序 列上所具有的性质。引入多智能体系统后，协议的执行不仅受时间的影响，还与 智能体的知识状态有关。在多智能体系统中考察协议的执行，不仅可以从时间序 列上考虑，还可以从系统中的智能体执行协议后，所具有的知识发生变化这个角 度去考虑。这正是本文讨论的切入点，本文在传统的基于时态逻辑的协议验证方 法基础上，引入知识逻辑，借助多智能体系统的知识模型，以新的视角研究协议， 并利用模型检测技术实现了对有限知识模型的多智能体系统的协议验证。 作为研究成果，我们定义了一个有限状态多智能体系统框架，并研究了在采 用不同观察策略的多智能体系统中如何计算智能体的知识。以此为理论基础，我 们实现了基于知识的协议验证系统k m a s ，并利用模型检测技术成功验证了几 个协议实例。同时，作为研究的一个附加成果，我们实现了基于知识的程序设计 工具l k b l 。 关键词：协议验证、知识逻辑、模型检测、多智能体系统、基于知识的程序设计 中山大学硕士研究生毕业论文唐辉0 1 0 1 8 2 0 0 4 k n o w l e d g e - b a s e d p r o t o c o lv e r i f i c a t i o n ： a p p r o a c h e s a n dt o o l s b y t a n g h u i m a j o r ：c o m p u t e r s o f t w a r ea n di t st h e r o y s u p e r v i s o r ：s u k a i l e a b s t r a c t i nt h i sp a p e r , w es t u d yh o w t ov e r i f yp r o t o c o l sb yu s i n gt e m p o r a ll o g i c o fk n o w l e d g e t h ec l a s s i c a la p p r o a c h e s f o r p r o t o c o l v e r i f i c a t i o na r e b a s e do nt e m p o r a ll o g i cs u c ha sc t l o rl t l w e i d e n t i f yt h a tap r o t o c o l c a nb ed e s c r i b e db ya g e n t s k n o w l e d g ee v o l v e m e n t i nam u l t i 。a g e n t s y s t e m b a s e d o nt h es e m a n t i c so fi n t e r p r e t e ds y s t e m sp r o v i d e db y h a l p e r n a n dh i s c o l l e a g u e s ，w e d e v e l o p af r a m ef o r f i n i t es t a t e m u l t i a g e n ti n t e r p r e t e d s y s t e m s f u r t h e r , w e i n v e s t i g a t ea g e n t s k n o w l e d g ee v a l u a t i o ni n d i f f e r e n ts e m a n t i c so fv i e w a sar e s u l t ，w e i m p l e m e n t ak n o w l e d g e b a s e dp r o t o c o lv e r i f i c a t i o ns y s t e mk m a s ，a n d u s ei tt ov e r i f ys e v e r a lp r o t o c o l ss u c c e s s f u l l y ab y p r o d u c t o fo u rr e s e a r c h i sa k n o w l e d g e b a s e dp r o g r a m m i n g t o o ll k b l - k e y w o r d ：p r o t o c o l v e r i f i c a t i o n ，l o g i c o f k n o w l e d g e ，m o d e l c h e c k ， m u l t i a g e n ts y s t e m ，k n o w l e d g e b a s e dp r o g r a m m i n g 中山大学硕士研究生毕业论文 唐辉0 1 0 1 8 2 0 0 4 绪论 早在计算机出现之前，人们就已经开始思考“如何设计高效无二意的通信协 议”这个问题，我国古代用于通报敌情的烽火台和用作通讯信号的狼烟就是例证。 然而，时至今日这个问题依然没有得到很好的解决。同时我们看到，由于计算机 硬件和问题规模的限制，许多现存的通信协议仅凭协议设计者的主观意愿和有限 的测试来说明协议的无二意性，这显然是不够的，这样的协议我们只能说，在已 进行的测试中尚未发现协议与规范不符，还远不能说该协议与规范相符。协议验 证正是希望给出一种方法，使得协议设计者通过该方法可以证明他她所设计的 协议是符合规范的。协议验证工具则为协议验证者提供一种自动半自动的验证 手段。 模型检测作为一种自动化验证方法，在协议验证中得到广泛的应用。模型检 测需要两个输入：一是系统，我们需要验证其正确性的一个系统；二是规范，该 系统应具有的性质。模型检测中最大的挑战就是状态空间的爆炸问题。这个问题 源于系统中有许多相互作用，或者系统中有复杂的数据结构，而这些数据结构可 以取许多不同的值。在这种情况下系统状态的数目将变得十分巨大。 模型检测技术的一大优点就是我们可以利用它进行自动化的验证。模型检测 工具通常使用一种对系统的状态空间穷举搜索的过程决定某些规范是否为真。给 予足够的资源，模型检测工具总是以y e s n o 作为回答而终结。这种方法已经成功 应用于许多复杂的电路设计和通信协议验证工作，目前主要用来检测使用时态逻 辑描述的规范。模型检测工具主要有s m v ，s p i n 2 1 等。 知识逻辑口l 常用于对分布式系统中各个实体知识的推理，并用来描述分布式 系统的规范，这些规范准确的描述了系统中各个实体的知识h 。模型检测技术目 前也用来检测知识，这是一个相对新的领域，包括许多重要课题。模型检测知识 问题首先在5 1 中提出。之后关于这方面的研究有【6 ，7 ，8 ，9 1 。 在嘲中对具有完全记忆的同步系统中用知识表述的规范进行了模型检测，在 知识检测方面走出了较重要的一步。m c k t l 伽使用标准程序1 1 1 ( s t a n d a r dp r o g r a m ， 以下简称s p ) 来描述系统，使用知识逻辑和时态逻辑来定义系统规范，m c k 能 够对s p 描述的系统进行这一类规范的模型检测，但m c k 不能检测基于知识的 程序1 ”( k n o w l e d g e b a s e dp r o g r a m ，以下简称k b p ) 所描述的系统规范。 中山大学硕士研究生毕业论文唐辉0 1 0 1 8 2 0 0 4 本文定义了一套k b p 语言_ i ，日j l ( l i r n i t e dk n o w l e d g e - b a s e dl a n g u a g e ) ， 使用该语言作为模型检测输入的系统描述语言，对包含知识的协议验证进行了研 究。 本文的结构如下：在第1 章中介绍我们的研究工作所需要的相关背景知识。 首先引入了一个知识模型，包括其语法和语义模型，并介绍了如何利用该知识模 型刻画多智能体系统，然后讨论多智能体系统中的协议和程序，最后介绍模型检 测技术，主要是符号化模型检测技术。在第2 章中我们讨论模型检测知识的方法。 我们定义了自己的语义模型框架，并给出了利用模型检测技术来计算多智能体系 统中的知识的方法。在第3 章中我们在前章的基础上定义了一套用于模型检测 知识的语言l k b l ，并讨论了其实现细节，包括该系统输入语言的语法和操作语 义。第4 章给出验证实例，并与相关工作进行了比较。第5 章对我们的研究工作 做了一个总结，并提出了进一步研究的方向。 2 中山大学硕士研究生毕业论文 唐辉0 1 0 1 8 2 0 0 4 第1 章基于知识的协议验证的理论基础 本章我将介绍我们的研究工作所需要的相关背景知识和目前该领域的研究 现状。 1 1 知识与多智能体系统 不同的学者对知识有不同的定义，我们的研究基于1 中对知识的定义。 1 1 1 知识的定义 直观上，一个事件可以有许多可能状态，在这些可能状态中只有一个状态是 该事件的真实状态。给定一些信息，智能体可能无法根据已有信息，从这些可能 状态中分辨出事件的真实状态。例如，我在阳光明媚的广州逛街，对于广州的天 气状况这一事件，我认为可能的所有状态中都是阳光明媚，因此我可以确信广州 天气晴朗。另一方面，由于我没有任何关于北京天气状况的信息，在我认为可能 的状态中，北京可能天气晴朗，也可能阴雨绵绵，因此，我不知道北京的天气状 况。直觉上，我需要考虑的可能状态越少，我对外界的不确定性也越少，我知道 的就越多。如果我得到一些额外的信息，例如从朋友那里得知北京现在的天气晴 朗，那么我将不再把那些北京正在下雨的状态当作是可能状态。 为了精确描述这些思想，我们需要某种语言来表达“知道”这一概念，在此 我们使用模态逻辑语言作为我们的描述语言。 假设n 个智能体构成一个系统，我们依次称这n 个智能体为1 ，1 1 。为 了简化，我们假定这些智能体能够推理一些由非空原子命题集m 所描述的可能世 界，中中的原子命题一般记作p , p ，q , q ，。这些原子命题代表着客观世界的 一些基本事实，例如“广州天气晴朗”，为了表达像“我知道广州天气晴朗”这 样的陈述，我们引入模态词k 。，k 2 ，k 。( 每个智能体一个) ，k 。p 读作“智 能体1 知道p ”。 定义l ：公式 1 命题变元是公式； 2 如果p 是公式，那么1 p 是公式； 3 如果p 和q 是公式，那么( p a q ) 是公式； 4 如果p 是公式，那么k i p 是公式，其中i _ l ，2 ，n ； 中山大学硕士研究生毕业论文唐辉0 1 0 1 8 2 0 0 4 5 当且仅当能够通过有限次应用1 、2 、3 、4 构造出来的符号串是公式。 为了简便易读，在不引起混淆的情况下，可以省略公式中的括号，例如公式 ( p q ) 简记为p a q 。根据命题逻辑的标准简化规则，把弋_ 1 p a _ 1 q ) 简记为p v q ； - 1 p v q 简记为p _ q ；( p _ q ) a ( q - - q ) 简记为p hq ；t r u e 作为永真公式，例 如p v q ，的缩写：一t r u e 简记为f a l s e 。 使用这种语言我们能够用一种简明的方式表达非常复杂的陈述。 例如，公式 k l k2 p 1 k 2 k 1 k 2 p 表示智能体1 知道智能体2 知道p ，但智能体2 不知道智能体1 知道智能体 2 知道p 。 可能性可以看成是双重知识。因此，智能体1 认为p 可能，当且仅当智能体 1 不知道，p 。这种情况可以用公式- 1 k 。一p 来描述。像“我不知道p 是否成立” 这样的陈述表达了我认为p 和_ p 都有可能。 1 1 2 语义模型 我们已经描述了语言的句法，现在我们需要给出语意。如前所述，我们将采 用可能世界模型语义，该语义模型可以使用k r i p k e 结构 1 2 1 来形式化描述。原子 公式集中上含有n 个智能体的k f i p k e 结构m 是一个n + 2 元组( s ，兀k ，k 。) ，其 中，s 是状态( 可能世界) 集：冗是一个解释，它为公式集中中的原子命题在每 一个状态下指派一个真值，即n ( s ) ：西- - t r u e ，f a l s e 对每一个状态s s ；1 c i 是s 上 的二元关系。 随着二元关系k ；的变化，k r i p k e 结构m 所具有的性质也发生变化，在此我 们考虑一种理想情况，即二元关系1 c ；是在状态集s 上的等价关系，这样，k i 将具 有自反性、对称性和传递性。我们取k 。为等价关系，原因在于我们希望描述这样 一种直觉：如果在状态s 和t 智能体i 关于可能世界的信息都相同，那么智能体 i 在状态s 时会认为状态t 也是可能的，也就是说这两个世界对这个智能体来说是 不可区分的。 4 中山大学硕士研究生毕业论文唐辉0 1 0 8 2 0 0 4 定义2 ：f - 关系 1 ( m ，s ) f = p ( 对原子命题p m ) 当且仅当兀( s ) ( p ) = t r u e ； 2 ( m ，s ) j = _ 1 p 当且仅当( m ，s ) | p ： 3 ( m ，s ) b p q 当且仅当( m ，s ) i _ p 并且( m ，s ) b q ； 4 ( m ，s ) 卜k j p 当且仅当v t ( ( s ，0 k i ) 有( m ，t ) 辟p 。 从上述对b 关系的定义可以看出，定义2 中的1 3 与经典命题逻辑的定义一 致，其与经典命题逻辑的区别在4 ，4 的直观解释为，只有在智能体i 考虑的所 有可能世界中p 都成立，智能体i 才能确定p ，即它知道p 。 1 1 3 多智能体系统中的知识 本节我们考虑多能系统中的知识表示的问题 运行路径和系统( r u n sa n ds y s t e m s ) 我们所考虑的系统是个由多个智能体构成的系统，每个智能体在任一时间 点都处于某个状态。在本文中，我们认为任何相互作用的多个智能体的集合是一 个多智能体系统。例如，在运行特定协议的计算机网络中，多个进程构成的分布 式系统组成了一个多智能体系统。通常，多智能体系统极为复杂，推理系统中单 个智能体的行为也很困难。例如，在考虑泥巴小孩问题时如果我们试图详尽的模 拟这个系统，我们不得不把小孩一生中发生的所有事情包括进来，对他们的所见 所闻，他们的动作，全都详细的描述出来。这样，小孩所有可能的状态几乎无穷 无尽。所有这些因素，原则上都会影响这些小孩的行为。 对于这种情况，我们把注意力仅仅集中在部分细节上，并要求这些细节包括 了与我们分析有关的所有信息。为了进一步降低问题的复杂度，必须寻找更理想 的方法去考虑系统，因此我们需要一个理想化的多智能体形式化模型。该模型允 许我们把握多智能体系统中所有的重要特性，而不拘于太多的细节。 我们假设在任何一个时间点上，系统中的每个智能体都处于某种状态，该状 态封装了智能体能访问到的所有的信息，我们称之为智能体的局部状态。在我们 的抽象框架中，我们不对状态做任何附加的假设。一旦我们认为每个智能体有一 个状态，很自然的，我们认为整个系统也处于某个状态。从概念上，我们把一个 中山大学硕士研究生毕业论文 唐辉0 1 0 1 8 2 0 0 4 系统分成两部分：智能体和环境。环境可认为是“系统中与智能体有关的任何其 他东西”。通常，环境也可以看成是另一个智能体。这样，系统的全局状态定义 为n + 1 元组，形如： s = ( s 。，s ”，s 。) 其中，s 。是环境状态，s i 是智能体i 的局部状态。全局状态可以描述给定 时间点的系统。但是，系统不是一个静态的实体，它会不断变化。既然我们感兴 趣的是系统如何随着时间而变化，我们把时间加入我们的模型。我们定义运行路 径是一个从时间域t 到全局状态域g 的函数。这样，一条g 上的运行路径可以 用一个全局状态序列唯一标识。 我们假设系统时间在自然数上取值，这意味着时间步是离散和无穷的。一个 系统可以有许多可能的运行路径，因为系统的全局状态能够以许多可能的方式演 化：系统存在许多可能的初始状态，许多情况可以在系统的各个状态发生。为了 描述这种情况，我们形式化的定义一个系统是一个非空运行路径集。 定义3 ：运行路径和多智能体系统 设l 。是环境状态集；对i - - 1 ，n ，l ；为智能体i 的局部状态集。 g = l 。x l l l 。为全局状态集。在g 上的一个运行路径l u l l 用g 中全局状态 的一个序列标识。我们把由一个运行路径r 和时间m 构成的一个序对( r ，m ) 称为一 个点。如果r ( m ) = ( s 。，s ，s 。) 是在点( r m ) 的一个全局状态，我们定义t o ( m ) = s 。 并且对i ：1 ，n 有r i ( m ) = s ；成立。因此( m ) 是智能体i 在( r m ) 点的局部状态。 在g 上的系统r 是g 上的运行路径集。如果r r ，我们说( r ，m ) 是系统r 的一 个点。 在系统中加入知识 通常，我们认为一个智能体的动作取决于它的知识。事实上，前述框架已经 可以直接表示知识。基本思想是，像“智能体a 在系统r 中不知道p ”这样的 陈述，就系统r 而言，意味着在系统的某个点( r m ) 上p 不成立。我们认为，智 能体a 在系统r 中的知识由它的局部状态决定，因此智能体a 不能分辨系统r 中有相同局部状态的两个点，但它能分辨局部状态不同的点。我们可以形式化这 6 中山大学硕士研究生毕业论文 唐辉0 1 0 1 8 2 0 0 4 些思想。 我们看到，前述由运行轨迹构成的系统可被看成是一个k r i p k e 结构，只是 这个结构没有函数万来告诉我们如何把一个真值赋值给原子命题。为了将系统和 k r i p k e 结构统一，我们需要引入解释系统。我们假设有一个原子命题集巾，该 集合描述了系统的基本事实。为了简化，我们假设命题逻辑能够描述系统的所有 基本属性。 定义4 ：解释系统 解释系统l 由一个序对( r ，石) 组成，此处r 是在一个全局状态集合g 上的一 个系统，石是一个在g 上对中命题的解释，该解释对全局状态中的原子命题 进行真值赋值。因此，对于每个p 中和状态s g ，我们有刀( s ) ( p ) e t r u e ，f a l s e ) 。 当然，万也包括r 上点的解释；我们只要简单的令s r ( r ，i t i ) = 刀( r ( m ) ) 。必须 注意和l 是系统r 的内部属性。它们在r 上构成了附加结构，这些结构是我 们作为外部的观察者，为了方便而增加的，用来帮助我们更好的分析和理解 系统。我们分别称系统r 中的点和状态为点和状态。也就是，如果r r 我们说 点( 蛐1 ) 在解释系统i = ( r ，万) 中。同样，如果r 是在状态空间g 上的系统，我们 说i 也是在状态空间g 上的系统。 为了定义解释系统中的知识，我们需要把一个解释系统i = ( r ，t ) 跟一个 k i p k e 结构m 。= ( s ，万，f t ，茁。) 联系起来：s 仅包含i 中运行轨迹上的点，芷”，j r 。 是s 上的二元关系。我们注意到，对于环境不存在可能关系( e ：这是因为通常 我们对环境知道什么不感兴趣。为了定义可能关系峨，我们需要如下定义 定义5 ：不可区别关系一 设s = ( s 。，s 1 ，s 。) 和s = ( s 。，s l ，s 。) 是r 中的两个全局状态，如果智能体 i 在s 和s ，中有相同的状态，即s i - - s i ，那么我们说s 和s 对于智能体i 是不可区 别的。记作s ，s 。我们可以把不可区别关系。扩充到点上：如果“m ) ；r ( m 。) ， 我们说点( r m ) 和点( r ，m ) 对i 而言是不可区别的，记作( r m ) i ( r ，m ) 。 显然，：是点上的等价关系。当我们提到解释系统中的知识时，我们假设 7 中山大学硕士研究生毕业论文唐辉0 1 0 1 8 2 0 0 4 m i 中的可能关系k 由一；定义。直觉上，如果s 和s 对智能体i 来说是不可区别 的，在状态s 智能体i 认为状态s 也是可能的状态。因此，智能体的知识完全 由它们的局部状态决定。 建立起解释系统i 与k r i i p k e 结构的联系后，我们有 ( i ，r ，m ) i = p 当且仅当( m 。，s ) p ，其中s = ( r m ) 这样，我们可以通过解释系统给出多智能体系统的一个语义解释。设。是原 子命题集，仿照1 1 1 中的语言定义和1 1 2 中的语义解释，我们有 1 ( i ，r ，m ) p ( 对原子命题p m ) 当且仅当冗( r ，m ) ( p ) = t r u e ； 2 ( i ，r ，m ) j _ 1 p 当且仅当( i ，r ，m ) 睁p ； 3 ( i ，r ，m ) i _ p a q 当且仅当( i ，r ，m ) p 并f i ( i , r ，m ) | _ q ； 4 ( i ，r ，m ) k i p 当且仅当v ( r ，m 1 ) ( r ，m ) 一i ( r ，m 1 ) 有( i ，r ，m ) p 。 在系统中加入时间 前述语言的表达能力还是不够强，甚至对于像位传输这样的简单情况也不能 很方便的处理。例如，当我们需要诸如“接收者最终知道发送者的初始位”这样 的陈述式，前述语言就无能为力了。 为此，我们加入时间模态词，主要考察四个模态词：口( 总是) ，( 最终) ， o ( 下一时刻) ，u ( 直到) 。直觉上，如果p 在现在和将来都为真，那 么o p 为真；如果p 在未来某一个时刻为真那么p 为真；如果p 在下一个时刻 为真那么o p 为真；如果p 为真直到q 为真，那么p u q 为真a 在解释系统中形式 化定义如下 ( i ，r ，m ) b v l p 当且仅当( i ，r ，m ) b 对于所有m m ( i ，r ，m ) 卜p 当且仅当( i ，r m ) h 对于某个i r l m ( i ，r m ) 卜o p 当且仅当( i ，r ，m + 1 ) h ( i ，r m ) 卜p u q 当且仅当( i ，r ，m 1 ) i - p 对于某个m 1 m 并且( i ，r ，i r l 2 ) i _ q 对于所有m m 2 m 1 我们对于o p 解释为“p 在下一步成立”是有意义的，因为我们对于时间的 观念是离散的。通常，时态词可用于推理在一个运行轨迹上发生的事件。例如， 巾山大学硕士研究生毕业论文唐辉0 1 0 1 8 2 0 0 4 对于位传输问题，公式 ( r e c b i t = r e c a c k ) 解释为：在一个运行轨迹的某个点上， 如果接收者收到发送者发送的一个数据位，那么在该运行轨迹的将来某个时刻， 发送者将会接收到接收者发出的确认信息。通过结合时态和知识算子，我们可以 对系统中知识的演化做出断言。例如，我们可能会做出“接收者最终知道发送者 初始的位”的断言。这个断言现在可以用下面的公式表示： ( k r ( b i t = o ) v k r ( b i t = 1 ) ) 我们定义的这些时态算子仅仅能描述目前和将来发生的事情，不能描述过去 发生的事情。不过，这些算子对于我们的许多应用来说已经足够了。 1 2 协议与程序 在前面我们并没有提到运行轨迹从何而来，是什么引起系统改变状态。直觉 上，这些改变是环境和智能体的动作执行的结果。通常，智能体是按照它们的协 议来执行动作的，这些协议又常常被表示为程序。在这一节，我们将讨论协议和 程序。 1 2 1 动作 正如我们直觉上认识到的那样，智能体通过动作改变其所处的环境状态，从 而改变整个系统的状态。通常我们假设对于智能体i 有一个动作的集合，a c t i 代表它能执行的动作。为了统一和简化处理，我们把环境也看成是一个智能体， 允许环境执行a c t e 集合中的动作。对智能体和环境而言，我们允许它们执行 个特别的空动作a ，这个动作与智能体和环境没有执行任何动作相对应。 如果仅仅知道某个智能体所执行的动作，这对于确定系统全局状态的改变是 不够的。在系统中不同的智能体同时执行的动作可能相互作用。如果两个智能体 同时朝相反的方向推门，结果可能是不确知的，我们不能仅仅根据两个动作的执 行结果进行简单的叠加来计算。又比如两个进程同时对一个寄存器写入一个值， 结果会发生什么事情也是不确定的。为了处理动作中潜在的相互作用，我们需要 考虑联合动作。一个联合动作是一个形如( a 。，a ，a 。) 的元组，元组中的a 。代表 由环境执行的动作，a i 代表由智能体i 执行的动作。 为了能使用联合动作来描述系统状态的改变，我们需要把每个联合动作 ( a 。，a 。，a 。) 关联到一个迁移算子t 上。全局状态迁移算子t 是全局状态到全局 9 中山大学硕士研究生毕业论文 唐辉0 1 0 1 8 2 0 0 4 状态的函数，即，t ：g _ g 。联合动作通过与其关联的迁移算子t 来改变系统 状态。如果( a 。，a ，a 。) 执行时系统处于全局状态s 中，那么系统执行 ( a 。，a ，a 。) 后，系统状态将变为t ( s ) 。因此，无论何时，当我们讨论一个动作 时，我们都将有一个与之关联的映射f 和一个全局状态迁移函数f ( a 。，a ，a 。) 。 我们要求r ( a 。，a ，a 。) ( s 。，s ，s 。) 对于每一个联合动作和每个联合状态都有 定义。 1 2 2 协议和上下文 智能体通常根据一些协议来执行动作，协议是选择动作的一个规则。直觉上， 一个智能体i 的协议描述了智能体i 可以执行的动作，该描述通过智能体i 的局 部状态的函数给出。我们形式化的定义一个智能体i 的协议r 如下： 定义6 ：智能体的协议 设l ；是智能体i 的局部状态集，a c 工是智能体i 的动作集，智能体i 的协议 e ：l ；- 2 “q 当然，在智能体执行动作时，协议给定的这些动作中仅有一个被真正执行； 动作的选择是非确定的。一个确定协议在状态到动作上做一对一的映射，即，它 为每一个局部状态规定了唯一的动作。形式上， 如果对于每个s ；l ，都有ip i ( s ，) i ：1 ，那么p i 是确定的。 作为一个约定，如果p i 是确定的，那么我们一般把p i ( s i ) = ( a 写成p i ( s i ) - 一a 。 正如1 1 3 所讨论的那样，我们把环境看成是一个特殊的智能体，这样环境 也需要运行一个协议。我们定义环境的协议为一个从l 。到非空a c l 子集的一个 函数。虽然这样定义的协议概念是非常通用的，此处有一个关键的限制：协议函 数是局部状态的函数，而不是全局状态的函数。这一点也反映了我们已经把智能 体的所有信息编码进它的局部状态这一思想。因此，一个智能体可以做的事取决 于它的局部状态，而不是全局状态。再者，上述对协议的定义过于普遍以至于可 以设计出一些不可算的协议函数。当然，在实际应用中我们一般只对可算的函数 感兴趣。这里可算的协议函数是指，对于该协议有一个算法以局部状态作为输入， 1 0 中山大学硕士研究生毕业论文唐辉0 1 0 1 8 2 0 0 4 结果返回协议在这个状态定义的动作集。 进程并不单独的运行它们的协议，在多智能体系统中所有智能体运行的协议 的组合让系统以一种特定的方式动作。我们定义一个联合协议p 为包括每一个智 能体i 的协议e 的元组( p j ，p 口) 。注意，虽然我们确实把环境的动作包括进联合 动作a c t 中，这里我们并没有把环境的协议包括在联合协议中。这是因为环境 在多智能体系统中是一个特殊角色：通常在定义和分析智能体的协议时，我们把 环境的协议作为一个给定的条件。实际上，当我们设计多智能体系统时，环境通 常被看成是一个反面行为，它可能试图让系统表现出一些不合常理的行为。换而 言之，联合协议p 和环境的协议p e 能被看成是对立的游戏者的策略。 联合协议p 和环境的协议p e 给定了系统所有参与者的行为，决定了系统的 全部的行为。进一步考察发现，协议描述的仅仅是智能体和环境采取的动作。为 了确定系统的行为，我们还需要知道联合协议执行的上下文。这样一种上下文由 什么构成呢? 显然，环境的协议p e 应该作为上下文的一部分，因为它决定了环 境对于联合动作的作用。另外，上下文还应该包括迁移函数t ，因为正是t 描述 了联合动作的结果。此外，上下文还应该包括初始全局状态集g o ，因为它描述 了协议开始执行时系统的状态。许多时候，我们还希望考虑更多的对于环境行为 的全局限制，这些限制不容易用p c ，t ，g o 来描述。我们使用一种最简单的方 式，即，指定运行路径上的一个条件，用来确定那些我们可以接受的运行路径。 形式上，v 是运行路径的集合：如果运行路径r 满足条件，那么r v 。 有了上述讨论，我们可以定义协议的上下文。 定义7 ：协议上下文 协议上下文y 是一个四元组y = ( p o ，g 。，f ，、王，) ，其中p o ：k 一 2 a c n a ) 是一 个环境的协议，g o 是一个g 的非空子集，t 是一个迁移函数，是运行路径上 的一个条件。 上下文给我们提供了一个形式化的方式去描述我们对于系统的一些假设。在 许多情况下，当我们定义一个上下文时，在我们心里我们有特定的原子命题集合 中，和在g 上对西的一个特定的解释n 。一个解释上下文是由上下文y 和一个解 释n 组成的序对( y ，石) 。 中山大学硕士研究生毕业论文唐辉0 1 0 1 8 2 0 0 4 我们现在可以讨论在给定的上下文中协议的运行路径。如果下面的条件成 立，我们说一个运行路径r 与一个联合协议p = ( p 1 ，p n ) 在上下文 ，= ( r ，g o ，f ，甲) 是一致的： 1 r ( o ) g 。( 因此r ( o ) 是合法的初始状态) 2 对于所有m 0 ，如果“m ) = ( s e s ，s n ) ，那么存在一个联合动作 ( a 。，a l ，a 。) v o ( s 。) x p d s l ) p n ( s 。) 满足r ( m + 1 ) = z ( a 。，a l ，a 。) ( r ( m ) ) 3 r 、壬， 因此，如果r 是在上下文7 中p 所描述的动作的可能行为，那么r 在上下文7 中与p 一致。 1 2 3 程序 如前所述，协议是从局部状态到动作集的函数。在实际应用中，我们需要某 种程序语言书写的程序来描述协议。考虑位传输协议中的接收者r ，在它从发送 者s 那里接到一个位后，它开始发送a c k 。这一陈述可以用“f f r e c b i t d os e n d a c k ” 这样的程序来描述。这个陈述的实质是，程序根据一个完全依赖于局部状态的测 试结果选择一个动作。 我们现在举例描述一个简单的编程语言，它足够用来描述协议，它的语法强 调这样一个事实：智能体根据对它的局部状态测试的结果来选择执行的动作。一 个智能体i 的程序是一个如下的陈述： c a s e o f i f t t d oa l i f t 2 d oa 2 e n dc a s e 其中，t i 是对智能体i 的标准测试，a j 是智能体i 的一个动作。( 我们称这些 程序是标准程序，以便和我们后面引入的基于知识的程序区别开来。) 智能体i 的标准测试通常是一个原子命题集合o i 上的命题公式。直觉上，一旦我们知道 怎样在l i 的局部状态中计算这个测试，我们就能够把这个程序转化为l i 上的一 个协议：在一个局部状态，智能体i 非确定的选择在c a s e 陈述中测试结果为真的 1 2 中山大学硕士研究生毕业论文 唐辉0 1 0 1 8 2 0 0 4 一个子句，并执行相应的动作。 我们希望通过一个解释n 来计算这个测试的值。但是，并非任意一个解释都 能做到这一点。我们希望程序中对于智能体i 的测试是局部的，即，该测试仅决 定于智能体i 的局部状态。让智能体i 的动作取决于不是由它的局部状态的值能 确定的测试结果是不合适的。 定义8 ：与程序相容的解释 如果一个对g 中全局状态的解释n ，对于p g 。中的每一个命题都局部于智能 体i ，那么，我们说该解释n 与智能体i 的程序聘；相容，即，如果在飑；中出现 q ，状态s 和s 分别是g 中的两个状态，并且s 一；s ，那么石( s ) ( q ) = z ( s ) ( q ) 。 如果口是一个命题公式，它的所有原子命题都局部于智能体i ，并且a 满足 万( s ) ，其中s = ( s 。，s i ，s 。) 是一个全局状态，i s i = z ，那么记作忉，z ) j - 口。因 为口中的所有原子命题对智能体i 而言都是局部的，只要i 在全局状态s 的局部 状态是l ，我们选择哪一个全局状态s 并不重要。据此有如下定义， 定义9 ：与程序相容的协议 p g ；是智能体i 的程序，万是与p g ；相容的解释，我们定义与飑；相容的协 议，用p g ；”表示，为： p g ；”c z ，= 器，：篡! i 皇i t i 曼! 嚣嘉# ；：暑苫焉舅差 直觉上，p g 。”从满足测试的子句中选择所有的动作，如果没有测试满足就选 择空动作a 。通常情况下我们得到的是一个非确定的协议，因为对于一个给定的 状态，可能会有多个测试满足。 有了上述定义，我们可以定义一个联合程序p g = ( p g ，p g 。) ，其中p g ，是 智能体i 的程序。设解释石与每一个智能体的程序p g ；都相容，由p g 和石可以得 到一个联合协议p 9 4 = ( p g ，1 ，p g t l 4 ) 。联系前一节引入的解释系统，如果石与p g 相容并且解释系统i = ( r ，万) 表示了对应的联合协议赡”，那么我们称解释系统 i = ( r ，万) 在解释上下文( y ，石) 中表示了一个联合程序p g ，记作i ”( p g ，”力a 中山大学硕士研究生毕业论文唐辉0 1 0 1 8 2 0 0 4 与一般的程序语言相比，如c 或f o r t r a n 等，我们的标准程序在语法形 式上有更多的限制。在c 或f o r t r a n 这样的语言中，一般会看到如：f o r ，w h i l e 或者i f t h e n e l s e 这样的结构。包含这种结构的程序，其语义依赖于隐含了指 令指针的局部状态，指令指针指明在当前的局部状态中将要执行的命令。由于我 们显式的构建智能体的局部状态，在我们的框架里可以通过显式的在局部变量中 说明指令指针的取值来模拟这些结构。程序中的局部测试t i 也能显式的引用这个 变量，动作a j 也可以显式的对该变量赋值。 如果我们有足够丰富的原子命题集，很显然我们想要的每一个协议都可以由 一个标准程序导出。我们的编程语言甚至比许多其它的语言更普遍：一个程序可 以导出一个不可计算的协议。但通常我们只对能导出可计算协议的程序感兴趣。 实际上，标准程序通常满足一个更强的要求：它们是一个有限的描述，它们导出 确定的协议。 1 2 4 程序的规范 在设计和分析一个多智能体系统时，我们一般希望我们的系统满足一些性 质。通常情况下，我们首先确定我们希望得到的性质，然后再去设计一个满足这 些隆质的协议。例如，对于位传输协议我们希望得到的是发送者把这个位传送给 接收者。我们称这个性质为我们所考虑的系统或程序的规范。一般来说一个规范 是通过对“好的”系统的描述给定的。因此，一个规范可以标识一类解释系统， 一类“好的”解释系统。如果一个解释系统i 在某个规范盯所标识的一类系统中， 即，i 盯，那么我们称该解释系统i 满足规范仃。 在实际应用中，许多规范都属于一种基于运行路径( r u n - - b a s e d ) 的特定规范 类型。基于运行路径的规范一般作为运行路径的一个属性而给出。通常基于运行 路径的规格可以用包括模态词的公式来表示。如果一个系统的所有的运行路径满 足一个基于运行路径的规范，我们称该系统满足这个规范。例如，对于位传输问 题的一个可能的规范是：“接收者最终从发送者那里接到那个位，发送者最终会 停止发送这个位”：这个规格可以表示为r e c b i t a 口一s e n d b i t 。 尽管实际中最常出现的是基于运行路径的规范，不基于运行路径的规范也是 合理的。例如，在位传输问题中，对于发送者行为的规范可以是：“如果发送者 知道接收者- 0 k n 发送的位信息，那么发送者停止发送位信息，否则发送者将一直 1 4 中山大学硕士研究生毕业论文唐辉0 1 0 1 8 2 0 0 4 向接收者发送位信息。”这个规范用发送者知识的形式给出，该知识依赖于整个 系统，单独考虑各个独立的运行路径并不能确定。这种规范可以看成是为基于知 识的( k n o w l e d g e - - b a s e d ) 规范。更一般的，我们称用认知模态词表达的规范为基 于知识的规范。与基于运行路径的规范不同，基于知识的规范指定的是整个解释 系统的属性，而不仅仅是某条运行路径上系统所具有的属性。 1 2 5 基于知识的程序设计 我们对于标准程序的概念非常简单，在标准程序中，每个智能体根据局部状 态测试的结果执行动作。如1 2 3 节所述，这种程序足以用来描述协议。然而， 标准程序不能用来描述知识和动作的关系，这种关系通常又是我们想要描述的。 这个问题可以通过泥巴小孩问题来理解。 泥巴小孩问题：有n ( n 1 ) 个小孩在一块玩，小孩的母亲告诫他们不要弄 脏额头，如果谁弄脏了，她就会惩罚谁。每个小孩都想保持干净，同时他们每个 人都希望看到其他人弄脏额头。在玩耍时，有一些小孩弄脏了额头，假设有k ( 1 c 妊；n ) 个。每个小孩都可以看到别人额头是不是脏了，但是不能看到自己的 额头是不是脏了。当然，每个小孩都不会告诉别人他额头是否脏了。这时，小孩 的父亲来了，他说：“你们当中至少有一个人额头脏了- t * 9 接着反复问小孩“你们 谁知道自己额头脏了没有? ” 在泥巴小孩问题中，小孩被父亲问他们是不是知道他们的额头有没有泥巴。 如果他们知道，他们就回答“y e s ”，否则回答“n o ”。如果我们用命题公式p ；表 示“小孩i 的额头有泥巴”，很自然，我们认为小孩i 按照下面的程序m c ；动作： c a s e o f i f c h i l d h e a r d i ( k p ivk i l p i ) d o s a y “y e s ” i f c h i l d h e a r d ii x ( 一k i p ，v1 k i p i ) d o s a y “n o ” e n dc a s e 在这里c h i l d h e a r d i 是一个原子命题，在一个给定的状态，如果在这一轮中 小孩i 听到父亲的问题“你们谁知道自己额头脏了没有? ”，那么这个命题为真 不幸的是m c i 并不是我们定义的一个标准程序。除了命题测试，这个程序也测 试知识，例如：( k ，p ivk 。、p ；) 。而且，对于这个例子我们不能用前面的技巧把 一个协议和一个程序联系起来，因为这样的知识测试不能通过仅仅查看局部状态 来判断其真假值。 我们称这种形式的程序为基于知识的程序，以便跟我们前面定义的标准程序 相区别。形式上，智能体i 的一个基于知识的程序有如下形式： c a s e o f i f t l 八k ld oa 1 i f t 2 八k 2d oa 2 e n dc a s e 此处，表示标准测试，k j 是智能体i 的知识测试。直觉上，智能体根据在 其局部状态上执行的标准测试及根据其“知识状态”执行的知识测试所得到的结 果来选择动作。我们定义一个基于知识的联合程序为p g = ( p g ，p g 。) ，每个智 能体有一个基于知识的程序。 我们已经描述了基于知识程序的语法，现在需要定义基于知识程序的形式化 语义。与1 2 4 节中从一个标准程序导出给定上下文中智能体动作的一个协议相 似，我们希望从一个基于知识的程序导出一个协议。一个协议是从局部状态到动 作集的函数。为了从一个标准程序到一个协议，我们需要做的所有工作就是在给 定的局部状态中计算标准测试的真假值，该计算必须用到解释。对于一个基于知 识的程序，我们还需要计算知识测试的真假值。在我们讨论的框架下，知识测试 依赖于整个解释系统，而不仅仅是局部状态。 为了解决这个问题，给定一个解释系统i = ( r ，刀) ，我们把一个基于知识的 联合程序您= ( p g ，p g 。) 关联到一个联合协议飚1 = ( p g 1 ，赡。1 ) 上。直觉上， 我们根据石计算飚中标准测试的真假值，根据i 计算p g 中知识测试的真假值。 像在标准程序中那样，我们要求石跟聘相容，即，出现在p g ；标准测试中的每 一个命题对i 而言都是局部的。注意，我们只对出现在标准测试中的命题有局部 性要求，对知识测试中的命题并没有这种要求。 我们希望对智能体i 的所有局部状态l 定义p g ；( z ) 。为了定义这个公式，首 先我们给出在一个解释系