（逻辑学专业论文）时态公开宣告逻辑初探.pdf

两南人学硕十学伊论文摘要 时态公开宣告逻辑初探 逻辑学专业硕士研究生张丽 指导教师唐晓嘉教授 摘要 在描述多主体间相互作用的过程中，公开宣告逻辑关注于在公开宣告发生后主体 的认知状态如何改变；认知时态逻辑关注于在主体的相互作用中能够发生哪些信息事 件。本文旨在讨论一个能刻画这两个方面的时态公开宣告逻辑系统t p a l ，t p a l 是 结合公开宣告逻辑和认知时态逻辑而形成的逻辑系统。 第一部分：首先讨论了公开宣告逻辑系统p a l ，该系统是动态认知逻辑系统 d e l 的一种特殊情况，它能够刻画在公开宣告这种行为发生之后主体知识的变化。 接着，讨论了认知时态逻辑系统e t l ，该系统能够描述在一些信息化的过程中知 识在时间进程上如何发展，能够对不同情景中的相关交流限制给出刻画。 第二部分：首先在这部分讨论了如何从p a l 生成e t l _ 模型，并给出实例予以 说明。接着，讨论了p a l 与e t l 之间的关系，p a l 协议并不能生成所有的认知模型。 实际上，这种e t l 模型具有一些特殊的性质，并得出一个典型的定理。 第三部分：结合公开宣告逻辑系统和认知时态逻辑系统，将认知模型中的认知 状态指派为公开宣告序列集，以讨论时态公开宣告逻辑系统t p a l 。但是，t p a l 并不能归约到p a l 中，因此采用h e n k i n 方法证明该系统是完全的。t p a l 与r 址 之间的关系不是很显然。 第四部分：对t p a l 做出评价，指出不足之出，并指明在未来需要进一步研究 的问题。 关键词：公开宣告逻辑认知时态逻辑协议p a l 生成e t 卜模型 两南大学硕十学位论文a b s 仃a c t a p r e l i m i n a r ys t u d yo nt e m p o r a lp u b l i c a n n o u n c e m e n tl o g i c m a jo r ：l o g i ca u t h o r ：z h a n gl i s u p e r v i s o r ：p r o f e s s o rx i a o j i at a n g a b s t r a c t i nd e s c r i b i n gm u t i - a g e n ti n t e l l i g e n ti n t e r a c t i o n ，p u b i ca n n o u n c e m e n tl o g i c ( p a l ) c o n c e r n sh o w a g e n t s e p i s t e m i cs t a t e sc h a n g ew h e nt r u ei n f o r m a t i o mi sp u b l i c l ya n n o u n c e d e p i s t e m i ct e m p o r a l l o g i c ( e t l ) c o n c e r n sw h a ti n f o r m a t i o ne v e n t sc a nt a k ep l a c ei nt h ec o u r s eo fa g e n t s i n t e r a c t i o n i n t h i st h e s i s ，al o g i cs y s t e mw i l lb ed i s c u s s e d - - - - - t e m p o r a lp u b i ca n n o u n c e m e n tl o g i c ，w h i c hc a n c a p t u r eb o t ht w oi m p o r t a n ti n g r e d i e n t sa n dm e r g e st h es e m a n t i cf r a m e w o r ko fp u b i ca n n o u n c e m e n t l o g i ca n de p i s t e m i ct e m p o r a ll o g i c p a r to n e ：p u b i ca n n o u n c e m e n tl o g i c ，t h ep r i m ee x a m p l eo fd y n a m i ce p i s t e m i cl o g i c ( d e l ) ， d e s c r i b e sh o wa g e n t s e p i s t e m i cs t a t e sc h a n g ew h e nt r u ei n f o r m a t i o mi s p u b l i c l ya n n o u n c e d s e q u e n t i a l l y , e p i s t e m i ct e m p o r a ll o g i c d e s c r i b e sh o wk n o w l e d g ee v o l v e so v e rt i m ei ns o m e i n f o r m a t i o n a lp r o c e s sa n dc a ns t r a i g h t f o r w a r d l yc a p t u r er e l a t i v ec o m m u n i c a t i o nc o n s t r a i n t si n v a r i o u ss i t u a t i o n s p a r tt w o ：f i r s t l y , w ei n 仃o d u c eh o wc a i lg e n e r a t ee t l m o d e l sf r o mp a la n ds u p p o r taf e w e x a m p l e s s e c o n d l y , w ed i s c u s st h er e l a t i o nb e t w e e np a la n de t l n o ta l le t lm o d e l sc a nb e g e n e r a t e db yap a lp r o t o c 0 1 i nf a c t ，s u c hg e n e r a t e de t l - m o d e l sh a v ean u m b l eo fs p e c i a l p r o p e r t i e s p a r tt h r e e ：t e m p o r a lp u b i ca n n o u n c e m e n tl o g i cw h i c hm e r g e st h es e m a n t i cf r a m e w o r ko fp u b i c a n n o u n c e m e n tl o g i ca n de p i s t e m i ct e m p o r a ll o g i ca n da s s i g n st oe a c hs t a t ei nag i v e ne p i s t e m i c m o d e las e to fs e q u e n c e so fp u b i ca n n o u n c e m e n t s b u t ，t p a lc a n tr e d u c et op a l s o ，t h ep r o o fo f c o m p l e t e n e s si sav a r i a n to ft h es t a n d a r dh e n k i nc o n s t r u c t i o n t h er e l a t i o nb e t w e e nt p a la n dp a l i sn o ti m m e d i a t e l y p a r tf o u r ：ic o m m e n to nt h et p a l ，a n dg i v es o m ep r o b l e m sf o rf u r t h e rr e s e a r c hi nt h ef u t u r e k e yw o r d s ：p u b i ca n n o u n c e m e n tl o g i ce p i s t e m i ct e m p o r a ll o g i c p r o t o c o l p a l g e n e r a t e de t l m o d e l i i 独创性声明 学位论文题目：j 嚣 _ 盔互主 堇王望己塞翌刍黉挫 本人提交的学位论文是在导师指导下进行的研究工作及取得的研 究成果。论文中引用他人已经发表或出版过的研究成果，文中已加了 标注。 学位论文作者： 张两签字日期：2 汐哆年 乡月0 日 学位论文版权使用授权书 本学位论文作者完全了解西南大学有关保留、使用学位论文的规 定，有权保留并向国家有关部门或机构送交论文的复印件和磁盘，允 许论文被套阅和借阅。本人授权西南大学研究生部可以将学位论文的 全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或扫 描等复制手段保存、汇编学位论文。 ( 保密的学位论文在解密后适用本授权书，本论文：口不保密， 口保密期限至年月止) 。 学位论文作者签名：弓氏雨导师签名：弦蟓 签字日期：2 0 0 罗年亏月i o 日 签字日期：二国罗年f 月0 日 两南大学硕十学伊论文文献综述 文献综述 认知在很多情况下是多个主体间相互作用的活动。在描述多主体间相互作用的过 程中，存在两个重要的方面。一是关注于在有关的信息事件发生后主体的认知状态如 何改变。就如同我们日常观察到的情况一样，最简单的信息事件都能够影响主体的知 识，因此，把握住信息事件和它们的认知结果就显得很重要。另一个方面关注于在主 体的相互作用中能够发生哪些信息事件。例如，在我们每天的谈话中，总是存在一些 特定的礼仪性的“协议 ，诸如“不要重复说你说过的话”、“不要抢着说话”等。同 时，在游戏中，对参与者怎样交流他们的信息也要做出具体的说明。为了正确地处理 这一些问题，刻画出交流中限制的种类就显得非常重要，例如，是否能够或者怎样能 够达到我们感兴趣的认知状态。 为了形式化地处理信息变化，人们将行动作为模态引进认知逻辑的语言中，产生 了动态认知逻辑( d e l ；d y n a m i ce p i s t e m i cl o g i c ) 。动态认知逻辑能够描述第一方面， 即在有关的信息事件发生后主体的认知状态如何改变。公开宣告逻辑( p a l ；p u b i c a n n o u n c e m e n tl o g i c ) 是d e l 的一种特殊情况，它描述了宣告真的信息之后主体认知 状态的动态性，能够处理公开宣告这一行动对主体知识和推理的影响。1 9 8 9 年，在j a n a p l a z a 提交给i s m i s 会议的一篇论文( l o g i c so f p u b l i ca n n o u n c e m e n t ) 中建立了第 一个公开宣告逻辑系统。1 9 9 7 年，jg e r b r a n d y , w g r o e n e v e l d 1 9 9 7 1 3 l 重新独立发现了 公开宣告逻辑系统。在p a l 中，公开宣告一个真语句( p 是通过认知模型的相对化来刻 画，即相对于( p 为真的那些认知状态集合。另一个方面，眦，假定了只有真的语句才 能被公开宣告。但是它没有给出一种表示交流限制的种类的方式。 为了能形式化处理主体认知状态的时态性，人们引入了由事件序列组成的分支一 时间树结构，产生了认知时态逻辑( e t l ；e p i s t e m i ct e m p o r a ll o g i c ) 。在e 爿莫型中， 给定节点发出的每个枝分别表示在那个时间点( 表示为节点) 之后能够发生哪些事件 序列。因此，e t l 能够直接刻画在不同情景中的相关的交流限制。然而，与给定e t l 模型无关的那些事件的认知结果，e t l 并没有予以说明。在任意e t l 模型中，事件的 认知结果必定要通过在主体之间的不可区分关系上加上特定的性质而说明。因此， e t l 不能提供一种系统化的方法末表示信息事件和它们的认知结果。r o b _ i tp a r i k h ， r r a m a n u j a m 2 0 0 3 中给出了e t l 的模型。 显然，在描述多主体相互作用的过程中，p a l 和e t l 各有其优点和不足。为了既 能够刻画在某些事件发生之后的认知结果，又能刻画对能够发生的事件的限制，就需 。ja p l a z a l o g i c so fp u b l i cc o m 】m u n i c a t i o n s mle m r i c h ，msp f e i f e r , mh a d z i k a d i c ，zw r a s ( e d s ) p r o c e e d i n g s o f t h e 4 t h i n t e r n a t i o n a l s y m p o s i u mo n m e t h o d o l o g i e s f o r i n t e l l i g e n t s y s t e m s 1 9 8 9 ，p 2 0 1 2 1 6 。r p a r i k h ，r r a m a n u j a m ak n o w l e d g eb a s e ds e m a n t i c so fm e s s a g e s j o u r n a lo f l o g i c ，l a n g u a g e , a n d i n f o r m a t i o n ，2 0 0 3 ，1 3 4 5 3 - 4 6 7 1 两南人学硕十学位论文文献综述 要融合d e l 和p a l 。j o h a nv a nb e n t h e m ，j e l l eg e r b r a n d y ，e r i cp a c u i t 2 0 0 7 也融合d e l 和e t l ，提出了时态动态认知逻辑系统t d e l ，并且也提到融合p a l 和e t l ，得到时态 公开宣告逻辑系统t p a l ，它能够较好刻画以上提到的多主体智能相互作用的两方面 的内容。论文中也介绍了d e l 和e t l 二者之间有怎样的关系，二者之间相互转化的一 个定理。 在建立了逻辑系统t d e l 之后，出现了一些新的研究方向。一方面，t o m o h i r o h o s h i 2 0 0 8 基- 于t d e l ，进一步系统研究时态公开宣告逻辑t p a l ，并且进一步扩展 了一个普遍的公开宣告算子，得到时态任意公开宣告逻辑系统t a p a l 。t a p a i 包 括了一些能对公开宣告进行量化的算子，例如，“在任意公开宣告发生之后，q 为真”、 “在任意公开宣告序列发生之后，( p 为真 等。 另一方面，t o m o h i r oh o s h i ，a u d r e y y a p 2 0 0 8 在时态动态认知逻辑t d e l 的基础 上添加了一个时态算子p ，得到系统t p a l + p ，这里添加的时态算子是带有标签的过去 算子和将来算子。尽管在时态框架上添加一个过去算子看来很简单，但是在表达力上 的增强具有很重要的应用意义。a u d r e y y a p 2 0 0 6 在d e l 中加入了一个类似的时态算 子，讨论了b m s 乘积更新模型中的时态信息，即将时态算子与乘积更新结合起来，这 样可以表达一些过去的信息，例如能够刻画“在你做c 之前，我不知道( p 为真，但我现 在知道( p 是假的”这样的语句。j o s h u as a c k 2 0 0 8 将动态认知逻辑与时态逻辑结合起 来，将时态算子添加到动态认知逻辑中，形式化地处理了动态认知逻辑中遇到的时态 问题。 时态公开宣告逻辑是融合公开宣告逻辑和认知时态逻辑而形成的一个逻辑系统。 作为一个较新的研究领域，目前，国内对其研究还很不够，相对而言，国外对它们的 研究比较活跃。本文是在大量参考国外专家、学者对有关公开宣告逻辑、认知时态 逻辑以及时态公开宣告逻辑等问题的文献后完成的，重在系统介绍时态公开宣告 逻辑这一系统。 j v a nb e n t h e m , j g e r b r a n d y , e p a c i t m e r g i n gf r a m e w o r k sf o ri n t e r a c t i o n ：d e la n de t l nt a r k , 2 0 0 7 锄t h o s h i p u b l i ca n n o u n c e m e n tl o g i c sw i t hp r o t o c o lc o n s t r a i n t s s t a n f o r du n i v e r s i t y 2 0 0 8 固参考pb a l b i a n i ，a b a l t a g ，h v a i ld i t m a r s c h ，a h e r z i g ，th o s h i ，t d el i m a w h a tc a l lw ea c h i e v eb ya r b i t r a r y a n n o u n c e m e n t s ? ad y n a m i ct a k ei nf i t c h sk n o w a b i l i t y p r o c e e d i n g so f t h e o r e t i c a la s p e c t so f r a t i o n a l i t ya n d k n o w l e d g e ，2 0 0 7 口p 表示在任意宣告v 发生之后，q 为真，其中口就是普遍公开宣告算子。 逻辑系统t a p a l 融合了系统t p a l 和任意公开宣告逻辑a p a l 。 th o s h i ，a y a p ，d y n a m i ce p i s t e m i cl o g i ca n d t e m p o r a lo p e r a t o r s s t a n f o r du n i v e r s i t y , 2 0 0 8 a y a p p r o d u c tu p d a t ea n dl o o k i n gb a c k w a r d m s s t a n f o r du n i v e r s i t y ，2 0 0 5 j s a c k a d d i n gt e m p o r a l 口毋ct od y n a m i ce p i s t e m i cl o g i c p h dt h e s i s ，i n d i a n au n i v e r s i t y , 2 0 0 7 2 两南大学硕+ 学位论文 第1 章公开宦告逻辑p a l 和认知时态逻辑e t l 第1 章公开宣告逻辑p a l 和认知时态逻辑e t l 本章首先讨论公开宣告逻辑p a l ，该系统是动态认知逻辑系统d e l 的种特 殊情况，它能够刻画在公开宣告这种行为发生之后主体知识的变化。接着讨论认 知时态逻辑系统e t l ，它能够刻画在不同情景中的相关的交流限制。这里只给出这 两个系统的部分说明，要了解更详细的内容和更多的技术方法，可以参考j a na p l a z a 1 9 8 9 和p a r i k h ，r a m a n u j a m 2 0 0 3 。 1 1 公开宣告逻辑p a l 公开宣告逻辑系统p a l 能够刻画在公开宣告某一事实之后主体知识的变化。 要表达和处理由公开宣告这一行动引起的知识变化，我们需要一个动态认知的形 式语言，公开宣告对于动作的处理是通过行动模态词来实现的。因此，公开宣告 逻辑从最基本的公开宣告这一认知行动入手，通过刻画动作对知识的影响来完成 对动作的处理。当然，p a l 逻辑的形式语言是原来静态认知逻辑语言的一个扩充。 定义1 1 ( 语言z 队l ) 给定一个非空的原子命题集p 和有限的主体集n ，公 开宣告逻辑系统p a j l 语言中的语句归纳定义如下： 【p ，v ：= pi - 1 叩l ( p 人vk i ( p | ! q v ，其中p p ，i n 。 显然，认知逻辑系统语言z e l 是队l 的一个片段，即z p a l 中去掉 ! q q v 而得 到。 k j 中和 ! ( p v 的直观意思分别是“主体i 相信中”和“在公开宣告( p 之后，v 成立 。 k i 和 ! 叫的对偶算子是 和 ， ( p = 1 k i _ 1 ( p 和 v = “! ( p 卜v 的直观意思分 别是“主体i 认为q 是可能的 和“并非如果宣告( p 成功则v 为假 ( 即成功宣告q 并且v 成立) 。 定义1 2 ( 认知模型) 给定一个非空的原子命题集p 和有限的主体集n ，认 知模型定义为斯= ( w ，( r i ) i e n , v ) ，其中： 1 w 0 ，w 是一个有限非空的可能世界集； 2 r ic _ w x w ，r i 对每个主体指派w 上的一个二元关系； 3 v ：p 一2 w ，v 对每个原子命题在每个可能世界上进行赋值。 定义1 3 ( 语义) 给定一个认知模型斯和一个可能世界w e w ，公式( p 在认知 模型q c t 中是真的，记作( 吖，w ) = 伞，归纳定义如下： 1 吖，w = p当且仅当w e v ( p ) ； ja p l a z a l o g i c so fp u b l i cc o m m u n i c a t i o n s mle r n r i c h ，msp f e i f e r , mh a d z i k a d i c ，zw r a s ( e d s ) m c 阳出，够 o f t h e 4 t h i n t e r n a t i o n a l s y m p o s i u m o n m e t h o d o l o g i e s f o r i n t e l l i g e n t s y s t e m s 1 9 8 9 p 2 0 1 2 1 6 r p a r i k h ，r r a m a n u j a m ak n o w l e d g eb a s e ds e m a n t i c so fm e s s a g e s j o u r n a lo f l o c , l a n g u a g e , a n d i n f o r m a t i o n ，2 0 0 3 ，p 4 5 3 4 6 7 3 两南大学硕十学何论文第1 章公开宵告逻辑p a l 和认知时态逻辑e t l 2 吖，w 1 q 当且仅当吖，wbq ； 3 m ，w ( p 八v 当且仅当m ，w ( p 且吖，w v ； 4 吖，w k j q 当且仅当对任意v w ，若w r v 则吖，v 平 5 硝，w ! 中 v当且仅当若斯，w q ，则硝j q ，w v ； 其中，m i 币= ( w i ( p ，( r i l 币) j n ，v l p ) 定义为： w l q = vi v = 叩) r i l 中 = r i l 3 w l 币w l q v i p ( p ) 2 v ( p ) n w k 6 硝，w v 当且仅当吖，w ( p 并且m i 母，w v 。 定义1 4 ( 证明系统) p a l 的证明系统是在认知逻辑的基础上扩充了关于p a l 算子 ! ( p 的必然化规则和一些归约公理而得到的： 一、公理： 1 、认知逻辑系统中所有的公理； 2 、 ! ( p ph ( ( p p ) ： 3 、【! ( p 】 vh ( ( p _ 1 ! ( p 】v ) ； 4 、 ! ( p ( v ) c ) h ( ! ( p 】v 八 ! ( p 】z ) ； 5 、 ! ( p k i vh ( 叩 k i ! ( p 】v ) 。 二、推理规则： 1 、从 ( p ，( p j v ) ，可以得到v ；( 分离规则) 2 、若卜v ，贝, u i - k i q o ； ( 必然化规则) 3 、若卜v ，则卜 ! ( p v 。( ! ( p 必然化规则) 很容易验证这些公理都是有效式，并且推理规则具有保真性。特别值得注意的 是，通过归约公理可以将z 队l 中的每一个公式都归约为等值于z e l 中的公式。因 此，p a l 公理系统是可靠的和完全的。 1 2 认知时态逻辑e t l 认知时态逻辑系统e t l 能够描述在一些信息化的过程中知识在时间进程上如 何发展。纯粹的认知语言是认知时态语言的一个片段，以前的可能世界只是一个 点，而这里的可能世界的内部有结构。 这里先介绍一些基本概念。假设主体集n 和事件集。 历史( h i s t o r y ) 是由事件集中的事件组成的有穷序列，其中宰是由所有历史 组成的集合。 给定任意h 宰和任意e ，则h e 表示在历史h 后紧接着事件e 。给定任意 h 幸和任意h 木，h h 表示h 是h 的一个有限的前段。h 兰。h 表示对于事件e ， 4 两南人学硕十学何论文 第1 章公开宣告逻辑p a l 和认知时态逻辑e t l h 7 - - - h e 。九表示空序列。 协议( p r o t o c 0 1 ) 就是历史集h 宰且相对非空的有限前段封闭。 定义1 5 ( z e t l 语言) 给定一个非空的原子命题集a t 、有限的主体集n 和事 件集，认知时态逻辑系统e t l 语言中的语句归纳定义如下： q ，v ：2pi ( pq a t l sk i ( pi e ( p l ，其中p a t ，i n ，e e 。 e t l 语言是在z e l 语言的基础上扩充算子 e 而得到的， e 】( p 的直观意思是“事 件e 发生后( p 成立。 定义1 6 ( e t l 框架) 令是事件集。e t l 框架就是三元组( ，h ， i i e n ) ，其 中h 是一个协议，对任意ie n ， i 是h 上的一个二元关系( i ：n 一矽( h h ) ) 。 e t l 框架描述了在一些信息进程中知识与时间是如何联系的。协议刻画了时 态结构，h e 表示e 在h 中发生之后的那个时间点。关系i 表示主体对当前历史的 不确定性，因此，l h h 意思是在主体i 看来历史h 与历史h 相同。 定义1 7 ( e t l 模型) e t l 模型是一个四元组( ，h ， i i n ，v ) ，其中( ，h ， i ) i e n ) 是e t l 框架，v 是一个赋值函数( v ：a t p ( h ) ) 。 定义1 8 ( 语义) 令= ( ，h ， i ) i n ，v ) 是一个e t l 模型。公式( p 在一个历 史h h 上是真的，记作见h 9 ，归纳定义如下： 1 、万，h p当且仅当h v ( p ) 2 、，h 1 伞 当且仪当 玎，h 每q 3 、万，h = q 八v 当且仅当万，h ：中且见h = v 4 、玎，h k i ( p 当且仅当 对任意h h ，若h i h 则，h q 5 、万，h e 】( p 当且仅当对任意e ，若h e h 则吖，h e ( p 在认知时态语言中同样能添加普遍知识( 如分布性知识或者公共知识) 和时 态算子( 过去算子或将来算子) ，只是这种扩张将增加逻辑有效性的复杂性。 对这些模型进行更多的限制能反映出主体的一些特征，如完美记忆、共时性、 没有奇迹。我们可以通过将认知和行为的可通达关系作为直接的结构条件或者通 过认知时态公理来刻画这样的限制，其中这两种观点都与模态框架对应相关。 命题1 9 公理k e ( p 一 e 】k ( p 对应性质完美记忆：若h e k ，则存在历史h 7 使得 k = h e 且h h 。 这说明了个体现在的不确定性只来自之前的不确定性，表达了完美记忆的一 个很强形式。 命题1 - 1 0 共时性：不确定性l l k 只发生在h 和k 的相同等级上。 这预先假定了对当前事件e 的完美观察：在d e l 中，这是假的，因为当主体 不能区分事件厂和事件e 时，不确定性也能形成于当前的观察。 p b l a c k b u r n ，m d er i j k e ，y v e n e m a m o d a l l o 垂c c a m b r i d g eu n i v e r s i t y , 2 0 0 1 ，p 1 2 3 1 3 7 5 两南人硕十学伊论文第1 章公开宵告逻辑p a l 和认知时态逻辑e t l 命题1 1 1 公理 e k 印专k e ( p 对应于性质没有奇迹：对任意k e 且h k 都有h p k e 。 这表达的意思是虽然学习可以取代观察事件，但不存在奇迹：当前的不确定 性只能通过对不同事件的不同观察来解决。 6 两南大学硕十学何论文第2 章p a l 生成e t l 一模型 第2 章p a l 生成e t l - 模型 前面提到纯粹的认知语言是认知时态语言的一个片段，认知逻辑中的可能世 界只是一个点，而认知时态逻辑中的可能世界内部是有结构的。p a j l 的形式语言 是静态认知逻辑语言的一个扩充。因此，本章将p a l 与e t l 联系起来，首先给出 r 址一协议，进而介绍如何由p a l 一协议生成e t l - 模型。 2 1p a l 生成e t l - 模型 为了后面的工作，首先把给定认知模型中的每个点都指派给公开宣告序列集。 我们称那些公开宣告序列的集合为协议。 定义2 1 ( p a l 协议) 令e p a l 是公开宣告! ( p 的集合，其中中z p 札。p a j l 协议 p 就是e p a l 中有限公开宣告序列的集合，并且它相对有限前段封闭。我们用p t c l 表示p a l 协议类。 定义2 2 ( s d p a l 协议) 令斯是任意的认知模型，研上的一个s d 协议厂是 一个从d o m ( 九) 到p t c l 的函数。我们用p a l 表示s d 协议类。如果s d p a l 协议厂 是常函数( 即对任意w d o m ( m ) 都有f ( w ) = p ) ，则称，是统一的p a l 协议( u n i f o r m p a l p r o t o c 0 1 ) 。 统一的p a l 协议将唯一的p a l 协议p 指派给认知模型中的每个点，当然，统 一的协议就成为主体间的公共知识。但是，s d 一协议不被任何主体所知道。因此， s d 协议和统一的协议是两种极端的情况。在本文中，我们就只讨论s d 协议和统一 的协议。 给定认知模型吖和吖上的一个统一的协议或者s d 协议厂，我们要根据吖来 构造e t l - 模型。那么，生成e t l - 模型的基本步骤：( 1 ) 检查由协议指派给每个点 上允许执行的公开宣告；( 2 ) 如果允许执行的公开宣告刚好在那个点上为真，那么 就产生一个新的点；( 3 ) 在新的点继承原来的不可区分关系。 先来看个由认知模型吖和吖上的一个统一的协议构造e t l 模型的例子。 例子2 1 如下认知模型吖中有四个点( s 、t 、u 和v ) 和两个主体( a 和b ) ， p 在点s 、u 和v 上均为真，q 在点s 、t 和u 上均为真，r 在点t 、u 和v 上均为真： s d - 协议就是s t a t e d e p e n d e n tp r o t o c o l 。 d o m ( 购足指吖的论域。 7 o 协 口 f ， 两南大学硕十学传论文第2 章p a l 乍成e t l 一模型 该例子中的协议是个统一的协议，因此，把协议p 指派给模型斯中的所有点。 由于! p 在模型斯中允许执行并且p 在点s 、u 和v 上均为真，就可以生成三个节点 s ! p 、u ! p 和v ! p ；由于p 在点t 上为假，就不能生成节点t ! p 。同时，在s ! p 与u ! q 之间和u ! p 与v ! p 之间仍然要分别继承s 与u 之间和u 与v 之间的关系。在第二级 上，! q 和! r 允许执行且q 在点s 和u 上为真，r 在点u 和v 上为真，就可以继续生 成节点s ! p i q 、u ! p i q 、u ! p ! r 和v ! p ! r ，同样要继承之前的关系。 在上述例子中生成的e t l 模型满足一个强的统一性条件：根据协议p ，如果! ( p 是可宣告的，那么对任意历史h ，! ( p 在h 上能被执行当且仅当( p 在h 上是真的。这 就蕴含了协议p 是公共知识。当然，在由s d 一协议生成的e t l 模型中不满足这个 条件。 例子2 2 认知模型吖是由三个不可区分的点w 、v 和u 构成。p 在点w 和点v 上为真，q 只在点w 上为真。令，是斯上的一个s d 协议，且使得( w ) = ! p ! i p ， 八v ) = ! p p ，g p ，一口 切! f p ，! - - , q 切，1 1 9 ! t ) 图2 2 下图： 佛! p 指派给了模型硝中的所有点。由于p 在点w 和点v 上都为真，就可以生成 两个节点w ! p 和v ! p ；由于p 在点u 上为假，就不能生成节点“u ! p ”。同时在w ! p o 其中横线表示不可区分关系，带箭头的线表示在每个历史卜可得到的宣告。 。实际上二，这还蕴含j ，更强的事实，即如果! p 能被执行，那么只要p 为真，在当前模型中任何地方都能被执行。 注意：这罩的【i 】q 就是前面介绍的脚。 固本图来源于t h o s h i p u b l i ca n n o u n c e m e n tl o g i c sw i t hp r o t o c o lc o n s t r a i n t s s t a n f o r du n i v e r s i t y ，2 0 0 8 ，p 6 。 8 两南大学硕+ 学何论文第2 章p a l 生成e t l 一模型 和v ! p 之间要继承w 和v 之间的不可区分关系。生成的节点就构成了将! p 运用于 斯而得到的模型硝if p o 在第二级上，! i p 是被允许执行的并且在w ! p 和v ! p 上都 为真。因此，生成了第三级的节点w ! p ! i p 和v ! p ! i p 。同理，因为! - 1 q 在点v 和 点u 被允许执行并且 q 在这两个点上都为真，就生成了节点v1 1 q 和u ! 一q ；而不 能生成节点“w ! q ”，因为1 1 q 在点w 不能被允许执行且、q 在这个点为假。接着， 生成节点u ! - 1 q ! t 而不能生成节点“v ! _ 1 q ! t ”，因为! t 在点v ! 一1 q 不被允许执行。 然而，以上描述只给出了部分结果。注意在上面例子中，s d 协议，中并没有包 括含有公开宣告算子的公式。一旦我们碰到在协议中出现这种公式，就不能像上 面例子中直接简单地从最低端的认知模型开始生成e t l 模型。为了说明这个问题， 就必须假设协议厂允许在点w 宣告公式 t 。实际上要确定这个公式是否能 被宣告，我们需要知道这个公式在点w 是否为真。然而，为了确定这个公式在点 w 是否为真，我们需要知道a 在点w 是否为真并且厂是否允许在点w 发生! a 。当 然还需要知道b 在w ! a 上是否为真并且厂是否允许在点w ! a 发生! b 。否则，我们 就不能确定 t 的可宣告性。 这个例子说明了如下几点。首先，如果( p 包含宣告算子，因此相对包含在! ( p 中 的“低阶 公开宣告使得! ( p 是一个“高阶”的公开宣告，那么我们必须知道低级 宣告的可宣告性以便确定! ( p 的可宣告性。第二，在一些公开宣告序列之后，! ( p 可能 代表低阶的公开宣告。在这些情况中，我们需要知道相关公开宣告序列的可宣告 性以便确定! ( p 的可宣告性。 因此，我们需要将上述例子中的构造扩展到高阶的宣告。最重要的就是要对 宣告序列中出现的宣告的等级进行结构归纳来构造e t l 结构。给定认知模型吖和 协议厂，如果由厂给定的序列中的第一部分只由认知公式组成，首先根据上面的构 造方法从射构造e t l - 树。也就是，我们通过处理一阶宣告开始构造。然后将节点 添加到之前所得到的结构，基于涉及一阶宣告的二阶宣告。第二个构造过程就能 实现，因为要进行二阶宣告，我们就需要知道公式的真值，即那些一阶宣告使得 在一阶构造过程之后二阶宣告在这个点被确定。然后，我们继续这种方式在一阶 宣告的节点之后构造二阶宣告的节点，直到所有的一阶宣告和二阶宣告都被处理。 同理继续进入三阶宣告过程，等等。 定义2 3( 公式的等级) 公开宣告公式! ( p z p a l 的等级o ( ! q ) 归纳定义如下： 1 、o ( ! p ) = l ( p a t ) ： 2 、o ( ! 一( p ) = o ( ! ( p ) ； 3 、o ( ! ( ( p 八v ) ) = m a x ( o ( ! ( p ) ，o ( ! v ) ) ； 4 、o ( ! k i 甲) = o ( ! 中) ； 5 、o ( ! v ) = m a x ( o ( 1 9 ) + l ，o ( ! v ) ) 。 9 两南大学硕十学伊论文 第2 苹p a l 生成e t l 模璎 例如，o ( ! ! p 川= 2 ，0 ( ! ! q ! t 川= 3 等。公开宣告的等级是指嵌套 的“! 算子的最大值。给定序列o = ( p l ( p 2 e p a l ，定义o ( g ) = ( o ( ! 叩1 ) ，o ( ! ( p 。) ) 。 o 表示序列等级的集合。 定义2 4 我们以如下方式在等级的集合o 上定义排序，对p a j l 中任意两组序 列6 = o l 和t = 下l t n ，o ( 6 ) o ( t ) 满足： 1 、o t ： 2 、3 i e n v j n ( j i 专o ( q ) = o ( 勺) 且o ( a i ) o ( x i ) o 定义2 5 ( 模型的并) 令f = w k k n 是e t l 模型h k = ( h k ，、，v k ) 的一个族。 f 中的e t l - 模型的并uk n ， 是一个三元组( h ，v ) ： 1 、h = uk nh k 2 、一= u k n - - 一k 3 、对任意p a t ，v ( p ) = uk e n v k ( p ) 。 给定序列o ，我们用g ( 1 ( ) ( 0 k m ) 表示。中从第一个开始的长度为k 的前段， 用o k ( 1 - - - - - k m ) 表示a 中的第k 个元素。例如，o = ( p 1 ( p 2 ( p 3 ( p 4 ，则d ( 3 ) = ( p 仰2 ( p 3 ，o 3 = q ) 3 。 定义2 6 ( g 生成模型) 令斯= ( w ，( r i ) i n ，v ) 是一认知模型且，是吖上的一个 s d 协议。对于任意序列a 文l 和任意等级x o ，以下我们归纳定义6 一生成模型 卯，= ( 、矿，( 西) i n ，旷，) 和等级x 片段模型硝f = ( w f ，r i 乏vf ) ： 1 、m 0j = 北硝= 北 2 、硝k = u m 一io ( t ) o ( t ) ； 3 、w d ( n + 1 ) ，= 厂，( 。m + 1 ) ) u w 6 ( n + 1 ) i9 盯：( 。( n + 1 ) ) ，w f f ( n ) f i n + l 且6 ( n + 1 ) 八w ) ) ； 4 、( w ，c ，) r i 咐0 , 1 当且仅当( w r i 且t = r ； 5 、v o ( n + 1 ) 7 ( p ) = w t 、仃( n + 1 ) ，1w e v ( p ) 。 定义2 7 ( p a l 生成e t l - 模型) 由认知模型9 v f = ( w ，( r i ) i n ，v ) 和s d 一协议，生 成的一个e t l 模型f o r e s t ( m ，力定义为： f o r e s t ( 9 , ，g 力：= w u wa u e 贝w ) 夕旷，= ( h ， i i n ，v ) 1 、h = f hi 存在w w ，