（计算机软件与理论专业论文）命题投影时序逻辑的可判定性.pdf

摘要 摘要 本文主要研究命题投影时序逻辑( p r o p o s i t i o n a lp r o j e c t i o nt e m p o r a ll o g i c ， p p t l l 的可判定性问题。文中简要地介绍了p p t l 公式的语法、语义及逻辑规 则，定义了p p t l 公式的正则形( n o r m a lf o r m ) 和完备正则形( c o m p l e t en o r m a l f o r m ) 。在正则形的基础上，给出p p l m 公式正则图( n o r m a lf o r mg r a p h ) 的归纳 定义和可执行的算法，证明了该算法的可终止性。基于正则图，p p t l 公式在 无穷区间范围的可判定性问题得到解决。另外，本文也给出了命题区间时序逻 辑( p r o p o s i t i o n a li n t e r v a lt e m p o r a ll o g i c ，p i t l ) 在无穷区间范围的判定过程。 逻辑的可判定性是基于该逻辑的模型检测方法的基础，本文给出的判定算 法证实了基于p p t l 的模型检测方法的可行性。文章最后回顾了模型检测工具 的发展现状，分析了以p p t l 为逻辑基础的模型检测工具的优越性，阐明了开 发基于p p t l 的模型检测器的必要性，且给出了基于p p t l 的模型检测器的概 要设计。 关键词：命题投影时序逻辑i e 贝u l 形判定过程模型检测无穷模型 a b s t r a c t a b s t r a c t v t h i sd e s s a t a t i o ni n v e s t i g a t e st h ed e c i d a b i l i t yo fp r o p o s i t i o n a lp r o j e c t i o nt e m p o r a l l o g i c ( p p t l ) t h es y n t a x ，s e m a n t i c sa n dl o g i cl a w so fp p t la r eb r i e f l yp r e s e n t e d n o r m a lf o r ma n dn o r m a lf o r mg r a p hf n f a r ed e f i n e df o rp p t lf o r m u l a s f u r t h e r , b a s e do nn f gad e c i s i o np r o c e d u r ef o rc h e c k i n gt h es a t i s f i a b i l 时o fp p t lf o r m u l a s 诵t l l i n f i n i t em o d e l sa r ef o r m a l i z e d a n de x a m p l e sa g eg i v e nt os h o wh o wt h ea l g o r i t h mw o r k s i na d d i t i o n , ad e c i s i o na l g o r i t h mf o rc h e c k i n gt h es a t i s f i a b i l i t yo fp r o p o s i t i o n a li n t e r v a l t e m p o r a ll o g i c ( p i t l ) f o r m u l a si sa l s op r e s e n t e d d e c i d a b i l i t yo ff o r m u l a si saf u n d a m e n t a li s s u ei nt h em o d e lt h e o r yo fal o g i c m o r e o v e r , s a t i s f i a b i l i t yp l a y sa ni m p o r t a n tr o l ei nt h em o d e lc h e c k i n ga p p r o a c h b a s e do n t h ed e c i s i o np r o c e d u r ef o rc h e c k i n gt h es a t i s f i a b i l 时o fp p l lf o r m u l a s ，m o d e lc h e c k i n g b a s e do np p t lc a nb er e a l i z e d a tt h ee n do ft h i st h e s i s c u r r e n tm o d e lc h e e k e r sa a n a l y z e dt os h o wt h ea d v a n t a g e so ft h em o d e lc h e c k e rb a s e do np p r l a l s ot h em o d e l c h e c k e rb a s e do np p t li sb r i e f l yd e s i g n e d k e y w o r d s ：i n t e r v a lt e m p o r a ll o o e n o r m a lf o r md e c i s i o np ro e e d n r e m o d e lc h e c k i n gi n f i n i t em o d e l 创新性声明 本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研究 成果。尽我所知，除了文中特别加以标注和致谢中所罗列的内容以外，论文中不 包含其它人已经发表或撰写过的研究成果：也不包含为获得西安电子科技大学或 其它教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做 的任何贡献均已在论文中做了明确的说明并表示了谢意。 申请学位论文与资料若有不实之处，本人承担一切相关责任。 本人签名：望j 整日期鎏! 皇! ! 兰? 关于论文使用授权的说明 本人完全了解西安电子科技大学有关保留和使用学位论文的规定，即：研究生 在校攻读学位期间论文工作的知识产权单位属西安电子科技大学。本人保证毕业 离校后，发表论文或使用论文工作成果时署名单位仍然为西安电子科技大学。学 校有权保留送交论文的复印件，允许查阅和借阅论文；学校可以公布论文的全部 或部分内容，可以允许采用影印、缩印或其它复制手段保存论文。( 保密的论文在 解密后遵守此规定) 本学位论文属于保密，在一年解密后适用本授权书。 本人签名： 导师签名： 日期坦垄! 旦兰p 日期! 尘2 兰：! 一鹾 第一章绪论 第一章绪论 随着i n t e r n e t 的发展和工业界需求的不断提高，软、硬件系统的复杂度与日 俱增，系统的正确性已越来越受科学界和工业界的关注。定义在严密的数学和逻 辑基础上的形式化方法成为解决这一问题的有力工具。在学术界，对相关课题的 研究集中了世界上最优秀的数学家和计算机科学家，他们广泛地分布于世界上最 著名的高校、科研机构和公司；在工业界，几乎所有的世界顶尖i t 公司都投入大 量的人力和物力来开发它们的验证和测试工具。 i 1 形式化验证 形式化验证 o r m a lv e r i f i c a t i o n ) 起源于2 0 世纪6 0 年代的软件危机。直至整个 7 0 年代，形式验证技术所针对的仅是一般的转换型程序，即进行单纯的科学计算、 计数等功能的软件，所采用的主要是定理证明( t h e o r e mp r o v i n g ) 技术。8 0 年代初， p n u e l i 将时态逻辑引入到反应式程序的验证【4 3 】，c l a r k e 等提出了模型检验( m o d e l c h e c k i n g ) 方法m ，4 5 j ，并实现了对并发系统的自动验证，使得形式化验证技术有了 很大的进展。在形式化验证发展的基础上，形成了两类主要的方法，一类是以逻 辑推理为基础的演绎验k 正( d e d u c t i v ev e r i f i c a t i o n ) ，另一类是以穷尽搜索为基础的模 型检钡f l ( m o d e lc h e c h i n g ) “。 演绎验证是通过使用逻辑公式描述系统及其性质，然后从公理出发推导性质， 实现对系统的验证。在这个过程中，往往需要用户提供或引入某些定义或引理。 其优点是可以使用归纳的方法来处理无限状态的问题，并且能够在证明过程中帮 助用户对系统和被证明的性质有更多的了解；但是，其缺点是不能做到完全自动 化，其间需要和用户交互，导致证明过程非常耗时而且容易出错。演绎验证主要 有na r l r a ld e d u c t i o n ，r e s o l u t i o n 以及h o a r e - l o g i c 等方法。 模型检测是将要验证的系统表示成有限状态机，将要验证的性质用时序逻辑 公式描述 4 3 , 4 6 , 4 ”。然后，遍历有限状态机以检验性质是否存在。有限状态机模型通 常采用k r i p k c 结构i s a s ，在该结构上路径是无限延伸的。模型检验的优点是：全自 动进行而无须人机交互。当断定某性质不满足时，模型检验能提供反例，以便于 定位设计错误。凭借时态逻辑强大的描述能力，模型检验能够对各种复杂的时序 性质进行验证。但是模型检测也有自己的缺点状态空间爆炸问题。所谓状态 空间爆炸问题，主要指的是系统状态数随着系统规模的增加呈指数增长的问题， 所以需要采用各种方法消减算法搜索的状态数，常用的方法有符号化模型检测 ( s y m b o l i cm o d e l c h e c k i n g ) ”3 1 4 j 、偏序规约( p a r t i a lo r d e rr e d u c t i o n ) 1 5 1 、组合验证 命题投影时序逻辑的可判；性 ( c o m p o s i t o i n a lv e r i f i c a t i o n ) 和抽象( a b s t r a c t j o n ) 等技术。由于模型检测方法是 完全自动的，并且在系统性质未被满足时可以给出反例，帮助用户发现错误，因 而这种验证方法格外受到人们的青睐，目前模型检测方法已被成功的应用于网络 f l 艮务- ( w e bs e r v i c e ) 1 8 9 1 ，数字电路系统，混和、实时系统m2 1 1 以及j a 、，a 代码【2 2 】 的验证中。 1 2 1 模型检测简介 1 2 模型检测 模型检测就是给定要验证的系统( s ) 和该系统应该满足的性质 ) ，由模型检测 工具自动地验证系统是否满足性质，si = f 。模型检测过程主要分为三个阶段：系 统建模、性质描述和模型验证，如图1 1 所示。 图1 1 模型检测过程 系统建模：分析所要验证的系统，用模型检测工具的系统描述语言来刻画系 统。在建模过程中，需要对系统进行一定程度的抽象，所建立的模型应当如实反 映系统的行为，并且规模应该紧凑。这个阶段在模型检测过程中最为耗时，而且 对系统的理解深刻与否直接关系到所建模型的好坏。 性质描述：提出所要验证的性质，用某种时序逻辑公式描述。模型检测工具 只能确定模型是否满足所给出的时序逻辑公式，因而若要得到正确的模型检测结 果，所给公式应该确切的刻画出我们所关心的性质。 模型验证：用模型检测工具验证模型是否满足给出的时序逻辑公式。狭义的 验证过程是指对模型的状态空间进行搜索，这是由模型检测工具自动完成的。广 义的验证过程包括搜索状态空间、发现错误、修改系统或模型、再搜索这样一个 反复的过程。 第一章绪论 1 2 2 模型验证方法 模型验证是一个状态空间的穷尽搜索过程，搜索的可穷尽性有赖于为系统建 立的有穷状态模型。一般来说，模型检测工具所使用的状态空间搜索方法可分为 两种：局部方法和全局方法。 全局方法首先产生系统的整个状态空间，并计算出满足原子命题公式的状态， 然后根据公式的结构自底向上进行计算。全局方法的缺点是对存储空间的要求比 较高，需要存储系统的所有状态，不过使用符号化模型检测技术，可以有效地降 低算法的存储需求。全局方法的优点是在算法结束时不仅能知道系统是否满足性 质，而且还能知道系统的哪些状态满足性质。 局部方法并非在一开始就产生出系统的全部状态空间，而是边搜索边产生， 只产生搜索过程中所需要的那部分状态空间，也叫o n 地n y 方法【2 ”。这样做避免 了预先生成全部的状态空间，如果系统不满足性质，那么有可能只产生和搜索了 部分状态空间就发现结果。但是，如果系统满足这个性质，那么仍然需要产生全 部的状态空间。如l t l 模型检测算法，对于待验证的系统s 和l t l 公式由，算法 首先把公式，巾转化为另一个系统s 1 ，然后对s 和s _ 的同步组合系统进行深度优 先搜索，在搜索时只产生搜索过程所需要的局部状态空间，并进行性质检测。相 对于全局方法，局部方法对存储空间的要求相对较低，但是由于搜索过程需要不 断的回溯，局部方法的时间代价比较高。 1 2 3 模型检测的发展 可以说，模型检测技术的发展历史就是不断寻找新思路、新策略和新算法来 克服状态空间爆炸问题的历史。模型检验技术产生于8 0 年代初，由美国的c l a r k e 和e m e r s o n “, 4 s ，法国的q u i e l l e 和s i f a k i s l 4 9 分别独立提出。当时的模型检验算法 都是通过显式地枚举可达状态来验证性质，通常所能处理的状态数也就在几百万 左右。状态数呈指数上升的状况和显式模型检验有限的处理能力之间存在难以克 服的矛盾。1 9 8 6 年，b 掣m t 【5 0 】将传统的b d d ( b i i l a r yd e c i s i o nd i a g r a m ) 技术加以改 进，使之成为布尔表达式的规范表示方法。m c m i l l a n 在1 9 8 7 年将这种技术应用于 模型检验中【5 1 , 5 2 ，取得了巨大的成功，使模型检验的发展再度复兴。基于b d d 的 模型检验称为符号模型检、狈t j ( s y m b o l i cm o d e lc h e c k i n g ) 。符号模型检验的主要思想 是用o b d d 来隐式地表示有限状态机的状态和状态之间的迁移，其优点是能够表 示一组而不是单个的状态和状态之间的迁移关系，因此大幅度降低了对存储空间 需求。实验表明，符号模型检验方法能处理的状态数达i 0 2 0 量级【5 l l ，进一步改进 4 命题投影时序逻辑的可判定性 的算法所能处理的状态数达到1 0 1 2 0 盼5 4 i 。 模型检验理论经提出后，在工业界取得了巨大的成功。但符号模型检验并没 有彻底地解决问题，其最大瓶颈仍然是：存储和操作b d d 时对内存要求过大。定 界模型检验技术是继符号模型检验后的又一重要进展，该技术是由b i e r e 等在i 9 9 9 年提出。定界模型检验的主要思想是：在限定的步数k 内，考察系统运行的情况， 确定性质是否满足。若不能确定性质是否存在，则提高k 值，重新进行检验。在 每一个检验周期内，定界模型检验问题被转化成s a t ( s a t i s f i a b i l i t y ) 问题求解。s a t 问题虽然已被证明是n p - e o m p l e t e 问题，但在实际应用中却很有效。 综上所述，现今模型检验问题的研究已经取得了重大的进步，但它仍然是具 有挑战性的研究课题。 1 3 时序逻辑 在模型检测方法中，时序逻辑作为一种规范语言( s p e c i f i c a t i o nl a n g u a g e ) 被 广泛地应用于数字电路系统“o j 7 ，5 9 , 5 9 1 ，软件工程删，人工智能【l l 】，医疗协议 9 1 等领 域的形式化验证中。 按照对时间的看法，时序逻辑可分为线性时序逻辑( l i n e a rt e m p o r a ll o g i c ) 和分 支时序逻辑( b r a n c h i n gt e m p o r a ll o g i c ) ，具有代表性的分别是l t l 【2 3 】和c o m p u t i n g t r e el o g i c ( c t l ) 1 2 4 , 2 5 1 。对于一个状态s ，孤立的看，从s 开始的一个计算只是由状 态形成的一个无穷序列，联系的看，从s 开始的所有计算形成一棵由状态组成的无 穷树。l t l 公式所刻画的就是从s 开始的每一个孤立计算所具有的性质，若从s 开始的每一个孤立计算都满足l t l 公式巾，那么s 满足巾；c t l 公式所刻画的是从 s 开始的计算的全体所具有的性质，如果从s 开始的计算的全体满足c t l 公式咖， 那么s 满足由。表达能力上，l t l 和c t l 各有千秋，都能表达出一些对方无法表 达的性质。l t l 公式刻画的是孤立的计算，具有直观，容易理解的优点。但是l t l 模型检测算法的复杂度较高，线性于待验证的系统的状态空间规模，而指数倍于 l t l 公式的大小，其复杂度为o ( j 1 9 2 1 | ) ，其中| l 是系统状态空间的大小，是l t l 公式m 的长度。虽然如此，但是对于较短小的公式，l t l 模型检测算法的复杂度还 是可以接受的。最早提出的c t l 模型检测算法的复杂度多项式倍于系统状态空间 的规模，也多项式倍于c t l 公式的大小。后来改进的c t l 模型检测算法的复杂 度线性于系统状态空间的规模和公式的长度的乘积，o ( ( i e i + i r _ 1 ) g l 6 1 ) ，其中吲是系 统状态迁移关系的规模。 作为线性时序逻辑的一种，区间时序逻辑已被大量应用于硬件电路、实时系 统等领域。区间逻辑区别于点式逻辑( p o i n tb a s e dt e m p o r a ll o g i c ) 的根本性质是公式 的语义解释在区间上( i m e r v a lb a s e dt e m p o r a ll o g i c ) ，而不是在时间点上。对于某些 第一章绪论 性质，例如，“a 在任意长于l 的观察区间上总为真”等，使用区间逻辑来描述、推 导更方便、更自然。作为区问时序逻辑的代表，i n t e r v a lt e m p o r a ll o g i c ( i t l ) i t 于 1 9 8 3 由b m o s z k o w s k i 最早作为数字电路的规范语言被提出。l t l 公式最初仅被定 义在有穷区间上，d u a n 于i 9 9 4 年将该逻辑扩展到无穷区间上并引入了一个新的时 序操作符p 巧瞄j ，形成了i t l 的一个扩展逻辑，p r o j e c t i o nt e m p o r a ll o g i c ( p t l ) 。 1 9 9 5 年，b m o s z k o w s k i 亦将i t l 扩展到无穷区间范围。 1 4 区间时序逻辑的研究现状 区间时序逻辑自诞生以来，凭借它强大的描述能力和简单直观的特点颇受工 业界的青睐。特别是与l t l 和c t l 相比较，i t l 既能用来描述顺序行为，又能用 来描述并发行为。二十多年以来，先后有众多的科学家从事区间时序逻辑相关领 域的研究，并且取得了显著的成果。 公理证明系统 命题、一阶区间时序逻辑的公理证明系统已趋于成熟【3 6 l ，并且i t l 公式证明器 p v s 已被开发且广泛地应用于软件工程和实时系统中。例如，参考文献口刀中应用 p v s 做u m l 类图和序列图一致性的检验，文献d s 中用p v s 做飞机订票系统的形 式化描述和验证。 时序逻辑程序设计语言 m o s z k o w s k i 以区间时序逻辑的可执行子集为基础定义了一个时序逻辑程序设 计语言，并开发了相应的解释器( a n a ) t e m p 呦【3 6 】。d u a n 在扩展后的区间时序逻辑 p t l 中引入框架( f r a m e ) 技术，有效地处理了时序逻辑程序中变量值的继承问题， 并开发了相应的框架时序逻辑程序设计语言及解释器b3 9 , 4 0 , 5 5 , 5 6 1 。 遗憾的是，在前辈们的研究成果中，我们看不到区间时序逻辑在模型检测方 法中的应用。现有的模型检测工具，都是以线性时序逻辑或者计算树逻辑为性质 规范语言，而不能支持区间时序逻辑。逻辑可判定性是以该逻辑为基础的模型检 测方法的先决条件，因此，要将区间时序逻辑引入模型检测领域，必须从命题区 间时序逻辑的可判定性问题着手。 对命题区间时序逻辑的可判定性问题的研究已经历了一个漫长的、曲折的发 展过程。1 9 8 3 年，著名学者m o s z k o w s k i 给出了q p i t l ( q u a n t i f i e dp r o p o s i t i o n a li n t o - r v a lt e m p o r a ll o g i c ) 可满足性的判定算法【1 ，3 2 3 3 1 。s k o n o 于1 9 9 5 年完成了q p i t l 的基于t a b l e a u x 方法的判定算法1 3 4 1 。2 0 0 3 年，h b o w r a a n 和s t h o m p s o n 给出了 p i t l 的判定算法【4 3 5 】。s k o n o 和b o w m a n 的判定算法中都用了p i t l 公式的正则 形，这一正则形最早是由d u a n 【2 】提出并应用在框架投影区间时序逻辑程序语言 中。 6 命题投影时序逻辑的可划定性 区间时序逻辑最初仅被定义在有穷区问范围内，尽管d u a n 和m o s z k o w s k i 先 后分别将p t l 和i t l 扩展到无穷区间，在现有的判定算法中，区问时序逻辑公式 的解释依然被限定在有穷区间内。事实上，现实世界中的系统大多都是与外界不 断交互信息的反应系统( r e ae t i v es y s t e m ) ，这种系统一般具有不终止的特点。所以 要将区间时序逻辑广泛的应用在模型检测领域中，将该逻辑扩展到无穷区间范围 内是必要的，并且它在无穷区间范围上的可判定性也是必须证明的。因此，本文 研究命题投影时序逻辑在无穷区间范围可满足性的判定问题。 1 5 论文组织结构 本文研究命题投影时序逻辑的可判定性。文中简单地介绍了命题投影时序 逻辑公式的语法、语义及逻辑规则，定义了该逻辑公式的正则形和完备正则形。 在正则形的基础上，给出了命题投影时序逻辑公式正则图的递归定义和可执行 的算法，并证明了该算法的可终止性。基于正则图，给出了命题投影时序逻辑 在无穷区间范围内可满足性判定过程。另外本文也给出了命题区间时序逻辑在 无穷区间范围内可满足性的判定过程。文章最后研究了模型检测工具的发展现 状，分析了以命题投影时序逻辑为逻辑基础的模型检测工具的优越性，证实了 开发该工具的必要性，并给出了初步的设计框架图。 全文由六章组成： 第一章为绪论部分。简要地介绍了形式化验证、模型检测和时序逻辑，以及 本文的研究对象，区间时序逻辑、投影时序逻辑的研究现状和存在的问题。 第二章分为两部分，第一部分简单地介绍了命题投影时序逻辑的语法、语义、 逻辑规则等；第二部分从c h o p 操作符和投影操作符两方面对投影时序逻辑和区间 时序逻辑进行对比，分析了他们的表达能力，并且给出了投影操作鲥的应用实例。 第三章证明了命题投影时序逻辑的可判定性，是全文的主体部分。为了解决 命题投影时序逻辑的可判定性问题，文中定义了该逻辑公式的正则形( n o r m a lf o r m ) 和正则图( n o r m a l f o r m g r a p h ，n m ) ，给出了正则图的构造算法，并证明了该算法 的可行性。在正则图的基础上命题投影时序逻辑的可判定性得到解决。本章最后 用具体的实例展示了该判定算法的工作过程。 第四章简要地介绍了命题区间时序逻辑的语法和语义，定义了该逻辑公式的 正则形和正则图，给出了正则图的递归定义和构造算法。基于正则图，完成了命 题区间时序逻辑在无穷区间范围内可满足性的判定过程，并将这一判定算法与命 题区间时序逻辑现有的判定算法进行对比。 第五章研究了模型检测工具的发展现状，分析了以命题投影时序逻辑为逻 辑基础的模型检测工具的优越性，证实了开发该工具的必要性，并给出了初步 第一章绪论 7 的设计框架图。 第六章为结论部分。在总结本文主要工作的基础上，指出需改进之处和进一 步的研究问题。 第二章命题投影时序逻辑 第二章命题投影时序逻辑 9 投影时序逻辑( p t l ) 脚是基于区间的时序逻辑( i n t e r v a lb a s e dt e m p o r a ll o g i c ) ， 它是区间时序逻辑( i t l ) 【1 1 的一种扩展。由于i t l 是定义在有穷区间上的逻辑，所 以用它无法描述系统的无穷行为。p t l 将i t l 扩展到无穷区间范围内并引入了一 个新的并发时序操作符，投影操作符( p l j ) 。本文关注的是命题投影时序逻辑( p p t l ) 。 2 1 1p p t l 的语法 1 ) 3 ) 4 、 2 1 命题投影时序逻辑 p p t l 公式包括以下符号及括号： 命题常量：廿i l e 。f a l s e 原子命题：p ，q ，p t ，p 2 联结词： 1 ， ，v ，一( 蕴涵) ，冉( 等价) 时序操作符：o ( n e x t ) ，口( a l w a y s ) ，( s o m e t i m e s ) ，o ( w e a kn e x t ) ， ；( c h o p ) , p r j ( p r o j e c t i o n ) 5 ) 其他p f i l 公式： e m p t y ，m o r c ，s k i p ，l e n ( n ) 定义2 1 用p r o p 表示原子命题的集合，p p t l 公式归纳定义如下： p ：= p i p l y p 2 i _ 1 p l io p l i 口l ，p m ) 埘q 其中p p r o p ，p i ，p m 和q 为p p l l 公式。 另外p p t l 有以下导出公式： a l ：e m p t y 山_ - - f1 0 t m e a 3 ：o o p 型f p a s ：l e n ( n ) o “e m p t y a 7 ：l e n ( 0 ) 鬯fe m p t y a 9 q p 型f e m p t y vo p a l l ：d p 磐，p a 2 ：m o r eo t r u e a 4 ：o “p 磐0 ( 0 + 1 n 氐：l e i l ( n ) 磐0 1 ( n 1 ) ，n l a 8 ： s k i p d e - - fl e n ( 1 ) a l o ：o p a e - - ft r u e ；p a 1 2 ：p ；q 些q ) p r j e m p t y 命题投影时序逻辑的可判定性 a 1 3 ：f a l s e c = l e fp 1 p 2 1 2p p t l 的语义 a 1 4 ：t r u e o = k 4 p v 1 p 在p p t l 中，连接词- 1 ， ，v ，一( 蕴涵) 和付( 等价) 与经典命题逻辑中的 定义一致。 1 ) 状态( s t a t e ) 参照k r i p k e 结构【5 1 ，我们定义状态s 为从p r o p 到布尔值b = t r u e ，f a l s e 1 约 射，s ：p r o p b 。用s i p 表示p 在状态s 的值。 2 ) 区间( i n t e r v a l ) 区间。由一个非空的状态序列组成，该序列可以是有穷序列，也可以是无穷序 列。区间的长度f h l a l 来表示。对于无穷区间，l a i = c o ；而对于一个有穷区间，区间 长度为该区间的状态数减1 。 为了统一有穷区间和无穷区间的表示，我们做以下相关规定： n o 表示非负整数的集合 n , o 表示n o u = 对于任意的i n o ，i 国 蔓表示曼一 ( ，) ) 为了表达方便，用 s o ，s i ，s l 矿表示o ，当。无穷时8 h 无定义。f f ( i j ) 表示以s i 为第一个状态且8 j 为最后一个状态的子区间 。a 表示从状态s i 到该区间 末的子区间 s k ，s w ? 。 3 ) 投影区间 令o r = 1 ) ，且0 s r l s r 2 s r h ! i o l 。从区间a 到r l ，r h 的投影区间表示为： o i ( r l ，rh ) = 其中，t i ，t 4 是通过从r l ，i h 中去掉重复的数字而得到的。例如： l ( o ，o ，2 ，2 ，3 ) = 这里要强调的是，如上定义的投影区间能够处理终点公式( t e r m i n a lf o r m u l a , 详细 定义见2 1 3 节) 。例如公式( e m p t y , l e n 2 ，e m p t y , e m p t y , l 锄1 ) p r j l e n 2 的语义描述如图 2 1 示。 第二章命题投影时序逻辑 手寻霄s 3 垒当兰鸳s 。 5 l e n2矗1 1 5 2 1 公式( e m p t y , l e n2 ，e m p t y , e m p t y , l e n1 1p r jl e n2 其o e 3 个e m p t y 公式是只成立在一个状态上的终点公式。 4 ) 解释 解释是一个四元组i = ，i ，k ，j ) ，其中。是一个区间，i ，k 为整数，j 为整数 或者仿，并且i k - j s i a l 。 ，i ，l 【，j ) | - p 表示p 被解释在o r 的子区间 上，并且在该子区间上可满足。可满足关系( 1 = ) 归纳定义如下： i p r o p ip p 当且仅当对于原子命题p ，s k i p 】- t r u e i n o t i p 1 p 当且仅当i 毕驴 i o r i | = p v q 当且仅当i l _ p 或者i | - q i n e x t i i - o p 当且仅当k j 并且( a ，i ，k + 1 ，j ) i = p i 一埘i l _ ( p i ，p m ) p r j q ，当且仅当存在整数k = r o sr l s 5r m _ j ，并且( q 0 ，r o ，r 1 ) p p l ，( o ，r n - t ，r n q ，r n ) f p n ，l n 茎m ，对于以下两种情况的o r ， ，0 ，0 ，l a i ) l = q a ) r m q ， 那么公式p 弱等价于公式q ，表示为p * q 。同理，如果i - 口( p - q ) ，那么公式p 强蕴涵q ，标记为p - 2 q 。如果| ：p q ，那么公式p 弱蕴涵q ，标记为p l o 。 如果一个p p t l 公式不含任何时序操作符，称该公式为一个状态公式( s t a t e f o r m u l a ) 。如果公式p z p e m p t y ，称p 为一个终点公式。 命题投影时序逻辑的可判定性 2 1 4 优先级 为了避免过多地使用括号，本文使用以下优先级规则。 11 2 o ，o ，口 3 ，v 4 + 5 9 ，p r j 其中优先级从1 到5 依次递减。 2 1 5 逻辑规则 以下是本文中所用到的p p t l 公式的逻辑规则，其中表示状态公式( s t a t e f o r m u l a ) 。 l l ：口0 0 a q ) gf 1 p a fi q i a ( p v q ) i p v q l 3 ：o ( p v q 、0 1 v o q 1 4 -c ) ( p a q ) o pa o q l s ：r ；0 0 v q ) s 但；p ) v 限；q ) k ：( p v q ) ；r f - - 0 0 ；r ) v ( q ；r ) b ：p e p v oo p l s ： 口p p a o 口p l 9 ：m o r e a - - i o p i m o r e a 0 1 p l l o ：- 1 q p i 0 1 p l n ：o p ；q o ( p9q)l12：卧口；q ) ( p ；q ) l 1 3 ：q p r je m p t y ；q l 1 4 ： e m p t y p r jq ；q l l s ：0 1 ，p 2 ) p r je m p t y p l ；p 2 l 1 6 ：0 0 , e m p t y ) p r jq ! ( p a o e m p t y ) p r jq l 1 7 ： ( p l ，p t , t o a e m p t y , p t + l ，p m ) f h jq 0 0 1 ，p t , t 0 a p t + i ，p m ) 鲥q l 1 8 ：0 1 ，( p i vp i ) ，p m ) p 巧qs 佃l ，p i ，p m ) 两q ) v ( 0 0 1 ， p i ，p 。) p | j q ) l 1 9 ： p l ，p 。) v r j0 0 v q ) ；( 0 1 ，p m ) 鲥p ) v l ，p m ) p r jq ) i a 0 ：0 0 1 ，p 。) p r jo q i 1 a m o r e ；0 0 2 ，p m ) p r j q ) v 0 0 1 a e m p t y ；0 0 2 ， p m ) p 巧q ) l 2 1 ：( o p l ，p 。) p r jo q s o 口l ；( p 2 ，p m ) 两q ) l a 2 ( o a p l ，p 。) 鲥o = a ( p l ，p m ) 埘q 第一二章命题投影时序逻辑 l 2 3 ： ( p l ，p m ) p r j t o a q ； ( p i ，p 。) p l j q 以上所有逻辑规则的证明见参考文献【2 1 。 2 2 p p t l 与p i t l 的比较 p p t l 是同时定义在有穷和无穷区间范围的区间时序逻辑1 2 。而p i t l 仅被定 义在有穷区间范围内【1 1 。虽然在参考文献【7 1 中，p i t l 也被扩展到无穷区间范围内， 但是p i t l 中的时序操作符p r o j 并无法被合理的扩展到无穷区间范围，并且p i t l 中的c h o p 操作符在扩展到无穷区间上后，语义也与p p t l 中的c h o p 操作符不同。 2 2 1c h o p 操作符的区别 在p i t l 中仂，p ；q 可满足当且仅当存在一个区间o ( 有穷或者无穷) ，或者该 区间被从其间某一状态分为两个子区间，p 在前面的子区间可满足，q 在后面的子 区间可满足，或者当。为无穷区间时p 在整个区间上可满足。而在p p t l 中，p ；q 成立，当且仅当存在一个区间o ( 有穷或者无穷) ，该区间被从其问某一状态分为两 个子区间，p 在前面的子区间上可满足，q 在后面的子区间可满足。显然在p p l 吧 中，当p 在整个区间( 无穷) 上可满足时，p ；q 是不可满足的。 虽然在p i t l 和p p r l 中，c h o p 操作符的语义不同，然而它们是可以互相表达 的。如果用抽和d 分别表示p i t l 和p p t l 中的c h o p 操作符，它们可以互表达式如 下： p ；m q i 口；d q ) v p i - l m o r e 口；d q ) z 口 e m p t y ) m q 证明： ( 1 )( o ，i ，k i o i ) i - p ；m q 营存在r k _ _ 2 - , l e n ( 1 ) h h a l t ( x = 2 ) ) 然而，在p p t l 中，如果p l ，p m 中存在终点公式( t e r m i i l a lf o r m u l a ) ，以上的表达 方式将产生在某个状态上x 有不同的赋值的现象。 2 2 3 投影应用实例 例2 1 ：四位串行进位加法器的描述。 图2 4 为四位串行进位加法器的逻辑电路，它由四个一位全加器构成，对于 每个一位全加器，输出0 = n 1 0 n 2 0 c ，c = ( n l o n 2 ) c + n i n 2 图2 4 四位串行进位加法器 四位加法器用来计算两个4 位2 进制数皿1 口= a o a l a 2 a 3 】和k f l = b o ，b l ，b 2 ， b 3 】) 的和。运算从两个数的最低位( 第4 位) a 3 ，b 3 及初始进位值c 4 ( c 4 = 0 ) 开始， 经过一个全加器的运算产生和的最低位值0 3 以及进位c 3 。然后两个数的第三位 a 2 ，b 2 及进位值c 3 经过第二个全加器的运算产生和的第3 位0 2 和进位值c 2 。 该运算过程的状态转换关系如图2 5 示。 兰垒墼丝墅翌壁望塑塑里型丝丝 图2 5 四位加法器运算过程状态迁移图 在该状态迁移图中，状态由变量n i ，n 2 ，c 及两个数组变量n u m l 并f l n u r n 2 h 来定义。其中n u m l 和n u m 2 i 】表示四位二进制数，n i ，n 2 及c 表示一位二进制 数。若两个加数分别为l i 【4 】和k 【4 】，该运算过程可描述为p p r jq ，其中p 表示 l l 【4 】和k 4 】经过4 个一位全加器的运算过程，q 表示l i 4 和l 2 【4 】经过一个加 法器的运算。 p ! 彗l e n ( 4 ) a ( n l = n u m l 【3 】) ( n 2 = n u m 2 3 ) a ( o n l ；n u m l 2 ) a ( o n 2 = n u m 2 2 ) a ( 0 2 n l = n u m l 【1 】) ( 0 2 n 2 2n u m 2 1 ) a ( 0 3 n l = n u m l 0 ) a ( o 珠l z = n u m 2 0 ) a ( m o r e - - , ( o c = ( n t on 2 ) c + n i n 2 ) a 0 4 n 哪! 口= 叫啪l 【o 】。n 啪2 0 0 0 3 c , n u m l 1 o n u m 2 1 0 0 2 c , n u m l 2 1 o n u m 2 2 o o1 c ，n 脚1 【3 】咖叮呲口 3 o c 】 q 管l e n ( 1 ) a c = 0a ( n u m if l = l l 4 ) a ( n u m 2 f l = l 2 4 ) 例2 2 ：四位串行借位减法器的描述。 图2 6 为四位串行借位减法器的逻辑电路，它由四个一位全减器构成对于 每个一位全减器，输出o = n 1 0 n 2 0 c ，c = n 1 。o c ) c + n 2 c 。 图2 6 四位串行借位减法器 一痧苫 善黜 第一章命题投影时序逻辑 四位减法器用来计算两个4 位2 进制数( l l 【】- 【a o ，a l ，a 2 ，a 3 和l 2 【】_ 【b o ，b l ，b 2 ， 岛】) 的差，运算从两个数的最低位( 第4 位) a 3 ，b 3 及初始借位值c 4 ( c 4 = 0 ) 开始，经 过一个全减器的运算产生差的最低位值0 3 和借位值c 3 。然后两个数的第三位a 2 ， b 2 及借位值c 3 经过第二个全减器的运算产生差的第3 位0 2 和借位值c 2 。该运 算过程的状态转换关系如图2 7 示。 n “m 1 0 = l i b i n u m 2 0 b 4 1 图2 7 四位减法器运算过程状态迁移图 n u m l 0 = l l 4 1 。m 2 b 掌b 4 1 若两个被减数和减数分别分别为l l 4 和k 【4 】，该运算过程可描述为pp r jq ， 其中其中p 表示l 1 【4 】和k 【4 】经过4 个一位全减器的运算过程。q 表示l l 【4 】和 k 【4 】经过一个减法器的运算。 p 譬l e n ( 4 ) a ( n l = n u m l 3 ) a ( n 2 = n u m 2 3 ) a ( o n i = n u m l 【2 】) ( o n 2 = n u m 2 2 ) a ( 0 2 n l = n u m l 1 ) a ( 0 2 n 2 = n l l m m 1 ) a ( o n l = n u m l 0 ) a ( o n 2 - n u m 2 0 ) a m o m