（计算机软件与理论专业论文）概率时态知识逻辑的符号模型检测研究.pdf

概率时态知识逻辑的符号模型检测研究 专业：计算机软件与理论 硕士生：宿云 指导教师：苏开乐教授 摘要 模型检测作为一种自动验证有限状态系统是否满足规范的形式化技术，在规 划和多智能体系统等人工智能领域得到了越来越多的应用。现在已经开发出多个 多智能体系统的模型检测工具，如m c t k 等。人工智能领域常遇到对具有概率 特性的不确定信息进行表示、推理和验证的问题。智能体常常以一定概率相信某 命题成立。虽然现今有较成熟的概率系统模型检测工具，如p r i s m 等，但是它 们不能表示智能体的知识，并不适合于多智能体系统。如今，在多智能体系统的 研究中，缺乏对智能体在不确定环境下对具有概率特性的信息的形式化描述和模 型检测方法。 本文重点研究具有概率特性的多智能体系统的规范表示及其模型检测方法。 提出概率认知解释系统，并在这一新的模型基础上研究多智能体系统的概率时态 知识逻辑的语义及符号模型检测算法。提出的概率时态知识逻辑p e c t l k 。是在 分支时态逻辑的存在片断e c t l 语言中加入表示智能体知识的s 5 。知识算子和表 示智能体认为事件发生概率的概率算子后得到的。该逻辑有丰富的概率、时态和 认知表达能力，用户可以方便地检测智能体的非确定性推理过程。因此，本文研 究成果在概率方面扩展并丰富了当前的多智能体系统的模型检测技术。 多智能体系统模型检测技术的研究不仅有重要的理论意义，还有重大的实际 应用价值，它特别适用于信息系统可靠性和安全性的形式化验证。今后我们将在 本文工作的基础上，进一步实现概率时态知识逻辑模型检测工具，并针对安全协 议验证这一课题提出和实现新的多智能体系统模型及相关模型检测算法。 关键词：多智能体系统，符号模型检测，概率时态知识逻辑，非确定性推理 r e s e a r c ho ns y m b o l i cm o d e lc h e c k i n g t e m p o r a ll o g i c so f k n o w l e d g ea n dp r o b a b i l i t y m a j o r ： c o m p u t e rs o f t w a r ea n dt h e o r y n a m e ：s uy u n s u p e r v i s o r ：p r o f e s s o rs uk a i l e a b s t r a c t a sak i n do fa u t o m a t e dv e r i f i c a t i o nt e c h n i q u e so ff i n i t es t a t e s y s t e m ，m o d e l c h e c k i n gh a sb e e nl e dt oar e c e n tg r o w t ho fi n t e r e s ti na p p l i c a t i o n so ft h et e c h n i q u e s t ot h ef i e l d so fa r t i f i c i a li n t e l l i g e n c e ，s u c ha sp l a n n i n ga n d m u l t i a g e n ts y s t e m s t h e r e a r es o m em o d e lc h e c k e r sh a v eb e e nd e v e l o p e df o rm u l t i a g e n t s y s t e m ss u c ha s m c t k i nt h ea r e ao fa r t i f i c i a li n t e l l i g e n c er e p r e s e n t i n g ，r e a s o n i n ga n dv e r i f i c a t i o n a b o u tu n c e r t a i n t yi n f o r m a t i o ni su n a v o i d a b l e u s u a l l yt h ea g e n t sb e li e v es o m e t h i n gi s l i k e l yt r u ea n dg i v ei tap r o b a b i l i t y al t h o u g ht h e r ea r es o m em o d e lc h e c k e r sh a sb e e n d e v e l o p e ds u c c e s s f u l l yf o rp r o b a b i l i s t i cs y s t e m ，s u c ha sp r i s m ，t h e yc a nn o te x p r e s s t h ek n o w l e d g eo fa g e n ta n da r en o ts u i t e dt om u l t i - a g e n ts y s t e m s u n t i ln o wt h e m e t h o do fr e p r e s e n t i n gf o r m a l i z e da n dm o d e lc h e c k i n gt h ep r o b a b i l i s t i ci n f o r m a t i o n u n d e ru n c e r t a i n t yc o n d i t i o ni ss t i l ll a c k t h ea i mo ft h i st h e s i si st od os o m er e s e a r c ho nt h er e p r e s e n t a t i o no fm u l t i a g e n t s y s t e m sf e a t u r e dp r o b a b i l i t ya n dt h em o d e lc h e c k i n gm e t h o d st ot h ev e r i f i c a t i o no f m u l t i a g e n ts y s t e m s w ep r o p o s eap r o b a b i l i t ye p i s t e m i ci n t e r p r e t a t i o ns y s t e m ，a n d b a s e do nt h i sm o d e lg i v et h es e m a n t i c so ft e m p o r a l l o g i co fk n o w l e d g ea n d p r o b a b i l i t y , a sw e l la sd e v e l o ps o m em o d e lc h e c k i n ga l g o r i t h m sf o rv e r i f i c a t i o nt h i s m o d e l t or e a s o na b o u tu n c e r t a i n t yo f m u l t i a g e n ts y s t e m s ，w ei n t r o d u c ep e c t l k n ，a t e m p o r a ll o g i cf o rk n o w l e d g ea n dp r o b a b il i t yt h a ti st h ef u s i o no ft h et w ou n d e r l y i n g l a n g u a g e s ：a ne x i s t e n t i a lf r a g m e n to fc t la n ds 5 nf o rt h ek n o w l e d g eo p e r a t o r s t h i s l o g i ci so f g r e a te x p r e s s i v ep o w e ri nb o t hk n o w l e d g ea n dp r o b a b i l i t y i ti sc o n v e n i e n t f o ru s e r st o s p e c i f ya g e n t s m e n t a ls t a t e sa n dt h ep r o b a b i l i t ye v o l u t i o no ft h e s e t h e r e f o r e ，t h er e s e a r c ha c h i e v e m e n t so ft h i st h e s i se x t e n da n de n r i c hs t a t eo ft h ea r t m o d e lc h e c k i n gt e c h n i q u e sf o rm u l t i - a g e n t s y s t e m si np r o b a b i l i s t i cd i m e n s i o n v i i i a b s t r a c t t h es i g n i f i c a n c eo fm o d e l c h e c k i n gt e c h n i q u e sf o rm u l t i - a g e n ts y s t e m si sn o to n l y o nt h et h e o r yr e s e a r c h ，b u ta l s oo nt h ep r a c t i c a la p p l i c a t i o n s i ti sv e r ys u i t a b l et ot h e f o r m a lv e r i f i c a t i o no fr e l i a b i l i t ya n ds e c u r i t yo fi n f o r m a t i o n a ls y s t e m s b a s e do no u r p r e s e n tw o r k ，w ew i l lf u r t h e rd e v e l o pt h es y m b o l i cm o d e lc h e c k e rf o rt e m p o r a ll o g i c o fk n o w l e d g ea n dp r o b a b i l i t y , a n dd e s i g nr e l a t e dm o d e lc h e c k i n ga l g o r i t h m sf o r s e c u r i t yp r o t o c o lv e r i f i c a t i o n k e y w o r d s ：m u l t i a g e n ts y s t e m s ，s y m b o l i cm o d e lc h e c k i n g ，t e m p o r a ll o g i co f k n o w l e d g ea n dp r o b a b i l i t y , r e a s o n i n ga b o u tu n c e r t a i n t y 论文原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指 导下，独立进行研究工作所取得的成果。除文中已经注明引 用的内容外，本论文不包含任何其他个人或集体已经发表或 撰写过的作品成果。对本文的研究作出重要贡献的个人和集 体，均已在文中以明确方式标明。本人完全意识到本声明的 法律结果由本人承担。 学位论文作者签名：1 镭云 e l 期：7 阳 p 8 年r 月0 日 学位论文使用授权声明 本人完全了解中山大学有关保留、使用学位论文的规 定，即：学校有权保留学位论文并向国家主管部门或其指定 机构送交论文的电子版和纸质版，有权将学位论文用于非赢 利目的的少量复制并允许论文进入学校图书馆、院系资料室 被查阅，有权将学位论文的内容编入有关数据库进行检索， 可以采用复印、缩印或其他方法保存学位论文。 学位论文作者签名：丽云 导师签名： 孩弓 日期：游r 月，d 日日期：劢娼年r 月1 0 日 第一章绪论 计算机软硬件系统日益复杂，功能日益强大，计算机几乎已在各个领域中得 到普遍应用。随着计算机软件在国民经济、国防等关键领域的广泛应用，由软件 故障造成的损失可能会是灾难性的。因此，如何验证其正确性和可靠性以保证软 硬件系统质量成为日益紧迫的问题。 验证方法主要有模拟，测试，定理证明和模型检测等。模拟和测试是在一组 方案下测试系统行为是否与预期的一致。这两种方法只能显示错误的存在，而不 能证明系统没有错误，是正确的。定理证明是通过演绎推理证明软件的正确性， 但推理过程往往需要人工参与以使推理向正确的方向进行。这是一个耗时的过 程，并且只能由具用丰富逻辑推理经验的专家完成，因此大多数证明系统不能完 全自动化。在计算机领域我们尤其感兴趣的是可完全自动化的形式验证技术，模 型检测就是其中最引人注目的一个。 模型检测的研究开始于2 0 世纪8 0 年代初，当时c l a r k e 、e m e r s o n 和q u e i l l e 等 人提出了用于描述系统性质的分支时态逻辑c t l ( c o m p u t a t i o nt r e el o g i c ) ，设计 了检测有限状态系统是否满足给定公式的算法，并实现了一个原型系统e m c t l l 。 这一工作为对系统的性质自动进行验证开辟了一条新的途径，成为近二十多年来 计算机科学基础研究的一个热点。模型检测的基本思想是用状态转移系统表示系 统的行为，用模态和时态逻辑公式描述系统的性质。这样，“系统是否具有所期 望的性质”就转化为数学问题“状态转移系统是否是公式的一个模型”。对有限 状态系统而言，这个问题是可判定的。模型检测器解决这一问题的方法是基于对 系统状态空间的穷举搜索。与其他方法相比，模型检测能够自动进行验证，而且 能够在系统不满足公式的情形下给出反例。正是这两点使模型检测在诸多形式化 方法中引人注目。随着这种技术的发展，人们在不断探索如何扩展模型检测适用 的范围。 概率在软硬件的设计和分析中被广泛使用，它可以作为不可靠或不可预知的 系统的模型，如随机分布算法，通信网络中的内在不确定性只有使用概率才能进 行精确建模。因此将概率引入模型检测技术是其中的一个热点。描述不确定系统 的概率模型是通过在状态间的转移关系上标记表示该转移出现的可能性的概率 而获得的。常用的模型是马尔可夫链( m a r k o vc h a i n ) 。描述系统性质的逻辑通 2 概率时态知识逻辑的符弓模型检测研究 常是在c t t _ , 或c t l ( 集成c t l 和线性时态逻辑l t l 的有丰富表达能力的时态逻 辑) 上增加概率算子p 形成新的逻辑p c t l 或p c t l 。概率系统模型检测器可以计 算概率系统在执行中特定事件出现的概率。 多智能体系统的模型检测是另一个近年来的研究热点。当智能体应用于与安 全攸关的领域时，验证其是否满足设计要求就显得尤为重要了。传统的时态逻辑 模型检测在应用中的成功让研究者们深受启发，他们也试图将模型检测技术运用 到多智能体系统的验证中去，希望借助它来实现知识逻辑描述的系统性质的自动 验证嵋j 。与此同时，由于在逻辑模型，卜的杳n 似性，时态逻辑和知识逻辑也逐渐呈 现相互融合的趋势，这最终导致了时态知识逻辑的产生，如h a l p e m 和v a r d i 提出 的结合线性时态逻辑l t l ( l i n e a r t i m et e m p o r a ll o g i c ) 和知识逻辑的带n 个智能 体的知识与公共知识时态逻辑c k l 。1 3 】。时态知识逻辑的出现极大地促进了知谚 推 理的研究，由于其强大的表达能力，时态知识逻辑能用于描述各种多智能体系统 中的时态知识性质【4 】。为了能对这些性质进行自动验证，学者们的焦点开始集中 于研究时态知识逻辑模型检测的理论和工具，并在近十年间得到了高速发展，很 多高效的时态知识逻辑模型检测方法不断地涌现出米【5 刁】，相应的模型检测工具 也不断地被开发出来o l 。 概率系统的模型检测可以描述系统的概率特性，但不能表达智能体的知识。 多智能体系统的模型检测可以表达智能体的知识，但目前还不能在不确定环境下 对信息进行表示和验证。f a g i n 和h a l p e m 在2 0 世纪9 0 年代给出了一种可以对具有 概率特征的知识进行推理的概率知识逻辑，并证明了可靠性，完备性等性质，但 是没有涉及概率知识逻辑的模型检测问趔1 。至今概率知识逻辑的模型检测技术 尚未见文献报道，针对这一现状，本文的工作就是要向这个方向迈出第一步。本 论文的主要目标就是解决对具有概率特性的多智能体系统的模型检测问题。 论文大纲 本文结构如下：第二章从文献角度介绍概率系统和多智能体系统模型检测技 术的相关研究工作：第三章介绍关于模型检测，概率计算和知识推理等的一些预 备知识；第四章和第五章是该篇论文的主要贡献。介绍一个概率时态知识逻辑 p e c t l k 。，及这种逻辑在多智能体系统的概率认知解释系统下的语义和基于 m t b d d 的符号模型检测算法。最后，我们在第六章总结本文的研究成果并展望 未来的工作。 第二章概率系统和多智能体系统模型检测的 相关研究工作 在这一章我们从文献资料简单回顾与本论文主题概率时态知识逻辑模型 检测紧密相关的一些工作的研究进展。首先，在2 1 节回顾符号模型检测技术， 及m t b d d 。m t b d d 是b d d 的扩展，可以用于概率系统下的符号模型检测。 下来在2 2 和2 3 节我们将关注于概率系统和多智能体系统模型检测技术的发展 及相应的工具。 2 1 符号模型检测和m t b d d 的相关研究工作 模型检测( m o d e lc h e c k i n g ) 是一种被广泛应用的验证有限状态系统是否满 足某种性质的形式化方法。这种技术分别由c l a r k e ，e m e r s o n 1 2 和q u e i l l e ， s i f a k i s 1 3 】等人独立提出。模型检测器通过对状态迁移图的分析，在状态空问上 穷尽搜索来完成检验工作。当要验证的性质不被满足时，模型检测器会产生一个 反例，即系统的一次使规范不成立的执行。 要验证的规范一般用时态逻辑描述，根据将时间看作是线性的还是分支结构 的，时态逻辑分为线性时态逻辑l t l 和分支时态逻辑c t l 。时态逻辑是由哲学家 p r i o r 在2 0 世纪6 0 年代首次提出的，他提出的逻辑类似于l t l 。b u r s t a l l 【l 引， k 艘e r z l 5 1 和p n u e l i 1 6 1 等许多人都曾提出使用时态逻辑对计算机程序进行推理。 p n u e l i 首次使用时态逻辑对并行系统进行推理。他的方法包括在给定条件下从公 理集证明程序的属性，那些公理描述了程序中各个状态的行为，但证明过程是手 工完成的，这种技术很难在实践中使用。c t l 逻辑是在2 0 世纪8 0 年代由c l a r k e 和 e m e r s o n 设计的。 在2 0 世纪8 0 年代初，c l a r k e 和e m e r s o n 1 2 , 1 7 1 j 丕首次提出了时态逻辑模型检 测算法，该算法使得推理过程可以自动完成。在一个模型巾验证一个公式是否成 立比在所有模型中验证一个公式的有效性要容易许多，所以高效实现验证一个公 式的可满足性是可能的。由c l a r k e 和e m e r s o n 开发的分支时态逻辑c t l 的模型 检测算法的复杂度是模型的大小和公式长度的多项式时问。许多同步程序的正确 性是依赖于某种公平性假设的，他们还给出了在不改变算法复杂度的前提下对公 平性的处理。 4概牢时态知识逻辑的符弓模型检测研究 几乎同时q u i e l l e 和s i f a k i s 1 3 也开发山了c t l 子集上的模型检测算法，但是 没有分析算法的时间复杂度。之后，c l a r k e ，e m e r s o n 和s i s t l a 设计了一个改进 的算法，这个算法的复杂度是公式长度和模型大小乘积的线性时间【1 引。s i s t l a 和 c l a r k e 分析了对于各种时态逻辑的模型检测问题，指出对- 丁线性时态逻辑l t l ， 模型检测问题是p s p a c e 完全的【旧2 0 1 。p n u e l i 和l i c h t e n s t e i n 分析了l t l 公式检 测的复杂度是公式长度的指数级，模型大小的线性级【2 。基于这个发现人们认为 在l t l 公式较短时，模型检测算法还是可以接受的。在同一年，f u j i t a 实现了一 个对l t l 公式的t a b l e a u 验证系纠2 2 1 。一些研究者还提出了使用自动机进行验证 的模型检测技术1 2 3 , 2 4 1 。 这些模型检测算法中，模型的转移关系是用邻接表来实现的。当这些算泫应 用到实际的一些例子时，人们发现要列出模型的所有状态是不可能的。最根本的 原因就是所谓的状态爆炸问题：当系统的大小线性增长时，描述系统的模型的状 态数会呈指数级增长。即使是一个很小的实际系统，状态数都有可能达到上百万 个。解决这一问题的一个最成功的方泫就是符号模型检测：使用二叉判定图b d d ( b i n a r yd e c i s i o nd i a g r a m s ) 作为表示状态集和状态转移关系的数据结构，从而降 低系统模型所需的内存空间。 b d d 是表示布尔函数的有向无环图。山l e e t 2 s l 和a k e r s l 2 6 最先提出。后来 b r y a n t 细化了这种数据结构，提出一组高效的操作算法【2 7 1 。1 9 8 7 年，m c m i l l a n t 2 s , 2 9 1 观察到以邻接表形式存储的状态转移关系可以符号化以b d d 形式表示，提出了 以高效的b d d 操作来实现c t l 的模型检测技术。b d d 为布尔函数提供了一个 标准形式，并且b d d 表示的布尔函数要比用合取或析取范式表示的布尔函数更 紧凑，这是因为符号化表示利用了模型状态空间的某种规则性。在文献 2 8 1 中指 出 1 8 】中的c t l 模型检测算法的符号化形式可以表示和验证1 0 2 0 个状态，自那以 后，研究者们提出了许多基于b d d 技术的模型检测算法，并且可验证的状态数 进一步推广到1 0 1 2 0 个状态 3 0 , 3 1 】。m c m i l l a n 等人实现这些技术并开发了著名的符 号模型检测器s m v ( s y m b o l i cm o d e lv e r i f i e r ) t ”1 。符号模型检测技术的出现使模 型检测向实际应用性迈出了关键的一步。现在成熟的模型检测器有s m vp 引， n u s m vm e ws m v ) 乃j ，s p i n t m l 等 表2 - 1 模型检测工具 建模语言逻辑语言b d d 包开发单位 s m v k r i p k e 结构 c t lo b d d 卡耐基梅隆人学 n u s m v k r i p k e 结构 c t l & l t lc u d d 卡耐基梅隆大学 s p i np r o m e l al t l b e l l 实验室 第二章概率系统和多智能体系统模型检测的相关研究工作 s m v 是一种检测有限状态系统是否满足c t l 公式的符号模型检测器，由 m c m i l l a n 开发。s m v 从用s m v 输入语言编写的程序中抽取o b d d ( o r d e r e d b i n a r yd e c i s i o nd i a g r a m ) 表示状态迁移关系，采用基于b d d 的搜索算法，用计 算不动点的方法检测状态的可达性和所满足的性质。s m v 采用卡耐基梅隆大学 的o b d d 软件包。 n u s m v 是由s m v 重新工程化并扩展实现的符号模型检测器。n u s m v 被设 计为一个开放的模型检测体系架构，可作为定制验证工具的核心和形式化验证的 试验床，并用于工业设计的验证。n u s m v 采用科罗拉多大学的c u d d 软件包设 计基于b d d 的模型检测部分，可验证c t l 和l t l 两种时态逻辑公式。 s p i n 用以检测有限状态系统是否满足l t l 公式及其它一些性质，如可达性 和循环等。其输入语言p r o m e l a 在语法上与c 接近，其程序山进程、通道和变量 构成。其模型检测的基本方法是以b u c h i 自动机表示进程和l t l 公式的非，计算 这些自动机的积，通过判别其可接受的语言是否为空的方法检测系统模型是否满 足给定的性质。 b d d 是布尔函数的图形表示，若当前函数是从布尔值到实数，则可将b d d 扩展为多终端二叉判定图m t b d d ( m u l t i t e r m i n a lb i n a r yd e c i s i o nd i a g r a m s ) 来 表示该函数。c l a r k e 等人首次在 3 5 1 中提出这个概念，但作者只给出了取值为1 或一l 的矩阵的m t b d d 表示及操作的实现方法。在文献 3 6 】中，作者提出取值可 在任意有限集合上的矩阵的m t b d d 表示，并与相应的稀疏矩阵的大小作比较， 得出结论：从存储空间大小的角度m t b d d 要优于稀疏矩阵。在这篇文献中同时 还给出了利用m t b d d 的递归性实现矩阵操作的算法，并分析这些算法的最坏复 杂度。指出尽管它们的最坏甚至平均复杂度是指数级，但在实际应用中被证明是 可以很好地完成的。文献【3 7 】给出了一个高效的m t b d d 表示的矩阵的乘法算法 及线性方程组的基于m t b d d 的求解方法。概率系统的符号模型检测一般是基于 m t b d d 实现的。 2 2 概率系统模型检测的相关研究工作 传统的模型检测是在定性模型上对系统性质进行定性验证，即系统性质成立 的概率为0 或1 。到2 0 世纪8 0 年代，人们对模型检测提出了纯概率模型离 散时间马尔可夫链d t m c ( d e s c r e t et i m em a r k o vc h a i n ) 1 3 8 刮j ，之后c o u r o u b e t i c s 和y a n n a k a k i s 给出了在d t m c 上做定量系统性质验证的方法，计算一个属性被 满足的概率1 4 0 ，4 1 1 。h a n s s o n 和j o n s s o n 提出了概率算子p 及一种概率时态逻辑： p c t l ( p r o b a b i l i s t i cc o m p u t a t i o nt r e el o g i c ) ，在这种逻辑下，允许使用如p p 伊 6 概率时态知识逻辑的符号模型检测研究 这样的公式表示事件缈出现的概率大于p 【4 2 1 。a z i z 等人在【4 3 】中介绍了如何用在 【4 0 ，4 l 】中的方法对概率时态逻辑p c t l 描述的公式进行验证。 概率系统的模型是在传统模型检测的状念转移关系上引入概率，表示转移出 现的可能性。该转移关系可用实值矩阵表示，概率就可利用基于矩阵的数字计算 ( 如线性方程组的求解，矩阵与向量的乘积等) 得到。由非概率系统符号模型检 测的成功实现，自然，将b d d 扩展为m t b d d 作为数据结构，隐式的表达转移 关系，实现概率系统符号模型检测是可能的。h a c h t e l 等人在 4 4 ，4 5 】中应用 m t b d d 验证了可以计算含有1 0 2 7 个状态的d t m c 模型中稳定状态的概牢。b a i e r 等人在 4 6 】中给出一种基于m t b d d ，在d t m c 上对p c t l 逻辑公式进行验证的 符号化算法。h a r t o n a sg a r m h a u s e n 在 4 7 1 q b 提出 4 6 】中p c t l 逻辑模型检测算法 的实现，并利用它对火车信号系统进行了验证。这表明了基- y - m t b d d 实现的对 d t m c 模型的p c t l 的符号模型检测可成功应用于实际系统的验证。除d t m c 外，k w i a t k o w s k a 和a l f a r o 等人还提出了基于m t b d d ，在马尔可夫决策过程 m d p ( m a r k o vd e c i s i o np r o c e s s e s ) 上对p c t l 公式验证的符号模型检测技 术【4 8 4 9 1 。文献【5 0 】中给出一个完整的基于m t b d d 的连续时间马尔可夫链c t m c ( c o n t i n u o u s t i m em a r k o vc h a i n s ) ，连续随机逻辑c s l ( c o n t i n u o u ss t o c h a s t i cl o g i c ) 的符号模型检测技术。当前已开发出的概率系统模型检测器有t p w b ( t i m ea n d p r o b a b i l i t yw o r k b e n c h ) 5 1 】，e l m c 2 ( e r l a n g e n - t w e n t em a r k o vc h a i nc h e c k e 0 旧， 和p r i s mf p r o b a b i l i s t i cs y m b o l i cm o d e lc h e c k e r ) s a l 等。 表2 - 2 概率系统模型检测工具 建模语言逻辑语言 t p w b 进程代数t p c c s t p c t l e 1 m c 2 c t m c s & d t m c sc s l & p c t l p r i s md t m cm d p & c t m cp c t l & c s l t p w b 是一种允许用进程代数t p c c s 描述概率与离散时间系统的，对 t p c t l 逻辑公式进行验证的检测器。 e 1 m c 2 提供在c t m c 模型上对c s l 逻辑公式及在d t m c 模型上对p c l t l 逻辑公式进行检测的非符号检测器。 p r i s m 是由英国伯明翰火学开发的，提供在c t m c 模型上对c s l 逻辑公式 及在d t m c 和m d p 模型上对p c t l 逻辑公式进行检测的符号检测器。p r i s m 第二章概率系统和多智能体系统模犁检测的棚关研究工作 采用科罗拉多大学的c u d d 软件包设计基于m t b d d 的模型检测部分。 2 3 多智能体系统模型检测的相关研究工作 知识模态逻辑从2 0 世纪8 0 年代中期开始逐步应用到分布式系统的形式规范， 用于精确地描述一个智能体的知识1 5 4 1 ，随后，在时态逻辑中加入知识模态算子的 时态知识逻辑也被广泛地应用于分布式系统的知识推理中。随着模型检测技术的 发展，知识也成为模型检测的一个领域。h a i p e r n 不1 3 v a r d i 首先在1 9 9 1 年提出一个 用模型检测方法进行知识推理的推演，但他们的知识逻辑没有时态算子【5 5 1 。r o n v a nd e rm e y d e n 在文献 5 6 d f l 研究了关于某一类系统( 实质上是无穷状态系统) 知识和时问的模型检测问题的复杂性，并指出该问题复杂度在最好情况下是 p s p a c e 完全的，而在最坏情况下是不可判定的。此后各种时态知识逻辑的模型 检测方法和工具相继出现。 v a nd e rh o e k f f i w o o l d r i d g e 在2 0 0 2 年提出- - 种方法将时态知识逻辑c k l 。1 3j 模 型检测问题转化为线性时态逻辑l t l 模型检测问题【5 j 。但是并没有直接实现c k l 。 模型检测的方法和工具。另夕b v a nd e rh o c k 和w o o l d r i d g e 还在文献【5 】中提出用交 替时间时态逻辑a t l 及其关于知识的扩展版本a t e l 进行多智能体系统验证的方 法。a t l 可以表示多个智能体联合起来达成某一性质；然而，不易于用a t l 处理 不完全信息或智能体的局部观察，因为不完全信息的a t l 模型检测问题是不可判 定的【5 7 1 。 v a nd e rm e y d e n 和s u 首次在2 0 0 4 年研究了包含知识公式的匿名性质的符号模 型检测方法【5 3 】。然而，他们假设智能体拥有完美记忆，并且只考虑- - d , 类没有嵌 套知识模态词的公式。 在2 0 0 4 年，v a nd e rm e y d e n 和g a m m i e 开发了一个时态知识逻辑的符号模型检 测器m c k 8 1 。给定多智能体系统的描述和智能体对系统的不同的观察，m c k 支 持几种不同的知识定义：基于观察的，基于观察和时钟的，和对所有观察拥有完 美记忆的知识。m c k 同时支持线性的和分支的时态算子。当前m c k 采用d a v i d l o n g 的o b d d 软件包实现符号模型检测算法。 同样是在2 0 0 4 年，r a i m o n d i 和l o m u s c i o 在文献 5 9 中也提出一个基于c t l 的 时态知识逻辑c t l k 的符号模型检测方法，并实现一个基于c u d d 的符号模型检 测器m c m a s ( m o d e lc h e c k i n go fm u l t i - a g e n ts y s t e m ) 。与m c k 不同的是， m c m a s 不仅考虑时态和通常意义的知识算子，还考虑其他与知识相关的算子， 并且他们的语义不假设拥有完美记忆。然而，他们的输入语言并不便于用户使用， 8概率时态知识逻辑的符号模犁检测研究 因为系统中每一变量的任一取值必须在输入语言中枚举出来。另外，r a i m o n d i 和l o m u s c i o 还祉文献 6 0 】中提出一种根据解释系统模型将多智能体系统规范语 言翻译成s m v 程序的一种编译方法，并将s m v 模型检测器和克里普克( k r i p k e ) 模型编辑器a k k a 结合起来，从而允许自动验证多智能体系统的认知性质。 2 0 0 5 年，k a i l es u 等人提出了一个基于c t l 的时态知识逻辑c t l k 的符号模 型检测方法，并实现了一个基于c u d d 的符号模型检测器m c t k 6 1 , 6 2 】。m c t k l i i m c k 和m c m a s 具有更丰富的表达能力及更快的验证速度。并且可以对一类基于 信息论的安全协议进行建模与验证。 多智能体系统可能是不可靠的，如通信系统。上面这些模型检测器只可以实 现对智能体的确定推理过程的验证。我们还需要验证智能体的非确定推理过程。 h a l p e r n 在 6 7 】中专门研究了智能体的非确定推理，包括非确定性的表示，非确定 性推理的描述逻辑及模型等。f a g i n 和h a l p e r n 在文献【l l 】给出了一种概率知识逻 辑，扩充了知识逻辑语言，使得在其中可以对具有概率特征的知识进行推理。还 在克里普克结构的基础上引入了概率测度，给出该逻辑系统的语义，并证明了可 靠性，完备性等性质。但是没有涉及概率知识逻辑的模型检测问题。本论文将着 手这方面的研究，这将在第四、五章中详细讨论。 第三章预备知识弟二早耿亩大u 识 在本章中我们将介绍一些与本论文主题相关的预备知识。在第一节中介绍模 型检测的思想，检测过程，标记算法，常用来描述系统的模型克里普克结构和描 述规范的语言时态逻辑。第二节我们介绍知识推理语言的语法，语义，知识的性 质及多智能体系统等。最后我们将回顾概率论的一些知识。 3 1 模型检测 模型检测是一种对有限状态系统进行形式化验证的技术。与验证的传统方法 如模拟、测试和演绎推理等相比有许多优势。这种方法已成功地应用于复杂的电 路设计和通信协议等的验证实践中。模型检测的主要挑战是状态空间爆炸问题， 在模型检测技术发展的二十多年中，为解决这个问题取得了很大的进展，提出了 很多方法，如：符号化技术，抽象，对称，归纳等。在这一节，我们将简要介绍 模型检测技术的主要思想，检测过程，介绍描述系统的模型克里普克结构，及描 述规范的时态逻辑。本节主要根据文献 6 3 ，6 4 来介绍有关模型检测方面的理论。 3 1 1 模型检测的思想和过程 模型检测的基本思想是用某种恰当的数学模型m 表示将要验证的系统s ， 用某种恰当的形式化语言将要验证的系统属性p 表示为公式，系统是否具有所 期望的属性就转换为数学问题m 是否是的模型，由谓词“i _ ”表示为m | - 矽定 义模型m 满足公式。通常，数学模型m 采用状态转移图或称为克里普克结构， 形式化语言采用时态逻辑。模型检测问题就是找到所有满足的状态集合 扣s l m ，s f = ) ，如果初始状态集瓯是该集合的子集，则说系统满足属性。对 于有穷状态系统，这个问题是可判定的，即可以用计算机程序在有限时间内自动 确定。模型检测的过程包括以下三步： 建模：这是模型检测的第一步，用某种模型检测工具所能接受的形式化语言 1 0 概率时态知识逻辑的符号模犁检测研究 将设计转化为模型，通常这仅仅是一个编译过程。有时，因为时间和内存的限制， 一个设计的建模过程会用到抽象( a b s t r a c t i o n ) 技术米去除无关的或不重要的细 节。 规范：在验证之前，确定设计要满足的属性是必要的。通常，使用某种逻辑 公式表达规范。对于软、硬件系统，常常使用时态逻辑，它能够描述系统的行为 是如何随时间而变化的。规范的一个重要问题就是完备性( c o m p l e t e n e s s ) 。模型 检测为验证一个设计的模型是否满足一个给定的规范提供了方法，但是确定是否 一个给定的规范包括了系统应该满足的所以属性是不可能的。 验证：将设计的模型和要验证的用时态逻辑描述的规范输入某种模型检测器 进行验证。理想的验证过程是完全自动化的，但是实际中对验证结果的分析还是 需要设计者的协助。验证结果有两种情况，一种是“y e s ”，表示模型满足规范。 另一种是“n o ”，同时输出一条不满足规范的路径，这条路径可以帮助设计者分 析错误并找到错误的位置，设计者修改系统并重新验证。错误也可能是南系统的 不正确建模或不正确的规范引起的，错误轨迹也可以用来识别和修正这两种问 题。验证的任务也有可能因为模型规模太大无法装入内存而非正常终止。这时， 需要调整模型检测器的某些参数或调整模型( 如使用抽象技术) 后重新验证。 下面我们将分别来介绍表示系统的模型克里普克结构，常用的描述规范的语 言时态逻辑和模型检测过程。 3 1 2 克里普克结构 设a p 是原子命题集合。定义在a p 上的克里普克结构m 是一个四元组 ( s ，孓，r ，) ，其中， s 是有穷状态集合 s o s 是初始状态集合 尺s x s 是状态间的转移关系 三：s 专2 舻是标记函数，( s ) 定义在状态s 成立的原子命题集 转移关系尺通常要求是完全( t o t a l ) 的，即对任意状态s s ，存在j s ，有 ( s ，s 3 r ，当s 无后继时，增加关系r ( s ，s ) 。在结构m ，从状态s 出发的一条路 径是一个无穷状态序列，万= s o s l s 2 ，s = s o ，并且对于任意f 0 ，有( ，s + 1 ) r 。 设v = ，) 是系统变量集。假设v 中的变量值在有限集合d ( d o m a i n ) 第三章预备知识 上变化。v 的一个赋值是从v 到d 上的函数。系统的一个状态s 就是系统中所 有变量的赋值，即s ：v d ( s es ) ，可以用一个恰好在这个状态的赋值下为真的 公式表示。例如给定v = v l ，v 2 ，v 3 ) ，状态s = ( 2 ，3 ，5 ) ，即s ( v 0 = 2 ，s ( v g = 3 ，s ( v 3 ) = 5 ， 可用一阶公式v l _ 2 a v 2 = 3a v 3 = 5 表示s 。通常一个公式会在多个赋值下为真，那 么一个一阶公式也可以表示一个特定的状态集合。设一阶公式编表示系统的初 始状态集。 一阶公式不仅可以表示状态集合，而且还可以表示转移的集合。转移是状态 间的一个有序对，设有序对中前一个状态用矿中变量的赋值表示，后一个状态用 v 中的变量赋值表示，v = v lv y ) ，v 中每一个变量v 对应v 中的1 ，。转移 就可看作是变量集合v 和y 上的赋值，凶此，可以用一个一阶公式表示转移或 转移的集合。r 是转移关系，那么我们用彳( y ，v ) 表示与关系r 对应的公式。 原子命题集a p 中的命题通常具有v = d 的形式，v v ，d d 。如果s ( 1 ，) = d 那么命题 ，= d 在状态s 中为t r u e 。当v 是布尔变量时，一般用v 来表示s ( ，) = t r u e ， 用一v 表示s ( v ) = f a l s e 。 由此，一阶公式编和贸( y ，y ) 描述的克里普克结