（计算机软件与理论专业论文）模型检测时态知识逻辑及其应用.pdf

模型检测时态知识逻辑及其应用 专业：计算机软件与理论 硕士生：何青 导师：苏开乐教授 摘要 在人工智能和理论计算机科学领域，多智能体系统中的知识表示和知 识推理最近十年来逐渐受到重视。研究者们使用知识逻辑来描述智能体的 知识特性，并且希望借助形式化方法来验证多智能系统中的知识逻辑规范。 模型检测作为一种成熟的形式化验证技术得到了学者们的关注，因为它能 很好地对大规模的系统进行自动验证。然而，传统的模型检测是基于时态逻 辑的，它并不支持知识逻辑规范的验证。于是有关专家们将时态逻辑和知识 逻辑融合为时态知识逻辑并创建了各种模型检测时态知识逻辑的方法和 工具。 本文首先介绍了模型检测和知识推理的基本概念，然后着重介绍了我 导师所提出的模型检测时态知识逻辑的方法，最后使用本实验室研制的相 关工具m c t k 来对两个特定领域的问题进行了自动验证：一方面的问题是 验证对弈中的必胜策略，即验证对弈中的行棋双方是否存在着必然获胜的 走法；另一方面的问题是验证基于知识的安全协议，而这类协议的安全特性 依赖于协议参与者的知识推理。 本文不仅详细地介绍了模型检测刊态知识逻辑的相关理论知识，而且 通过对实验结果的分析与比较检验了本文所使用方法及工具的正确性。更 重要的是，通过对实际问题的研究与探讨，本文展现了模型检测时态知识逻 辑理论的广阔应用前景。 关键词：模型检测，知识推理，模型检测时态知识逻辑，对弈的必胜策略 基于知识的安全协议 m o d e lc h e c k i n gt e m p o r a ll o g i co f k n o w l e d g ea n di t sa p p l i c a t i o n s 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 ：h eq i n g s u p e r v i s o r ：p r o f ，k a i l es u a b s t r a c t 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 ea n dt h e o r e t i c a lc o m p u t e rs c i e n c e ， r e s e a r c h e r sh a v ep a i di n c r e m e n t a la t t e n t i o n st ot h ek n o w l e d g er e a s o n i n go f m u h i - a g e n ts y s t e m sd u r i n gt h en e a rt e ny e a r st h e yi n t e n d e dt ou s el o g i co f k n o w l e d g et of o r m a l i z et h ek n o w l e d g ep r o p e r t i e so fa g e n t s ，a n dt h e nv e r i f y k n o w l e d g es p e c i f i c a t i o n so fm u l t i a g e n ts y s t e m sw i t hf o r m a lm e t h o d s m o d e l c h e c k i n ga saf u l l yd e v e l o p e dt e c h n o f o g yc a u g h tr e s e a r c h e r s e y e ，d u et oi t s e x c e l l e n tp e r f o r m a n c eo fv e r i f y i n gl a r g e - s c a l es y s t e m sh o w e v e r ，t h i st e m p o - r a ll o g i cb a s e dt e c h n o l o g yw a sn o tc o n v e n i e n t l ya p p l i e dt ot h ev e r i f i c a t i o no f k n o w l e d g el o g i cs p e c i f i c a t i o n t h u s ，s o m ee x p e r t sc o m b i n e dt h e s et w ol o g i c s i n t ot h et e m p o r a ll o g i co fk n o w l e d g e m l dt h e nd e v e l o p e dv a r i o n sm e t h o d s a n dt o o l sf o rm o d e lc h e c k i n gi t i nt h i st h e s i s ，w e v ef i r s ti n t r o d u c e ds o m ec o n c e p t i o n so fm o d e lc h e c k i n g a n dk n o w l e d g er e a s o n i n g t h e nw e v em a i n l yi n t r o d u c e dm yt u t o r sm e t h o d o fm o d e lc h e c k i n gt e m p o r a ll o g i co fk n o w l e d g e l a s t l y , w e v ea p p l i e dt h i s m e t h o dt ot w os p e c i f i ca r e a sw i t ho n rt o o lm c t k ：o n ep r o b l e mi st ov e r i f y t h ew i n n i n gs t r a t e g i e si nt h ez e r o - s u mg a m e s ，w h i c hi st oa u t o m a t i c a l l yf i n d o u tw h e t h e rt h e r ee x i s t saw a ye n s u r i n gt h en e c e s s a r i l yw i no fp l a y e r s ；t h e o t h e rp r o b l e mi st ov e r i f yt h ek n o w l e d g eb a s e ds e c u r i t yp r o t o c o l s ，w h o s e s e c u r ep r o p e r t i e sr e l yo nt h ek n o w l e d g er e a s o n i n go ft h ea n t i c i p a n t si nt h e p r o t o c 0 1 模型检测时态知识逻辑及其应川 w e v en o to n l yd e l i b e r a t e l yi n t r o d u c e dt h et h e o r e t i cb a s i so fm o d e lc h e c k i n g t e m p o r a ll o g i co fk n o w l e d g e ，b u ta l s oi n s p e c t e dt h ec o r r e c t n e s so ft h em e t h o da n d r o dt h a tw e v eu s e dt h r o u g ht h ea n a l y s i sa n dc o m p a r i s o n so ft h ee x p e r i m e n t a l r e s u l t s a d d i t i o n a l l y , b yd i s c u s s i n gt h ep r a c t i c a li s s u e ，w e v ep r e s e n t e dab r o a d p e r s p e c t i v e so ft h ea p p l i c a t i o n so ft h i st h e o r d k e yw o r d s ：m o d e lc h e c k i n g ，k n o w l e d g er e a s o n i n g ，m o d e lc h e c k i n gt e r n p o r a ll o g i co fk n o w l e d g e ，w i n n i n gs t r a t e g y - i ng a m e s ，k n o w l e d g eb a s e ds e c u r i t y p r o t o c o l 第1 章绪论 人类对知识本质的探索从未停止过，从古希腊时期以来，历代哲学家们都 试图回答关于知识的疑问，诸如“我们知道什么? ”，“什么能被知道? ”等等。 然而，直到上世纪五十年代初，对知识进行形式化分析的思路才首先由y o n w r i g h t 【1 提出。此后在1 9 6 2 年，h i n t i k k a 在他的著作知识与信仰f 2 1 中首次 以书面形式介绍了知识逻辑。随后，大批学者开始投入到对知识的形式化研究 中，各种有关知识的公理系统不断地被建立起来。 与此同时，在人工智能和理论计算机科学领域，人们对知识推理的研究兴 趣逐渐浓厚起来。科学家们试图借助知识逻辑模型来分析智能群体中的交互行 为，f a g i n 和h a l p e n 等在1 9 9 5 年出版的知识推理3 1 一书无疑为该方向的研 究注入了一针强心剂，使得相关的研究工作如雨后春笋般开展起来。该书中建 立的多智能体解释系统框架，更是成为了知识推理研究的基术假设，此后很多 重要的理论和方法都是在该框架下建构起来的。 然而，同是属于模态逻辑4 1 的知识逻辑和时态逻辑，它们却经历了不同的 发展道路。由于模型检测技术【5 的发展，时态逻辑更多的被运用于系统规范的 描述和验证中，而且随着上个世纪九十年代初符号化模型检测技术f 6 1 的出现， 它已被广泛地应用到大规模集成电路和大型软件系统的验证中7 1 。 模型检测时态逻辑在应用中的成功让研究者们深受启发，他们也试图将模 型检测技术运用到多智能体系统的验证中去，希望借助它来实现知识逻辑规范 的自动验证8 1 。与此同时，由于在逻辑模型上的相似性，时态逻辑和知识逻辑 也逐渐呈现相互融合的趋势，这最终导致了时态知识逻辑的产生，如h a l p e r n 和v a r d i 提出的结合线性时态逻辑和知识逻辑的c k l 。逻辑 9 】。 时态知识逻辑的出现极大地促进了知识推理的研究，由于其强大的表达能 力，时态知识逻辑能用于描述各种多智能系统中的时态知识规范3 1 。为了能对 这些规范进行自动验证，学者们的焦点开始集中于研究模型检测时态知识逻辑 的理论和工具。这方面的工作首先由h a l p e r n 和v a i d i 1 0 开展起来，并在近十 年间得到了高速发展，特别是进入二十一世纪后，很多先进的模型检测时态知 2模型检测时态知识逻辑及其应用 识逻辑的方法不断地涌现出来1 1 1 | 1 2 1 3 1 ，相应的模型检测工具也不断地被开 发出来1 4 1 5 1 1 6 卜 模型检测时态知识逻辑的理论在被提出之后，它们很快便被应用于实际问 题的研究中【17 】【1 8 1 9 口相比于传统的模型检测技术，它涉及的范围更加广泛， 适用于包括经济学、社会学、心理学、统计学、计算机科学等众多的社会科学和 自然科学领域及其交叉领域的相关问题研究。然而，由于相关的理论和工具的 提出时问还很短，它们还需要经受实践的检验，因此其应用价值还未能充分展 现。这就需要我们在其基础上进行大量的实验和分析工作，一方面用于证实相 关理论和工具的正确性，另一方而也能不断地发掘出新的应用领域。 本文的研究正是基于这样的研究背景而开展的，并且是在相关理论和工具 的支持下完成的。我们希望通过该文达到以下目标： 全面系统地介绍模型检测时态知识逻辑的理论。主要包括介绍模型检测技 术；时态逻辑、知识逻辑及时态知识逻辑：多智能体系统中的知识表示和 知识推理：模型检测时态知识逻辑的方法及工具。 初步探索模型检测时态知识逻辑的理论在实际问题中的应用价值。希望通 过博弈和安全协议方面的实例验证来展现该理沧在相关领域的应用潜力， 并以此来揭示其应用上的不足之处。 通过实验结果的分析与比较，对我导师提出的模型检测时态知识逻辑的方 法以及本实验室开发的相应工具进行检验。 本文结构大致如下：第2 章介绍基于时态逻辑的模型检测技术，同时介绍 b d d s 技术及与之相关的符号化模型检测技术；第3 章首先介绍知识逻辑模型， 进而介绍多智能体的解释系统框架及其框架下的知识语义：第4 章介绍时态知 识逻辑c k 厶。及其模型检测方法( 重点介绍我导师提出的方法) 与本实验室开 发的验证工具m c t k ；第5 章使用m c t k 来验证对弈中的必胜策略：首先介 绍一般性的验证方法，然后针对井字棋进行了实验和分析：第6 章使用m c t k 来验证基于知识的安全协议，分别验证了保密家就餐协议和俄罗斯牌协议，并 与其它工具的实验结果进行了比较；第7 章对全文的工作进行总结，同时对该 领域今后的研究方向进行展望。 第2 章模型检测技术 模型检测( m o d e lc h e c k i n g ) 是一种被广泛应用的验证有限状态系统满足规 范的形式化方法【5 】【2 0 】。在这里，规范( s p e c i f i c a t i o n ) 被形式化描述为时态逻 辑公式【2 1 】，如工具s p i n 2 2 使用的l t l ( 线性时态逻辑) ，s m v 2 3 】中使用 的c t l ( 分支时态逻辑) 。这些验证技术被称为时态逻辑模型检测，是由c l a r k e 和e m e r s o n ，以及q u i e l l e 和s i f a k i s 在2 0 世纪8 0 年代最先发展的。在这种方法 中，规范被描述为命题时态逻辑公式，系统( 如电路设计，协议等) 被模型化为 状态转换系统，然后使用高效的搜索算法来判定规范是否在系统中成立 2 4 】。 一般来说，有两种基本的模型检测方法。一种是构造出系统的所有可达状 态。这种方法面临着状态爆炸问题f 2 5 1 ，特别当系统转换关系很复杂时。另一 种更好的方法是符号化方法 6 】，该方法使得系统的规模得以大幅度提高，这 得益于有序二值判定图( o r d e r e db i n a r yd e c i s i o nd i a g r a m s ，o b d d s ) 【2 6 】的使 用，o b d d s 是一种用来表示布尔函数的数据结构。 在这一章里，我们将就以上内容进行详细说明。 2 1 时态逻辑 时态逻辑( t e m p o r a ll o g i c ) 是一种包含时间概念的逻辑，其公式能够表述关 于过去、现在和将来状态的客观事实。直观上看，时态逻辑是在命题逻辑的基 础上加入了时态算子。时态逻辑的种类有很多，我们这里主要是考虑计算树逻 辑c t l + 2 7 】，分支时态逻辑c t l 【2 8 】和线性时态逻辑l t l 2 9 】。文献 3 0 对 它们进行了比较，而 3 1 】中则分析了它们的复杂性。 2 1 1 k r i p k e 结构 在有限状态并发系统中，一个k r i p k e 结构【3 2 m 就是一个三元组 ，其中： s 是系统中所有状态的集合； 4 模型榆测时态知识逻辑及其应川 r sxs 是状态迁移关系，且对所有状态8 s ，存在一个状态s 7 s 使得( s ，s 7 ) r ； l 是一个函数s 一2 “f 对于每个状态，用该状态下为真的原子命题的集 合标记该状态，a p 是原子命题的集合1 。 m 中的一条路径是一个无限状态序列，该状态序列7 r = 8 0 ，s 。满足 对所有i 0 ，有( s i ，s i + 1 ) er 。 2 1 2 计算树逻辑c t l * 从概念上来说，c t l * 公式描述的是计算树的性质。计算树的形成如下：首 先指定k r i p k e 结构中的一个状态作为初始状态，然后将k r i p k e 结构展开成一 棵以初始状态为根的无限树。因此计算树描述了从初始状态开始的所有可能的 执行路径。 c t l * 公式由路径量词和时态算子组成。路径量词有两种：a ( 对所有路 径) ，e ( 对某些路径) ；基本时态算子有5 种：x ( 下一时刻) 、f ( 将来某时刻) 、g ( 总是) 、u ( 直到) 和r ( 释放) 。 2 1 2 1c t l 4 语法 c t l * 有两类公式：状态公式和路径公式。在某个特定状态为真的公式是 状态公式。沿着某个特定路径为真的公式是路径公式。f 列三个规则给出状态 公式的语法： l 如果p a p ，那么p 是状态公式 2 如果，和g 是状态公式，那么，、f v g 和，a g 是状态公式 3 如果，是路径公式，那么a f 和e f 是状态公式。 下列两个规则给h 了路径公式的语法 1 如果，是状态公式，那么，也是路径公式 第2 章模型检测技术 2 如果，和g 是路径公式，那么、，、f v g 、f a g 、x f 、f f 、g ，、f u g 、f a 9 是路径公式。 c t l * 是由上面规则产生的状态公式的集台。 2 1 2 2c t l + 的语义 我们用丌 表示从8 。开始的”的后缀。如果，是状态公式，那么m ，s f 意味着，在状态8 下为真。如果，是路径公式，那么m ，7 r ，意味着，沿着路 径7 为真。关系 递归定义如下： 1 m ，s p 甘p l ( s ) ； 2 m ，8 一 铮m ，s 睁f 1 ： 3 m ，s v ，2 营m ，8 ，1 o r m ，s ，2 ； 4 m ，s f la ，2 兮m ：s f l a n d m ，s 厶： 5 m ，s e g l 铮存在一条从s 出发的路径”，使得m ，7 r g l ： 6 m ，8 a 9 1 铮对于每条从s 出发的路径7 r ，都有吖，7 r g l ； 7 m ，口 ，1 营对于”的每一个状态s ，都有m ，s ，1 ； 8 m ，7 r 、9 1 铮m ，7 r 睁g l ； 9 m ，7 r g lv9 2 甘m ， 9 1 o r m ， 口2 ： l o m ，丌 9 l 9 2 m ，玎 9 l a n d m ，丌 啦； 1 1 m ，7 r x g l 甘m ，7 1 9 1 ； 1 2 m ，7 r f g l 兮存在k20 ，使得m ，7 r g l ； 1 3 m ，7 r g g i 静对于所有k20 ，都有m ，7 r 9 1 ； 1 4 m ， g l u 9 2 营存在k 0 ，使得m ，一 9 2 ，且对于所有的o j ， 都有m ，丌j g l ； 6模型检测时态知识逻辑及其应用 1 5 m ，” g l r 9 2 甘对于所有j 0 ，如果对于每个i j ，都有m ，丌t g l 那么有m ，一 9 2 。 这里我们假设 和，2 是状态公式，而9 。和9 2 是路径公式。 2 1 3 分支时态逻辑c t l 分支时态逻辑c t l 是c t l * 的一个约束子集，在c t l 逻辑中，时态算子 x 、f 、 g 、u 和r 之前必须立即跟随一个路径量词，如a x 、e f 和a u 等。更精确地 说，c t l 是通过使用下面的规则限定路径公式的语法后获得的c t l 4 的子集： 如果，和g 是状态公式，那么x f 、f f 、g f 、f u g 和f r g 是路径公式。 有十个基本的c t l 算子：a x 和e x ，a f 和e f ，a g 和e g ，a u 和e u ， a r 和e r 。 这十个算子都能用三个算子e x 、e g 和e u 来表示： a x f 一，e x 、， e f f = e t t u e u f a g f = 一e f 一， a f f = 一e g 一， a f u g = 、e ，9 u ( 、， 、9 ) 】ae g 一9 a f r g 】= 一e 一，u 、夕】 e f r g = 一a 一，u g 】。 在研究与c t l 公式有关的问题刚，只需要考虑三个c t l 算子e x 、e g 和 e u 。 第2 章模型检测技术 7 2 1 4 线性时态逻辑l t l 线性时态逻辑u 1 l 是由形如a f 的公式组成。这里，是路径公式且，中唯 一被允许的状态子公式是原子命题。更确切地说，l t l 路径公式由下列两条规 则产生： 1 ，如果p a p ，那么p 是路径公式 2 如果，和9 是路径公式，那么、，、f v 9 、f a 9 、x f 、f f 、g f 、，u 9 和f r g 是 路径公式。 c t l + 、c t l 和l t l 具有很强的时态表达能力，在并发系统中，一般采用 它们来对系统及规范进行描述。 2 2 模型检测的原理 假如给定了系统的k r i p k e 结构m = 和需要验证的规范咖，模 型检测的实质就是验证庐在m 下是否可满足，即验证m 币是否为真 5 1 。模 型检测大致可分为以下三个步骤： ( 1 ) 系统建模 在此阶段需要把系统的k r i p k e 结构用形式化语言描述出来，即将系统的状 态集合及状态迁移关系进行形式化描述。具体使用什么描述语言要根据模 型检测工具来确定，每个不同的模型检测工具都有各自的建模语言。系统 建模的关键是正确地描述好系统的状态迁移关系这是进行规范验证的前 提条件，若是迁移关系描述有误则不能保证规范验证的结果是可靠的。此 外，还要注意尽量使用精简的方式来描述系统，避免因为引入过多变量而 造成的系统状态爆炸问题。 ( 2 ) 建立规范 通常将需要验证的系统性质表示为时态规范，即时态逻辑表达式。对硬件 或软件系统，时态逻辑能够断言系统随着时间演变的行为变化。不同的 8 模型检测时态知识逻辑及其应川 模型检测工具对规范的描述有不同的要求。如，s p i n 中的规范必须使用 l t l 来描述，s m v 则能同时接受l t l 和c t l 描述的规范。对于c t l + 描 述的规范也有一些模型检测工具能剥其进行验证。本文考虑的规范除了 包含时态算子还包括知识算子，这将在后面的章节详细介绍。需要注意的 是，我们虽然能验证系统是否满足某个规范，但由于模型检测方法是基于 语义推导的，因此并不能确定给定的规范涵盖了系统应满足的所有的性 质。 f 3 1 系统验证 在理想情况下，系统验证过程是由模型检测工具自动进行的。然而在实际 应用中常常需要人工参与，这通常涉及到对验证结果的分析。如果系统不 满足规范，模型检测工具往往会把出错的路径呈现给设计者，并能帮助设 计者跟踪到出错的地方。产生错误也可能是因为不正确的系统建模或是 不正确的规范要求所导致，而错误路径可用于发现和修补这两类问题。此 外，验证任务可能会非正常终止，这是因为模型规模太大以致于不能装进 计算机内存。在这种情况下，通常需要更改模型检测工具的参数或调整模 型后重新进行验证。 2 3 二值判定图 二值判定图f b d d s ) 是一利一表示布尔函数的高效方法，它首先是作为一种 简单的形式，即二值判定树( b i n a r yd e c i s i o nt r e e s ) 被提出来的。b d d s 中每一 个非终端结点用布尔变量z ，y ，z 标记，终端结点用1 或0 标记。每一个非终 端结点v 由一个变量v a r ( ) 标识，它有两个后继结点：l o w ( v ) 对应变量被赋值 为0 的情况，h i g h ( v ) 对应变量w 被赋值为1 的情况。每一个终端结点v 被表示 为v a l u e ( v ) ，v a l u e ( v ) 要么是0 要么是1 。从初始结点出发到终端结点，我们可 以确定该路径上对变量的真值赋值是否使该_ 值判定树表示的布尔公式为真。 如果变量”被赋值为0 ，那么从根结点到终端结点的路径上的下一个结点将是 l o w ( v 1 。如果 被赋值为1 那么路径上的下一个结点将是h i g h ( v ) 。 第2 章模型检测技术 9 图2 1 ：( a 1 甘b 1 ) a ( a 2 铮b 2 ) 的二值判定树 对于布尔函数f ( a 1 ，a 2 ，b 1 ，b 2 ) = ( a l 铮b 1 ) a ( a 2 甘b 2 ) 表示的二位比较器， 其二值判定树如图2 1 所示。 。 由于包含了一些冗余，二值判定树未能为布尔函数提供紧凑的表示，事实 上，它和真值表的大小是一样的。b r y a n tf 2 6 给出了如何得到布尔函数的规范表 示的方法，该方法是在二叉判定树上加上两个限制，得n - - - 值判定图。第一个 限制是，从树的根节点到终端节点的每一条路径上，布尔变量的出现顺序必须 一致。第二个限制是，在图中不能有同构的子树或冗余的顶点。基于以上分析， 得到三种转换规则，用于简化b d d s ： 1 删除重复的终端节点：对于同样为0 ( 或1 ) 值的终端节点，只保留其中的 一个，删除其它的0 ( 或1 ) 节点，并让原来指向被删除的0 ( 或1 ) 节点的弧 指向唯- n 下的0 ( 或1 ) 节点。 2 删除重复的非终端节点：如果b d d s 中两个节点n 和m 是结构相同的两 个子b d d s 的顶点，那么删除其中一个，并让原本指向这一节点的弧指向 另一个节点。 1 0模型检测时态知阻逻辑及其应川 3 删除满足下列条件的其中一个节点：如果对于两个非终端节点u 和v 有v a r ( u ) = v a l ( v ) ，l o w ( u ) = l o w ( v ) 并且h i g h ( u ) = h i g h ( v ) ，那么去掉“ ( 或u ) ，并让原来指向“( 或u ) 的弧指向v ( 或u ) 。这里v a r ( v ) 表示节点”所 指的变量，l o w ( v ) 和h i g h ( v ) 分别表示 所指的左右节点。 对一个b d d s 不断使用上述规则进行简化，直到无法再简化为止，这样就 得到了b d d s 的规范形式。b r y a n t 给出了自底向上化简b d d s 的过程，该过程 对于原b d d s 的大小来说，是线性时问的。由上述方法得到的图称为有序二叉 判定图( o b d d s ) f 3 3 1 ，它是布尔函数的一种规范表示形式。对于一个用o b d d s 表示的布尔函数，当我们规定了其中的某一个变量x 。为常量t r u e 或f a l s e 时， 我们就得到了一个新函数，求新函数的算法对于原0 b d d s 的大小来说，是线 性时间的。不仅如此，o b d d s 的所有1 6 个二元逻辑运算都能在线性时间内高 效实现。 布尔函数f ( a 1 ，a 2 ，b 1 ，b 2 ) = ( a 1 甘b 1 ) a ( a 2 甘b 2 ) 的o b d d s 表示朝i 图2 2 所示，规定变量顺序为a 1 b 】 a 2 5 2 。 图22 ：( n l 甘b 1 ) a ( a 2 甘b 2 ) 的o b d d s n 第2 章模型检测技术 在对有限域上的关系进行压缩表示方面，o b d d s 显得特别有用，它能有效 地缓解状态爆炸问题。如果q 是在 o ，1 ) 上的n 元关系，那么q 可以用其特 征函数的o b d d s 表示。为了表示克里普克结构m = ，我们必须描 述状态集合s ，状态迁移关系r 和标签方程l 。对于状态集合s ，我们首先需 要对这些状态编码，为了简单起见，我们假设这里恰好有2 “个状态。我们假设 妒：( 0 ，1 ) m s 为把布尔向量映射到状态的函数。由于每个赋值都是s 中一个 状态的编码，表示s 的特征函数就是取值为l 的o b d d s 。对于状态迁移关系r ，我们使用与状态同样的编码。我们需要两个布尔变量集，一个表示开始状态， 另一个表示迁移的最终状态。如果迁移函数编码成布尔关系，那么r 由特征函 数如表示。最后，我们考虑标签方程l ，尽管l 定义为从状态到原子命题子集 的映射，把它看成从原子命题到状态子集的映射将更方便。原子命题p 被映射 到状态集 s i p l ( s ) ) ，我们称这些状态集合为l ，其可用上述的编码_ p 来表 不。 2 4 符号化模型检测 符号化模型检测( s y m b o l i cm o d e lc h e c k i n 2 ) 技术 6 【2 7 是对传统模型检测 技术的巨大改进，它通过二值判定图( b d d s ) 这种高效的数据结构来表示系统 模型，并通过“演算来计算出满足系统规范的状态集合，从而方便地在超大规 模的状态空间中来验证系统的性质。符号化模型检测自上个世纪9 0 年代出现以 来已经普遍应用于大规模集成电路系统的设计中7 1 它能验证的状态规模已经 达到l o ”o 3 4 ，从而很好地解决了状态爆炸问题。 在很多情况下，时态逻辑表达式的验证问题要涉及到不动点的运算f 3 5 1 。简 单来说，“演算就是在c t l 的分支时间模型中加入最大和最小不动点，因此可 以表达所有的( 不公平) c t l 结构。对于变量x 和命题公式，p ，和o ，分 别表示，相对于变量。的最小不动点和最大不动点。 目前最常见的符号化模型检测工具是s m v ( s y m b o l i cm o d e l e r 析e r ) 及其 增强版本n u s m v ( r e l bs y m b o l i cm o d e lv e l 、i f i e f ) 2 3 1 。s m v 是在1 9 8 7 年秋天由 卡内基一梅隆大学在读博士生m c m i l l a n 开发的，而n u s m v 在s m v 基础上加 入了一些新特性，如对有界模型检测( b o u n d e dm o d e lc h e c k i n g ) f 3 6 1 的支持。此 1 2 模型检删时态知识逻辑及其应用 外，n u s m v 是开放源代码的软件，研究者可以根据自身需要对其进行改进。本 文所使用的工具正是在n u s m v 的基础上改进而来的，这将在第4 章详细介绍。 第3 章知识与多智能体系统 不同领域( 如经济学、语言学、人工智能以及理论计算机科学) 的学者们都 对知识推理产生了兴趣。当然，这些学者也对哲学家们研究的一些问题感兴趣， 只是研究的焦点不一样而已。首先，存在许多对知识与动作之间关系的研究。例 如，机器人在打开一个饭橱前需要知道些什么? 机器人如何知道自己是否知道 足够的信息去打开这个饭橱? 一个商务智能体在什么程度上能够知道足够的信 息，以便于停止收集信息并作出决策? 等等。其次，计算知识的复杂度也是一个 研究方向。另外，知识推理研究的重点是针对群体智能体的情况，而非单个智 能体的情况。 本章主要根据3 1 来介绍有关知识推理方面的理论。 3 1 1 可能世界模型 3 1 知识的定义 我们的知识建模框架是基于可能世界( p o s s i b l ew o r l d s ) 的。可能世界模型可 直觉理解为在除了事件真实发生的状态外，还有其他许多这个事件可能发生的 状态( 或“世界”) 。一个智能体根据其当前拥有的信息不能说出这些可能世界中 哪一个是事件实际发生的状态。如果妒在一个智能体认为可能的所有世界f 根 据他当前拥有的信息) 中均为真，那么我们说这个智能体知道妒。从直觉上看， 一个智能体认为可能存在的世界越少，则他的怀疑越少，而他知道的就越多。 在扑克牌游戏中，可能世界有一个具体的解释：他们是牌被分发到玩家手 中的所有可能的情况。最初，一个玩家会考虑与他手中的牌相一致的所有可能 的发牌情况。玩家在玩牌的过程中可以获得一些附加的信息，使得他们可以据 此消除一些可能世界。即使a l i c e 不知道b o b 原先持有黑桃，但是如果她获得 了一些附加的信息使得她能够将b o b 手中没有黑桃的所有这样的世界消除，那 么她也可能在某一步中知道b o b 原先持有黑桃。 1 4 模型检删时态知识逻辑及其应用 为了使这些概念更为精确，首先我们要采用某种语言来直接表示知识这一 概念。对于复杂的知识推理，英语并不是一个特别好的语言。在这里我们采用 模态逻辑语言( m o d a ll o g i c l 。 假设有一个群体由n 个智能体组成，分别为l ，n 。为简单起见，我们假 设这些智能体希望推理的世界可以由一个非空的原子命题集合函来描述。这些 原予命题表示世界中的基本事实，比如“旧金山是晴天”或“a l i c e 的前额有泥 巴”。为了表达像“b o b 知道旧金山是晴天”这样的命题，我们在语言中增加模 态算子”，k 。( 每个对应一个智能体) 。这样，命题k ，妒就读为“智能体1 知道妒”。 从技术上说，一个语言就是公式的一个集合。我们由西中的原予命题开始 通过否定，合取和模态算子k ，k 。构成更复杂的公式。这样，如果妒和妒 是公式，则、妒，( 妒a t j ) 雨i 尬妒( i = 1 ，n ) 也是公式。为了增加可读性，我们 在不致引起混淆的情况下忽略圆括号。并使用命题逻辑的标准缩写，比如妒v 妒 对一( ，妒a 一妒) ，妒 砂对一妒v 妒，和妒甘妒对( 妒号妒) a ( 妒号妒) 。我们用 t r u e 作为某些固定的命题重言式的缩写，比如p v ，p ，用f a l s e 作为、t r u e 的缩 写。现在我们可以用这个语言来直接表达一个复杂的命题了。例如，公式 k 1 k 2 p a k 2 k l k 2 p 表示智能体1 知道智能体2 知道p ，但是智能体2 不知道智能体1 知道智能体 2 知道p 。 我们将可能性视为知识的对偶。这样，如果智能体1 不知道，妒则他认为妒 可能为真。这种情况可由公式、虬、妒表述命题“d e a n 不知道妒是否成立” 表示d e a n 认为妒和、妒均有可能。 我们已给出了这个语言的语法( 合式公式的集合) ，现在需要定义语义，也 就是一个用于决定一个给定公式是否成立的形式模型。我们根据可能世界定义 语义，并用( k ? j p k e ) 结构形式化。定义在妒上的n 个智能体的k r i p k e 结构m 为元组 ( s ，7 r ，疋，足。) ， 其中s 为状态或可能世界的集合，”为解释，即把s 中的每个状态下的原子命 题和真值赋值联系起来( 对于每个s s ，”( s ) ：妒一 t r u e ，f a l s e ) ；i c 。为s 上 第3 章知识与多智能体系统1 5 的二值关系( b i n a r yr e l a t i o n ) ，即s 中元素对的集合。 真值赋值( s ) 告诉我们在状态s 下，原子命题p 是t r u e 还是f a l s e 。这样， 如果p 表示事实“旧金山正在下雨”，则”( s ) ( p ) = t r u e 表示在结构m 的状态 s 中旧金山正在下雨。二值关系疋刻画智能体i 的可能性关系：如果智能体i 在世界s 中根据他当前拥有的信息认为可能存在世界t ，则( s ，t ) 心。我们将 e l 看作是一个可能性( p o s s i b i l i t y ) 关系，是因为它定义了在任意给定的一个世 界中，智能体i 认为可能存在的世界集合。 现在我们定义在一个结构的一个给定的状态中，一个公式为t r u e 的语义。 注意真值依赖于结构和状态，一个公式在一个状态为t r u e 而在另一个状态为 f a l s e 是很有可能的。例如，智能体1 可能在一个世界中知道旧金山是晴天而在 另一个世界中却不知道。我们在妒的结构上归纳定义 关系，即( m ，s ) 妒 ( 读为“l p 在( m ，s ) 中为t r u e ”或“妒在( m ，s ) 中成立”或“( m ，s ) 满足妒”o 当妒是一个原子命题时，我们可以用结构中的7 r 处理这一基本情况： 对于任意的原子命题p 曲，( m ，s ) p 当且仅当巧( s ) ( p ) = t r u e 合取及否定的处理与命题逻辑的相尉：砂a 砂为t r u e 当且仅当砂和妒同 时为t r u e ，而一妒为t r u e 当且仅当妒不是t r u e ： ( m ，s ) 妒a 妒7 当且仅当( m ，s ) 妒和( m ，8 ) 矽 ( m ，8 ) ，妒当且仅当( m ，s ) 睁妒 注意否定公式的定义保证了这个逻辑是二值的。对于每个公式砂，我们有要么 ( m ，8 ) 妒要么( m ，s ) ，妒，但不会同时满足。 最后，我们开始处理形如尬妒的公式。这里我们根据直觉可知，智能体i 在结构m 的世界8 中知道妒当且仅当智能体i 在世界s 中认为可能存在的所 有世界中廿均为t r u e 。形式地，我们有 ( m ，s ) k 妒当且仅当对于所有满足( s ，t ) 厩的状态t ，有( m ，t ) 妒 1 6模型检测时态知识逻辑及其应用 3 1 2 公共知识和分布知识 在上一节中介绍的语言不能表示公共知识和分布知识。为了表示这些概念， 我们在语言中加入模态算子正b ( 群体g 中的智能体都知道) ，c 台( 群体g 中所 有智能体的公共知识) 和d g ( 群体g 中所有智能体的分布知识) 。因此对于每 个非空集g f l ，n ) ，如果妒是一个公式，则正b 妒，c b 妒和d g 妒也是公 式。当g 是所有智能体的集合时我们常常省略下标g 。这样我们就可以表达 像玛、q 1 ，2 伊( 智能体3 知道p 不是智能体i 和2 的公共知识) 和d qa 、e q ( q 是 分布知识但不是公共知识) 这样的命题。 我们容易在一个结构m 中扩展真值定义来处理公共知识和分布知识。因 为髓妒为t r u e 当且仅当g 中所有智能体都知道妒，我们有 ( m ，s ) 玩r 妒当且仪当对于任意的i g ，有( m ，s ) 甄妒 公式e 台妒为t r u e 当且仪当g 中所有智能体知道妒，g 中所有智能体知道 g 中的所有智能体知道妒，等等。令e g 妒为妒，璐? 1 妒为f 1 g 磁妒的缩写，而 踢妒为e g ：。则我们有 ( m ，8 ) 妒当且仅当对于所有的= 1 ，2 ，有( m ：s ) 磁妒 如果一个群体g 的成员的“组合”知识蕴涵妒，则g 拥有分布知识妒。如 何在我们的框架中获取这样的组合知识呢? 通常，我们通过消除g 中每一智能 体认为不可能存在的世界来组合g 中智能体的知识。在技术上我们可将群体中 每一智能体认为可能存在的状态集合取交集。这样我们定义 ( m ：s ) d g 妒当且仅当对于所有满足( s ，t ) n ，g 赶。的状态t ，有( m ，t ) 妒 3 1 3 知识的性质 描述我们的知识解释中的性质的一个方法是刻画那些总是为t r u e 的公 式。更形式地，给定个结构m = ( s ，7 r ，疋1 ，k 。) ，如果对于所有的s s 有 ( m ：s ) 妒，则称妒是在m 中有效的( v a l i d ) ，记为m 妒。如果存在s s 使 得( m ，s ) = 妒，则称妒是在m 中可满足的( s a t i s f i a b l e ) 。如果妒在所有的结构 第3 章知识与多智能体系统 中是有效的，则称妒是有效的，记为 妒。如果妒在某些结构中是有效的，则 称妒是可满足的。显然，一个公式妒是有效的( 或是在m 中有效的) 当且仅当 、妒是不可满足的( 或在m 中是不可满足的) 。 我们现在将知识定义中的有效性质列出来，然后讨论这些性质的合理性。 本节假设可能性关系舷是等价关系。 知识定义的一个重要性质是每个智能体都知道所有关于他的知识的逻辑推 论。如果一个智能体知道妒并且也知道妒蕴涵砂，那么妒和妒号妒在所有他 认为可能存在的世界中均为t r u e 。这样妒在所有他认为可能存在的世界中也是 t r u e ，因此他必定也知道砂。即 ( 凰妒 甄( 妒= 争妒) ) = 峨妒 这个公理称为分配公理( d i s t r i b u t i o na x i o m ) ，因为它允许在蕴涵式中分配 算予。这意味着智能体具有相当强的推理能力。 我们的知识定义中的智能体具有相当强的推理能力，还因为智能体知道一 个给定结构中的所有有效公式。如果一个公式妒在结构m 的所有可能世界中 均为打u e ，则妒在所有他认为可能存在的世界中也是t r u e ，因此k 妒在结构m 的所有可能世界中均为t r u e 。更形式地，我们有下列知识概括规则( k n o w l e d g e g e n e r a l i z a t i o nr u l e ) ： 对于所有的结构m ，如果m 帆则m 甄【p 从中可知如果妒是有效的，那么尬妒也是有效的。这个规则与公式妒号妒 完全不同，后者说的是如果妒是t r u e ，则智能体i 知道妒。因为一个智能体不一 定知道所有为t r u e 的事情，然而却必然知道所有有效的公式。直觉上即存在必 然为t r u e 的公式，也存在偶然在某一给定状态中为t r u e 的公式。 虽然智能体可能不知道为t r u e