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

摘要 摘要 本文在研究了命题投影时序逻辑p p t l ( p r o p o s i t i o n a lp r o i e c t i o nt e m p o r a ll o g i 曲 的语义和语法的基础上，详细阐述了它的判定过程和表达性。首先介绍了命题投 影时序逻辑，包括基本的语法、语义和一些派生公式及常用逻辑等式，该逻辑除 了包含有常用的逻辑操作符v ( 或) 和一( 非) 外，还包含了两个时序操作符o ( n e x o 和 埘( 投影操作符) 。其次，本文定义了命题投影时序逻辑公式的正则形( n o r m a lf o r m ) ， 根据公式的结构采用归纳的方法证明了任意p p t l 公式都可以转换为正则形定理 的正确性并且给出了相应的转换算法。该算法将所有逻辑公式都归结为一种统一 的形式，这是采用t a b l e a u 方法进行判定的前提和基础。再次，为了找到给定公 式的模型，本文介绍了正则图( n o r m a l f o r m g r a p h ) 的概念，给出了为p 盯l 公式构 造正则图的算法和命题投影时序逻辑的判定过程，该方法简单实用。最后，本文 介绍和比较了区问时序逻辑中两个版本的投影结构并研究了这两个投影结构的表 达性，结果表明嘶投影结构比原始的投影结构p r o 的表达性更强。 关键词：投影时序逻辑正则形正则图判定过程投影结构 a b s t r a dm a b s t r a c t t h i st h e s i si n v e s t i g a t e st 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 i t yo f p r o p o s i t i o n a le r o j e c t i o nt e m p o r a ll o g i c ( p p t l ) a n di t se x p r e s s i v e n e s s w i t h i nt h i s l o g i c ，b e s i d e st h eu s u a ll o g i cc o n n e c t i v e s ，t w ob a s i ct e m p o r a lo p e r a t o r s ，o a n dp r ia r e i n t r o d u c e d an o r m a lf o r mo fp mi sf o r m a l i z e da n dap r o o ff o rt r a n s f o r m i n ga f o r m u l ao fp p t li n t ot h en o r m a lf o r mi sg i v e nb yi n d u c t i o no nt h es t r u c t u r eo f f o r m u l a si nd e t a i l s a na l g o r i t h mt r a n s f o r m i n gaf o r m u l ai n t ot h en o r m a lf o r mi s p r e s e n t e d t of i n do u tam o d e lf o rag i v e nf o r m u l a ，t h en o t a t i o no fn o r m a lf o r mg r a p h ( n f g ) a n da na l g o r i t h mc o n s t r u c t i n gn f g f o r t h ef o r m u l aa r ei n t r o d u c e d ad e c i s i o n p 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 i t yo fp m f o r m u l a sw i t hf i n i t em o d e l si s d e m o n s t r a t e da n ds o m ee x a m p l e sa r eg i v e nt oi l l u s t r a t eh o wt h ea l g o r i t h m sw o r k t w o v e f s i o n so fp r o j e c t i o nc o n s t r u c t si ni n t e r v a lt e m p o r a ll o g i ca r ep r e s e n t e da n d c o m p a r e d f u r t h e r , t h ee x p r e s s i v e n e s so ft w oc o n s t r u c t si si n v e s t i g a t e d k e y w o r d ：p r o j e c t i o nt e m p o r a ll o g i c n o r m a lf o r mn o r m a lf o r mg r a p h d e c i s i o np r o c e d u r e p r o j e c t i o nc o n s t r u c t s 独创性( 或创新性) 声明 本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研 究成果。尽我所知，除了文中特别加以标注和致谢中所罗列的内容以外，论文中 不包含其他人已经发表或撰写过的研究成果；也不包含为获得西安电子科技大学 或其它教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所 做的任何贡献均已在论文中做了明确的说明并表示了谢意。 申请学位论文与资料若有不实之处，本人承担一切相关责任。 本人签名： 。毯豳 日期边z ： 关于论文使用授权的说明 本人完全了解西安电子科技大学有关保留和使用学位论文的规定，即：研究 生在校攻读学位期间论文工作的知识产权单位属西安电子科技大学。本人保证毕 业离校后，发表论文或使用论文工作成果时署名单位仍然为西安电子科技大学。 学校有权保留送交论文的复印件，允许查阅和借阅论文；学校可以公布论文的全 部或部分内容，可以允许采用影印、缩印或其它复制手段保存论文。( 保密的论文 在解密后遵守此规定) 本学位论文属于保密在一年解密后适用本授权书。 本人签名：鲻豳日期团厶 导师签名： 第一章绪论 第一章绪论 1 1 引言 模态逻辑最初是描述必然和可能这两个概念的一种逻辑。自从1 9 7 7 年 p n u e l i 将模态逻辑用以描述程序性质【2 l 以来，这方面的研究有了很大的进展。一 方面我们可以方便地用模态逻辑描述程序的性质，另一方面随着计算机理论与技 术的进步，以模态逻辑作为性质描述和模型检测作为验证手段的研究和应用得到 了发展和重视。最简单的模态逻辑由命题符号和模态算子以及平常使用的逻辑联 接符：或、与、否等构成。基本的模态算子是必然算子，记作口。可能算子是口 的对偶算子，记作o 。这种逻辑可在可能世界作语义解释。由不同的公理，可以定 义不同的模态逻辑系统。将一个结构中的可达关系解释为时间的先后次序关系， 则描述这类结构的模态逻辑称为时序逻辑。 1 2 时序逻辑 逻辑的用途就在于能区分逻辑公式的成立和不成立。从计算机程序运行的角 度，可能世界就是运行状态。可能世界中的可达关系就是计算机程序运行过程中 状态的迁移关系。如果我们只讨论程序的一次运行，则程序运行过程中状态的迁 移关系是确定的，即任何状态的后续状态是唯一的。时序逻辑是人们长期以来研 究的模念逻辑的一个分支。自从1 9 5 7 年p r i o r l 3 】第一个给出了o 和口的时序解释以 来，不同的时序逻辑程序系统应运而生，关于这些方面的发展情况请参见文献1 4 】， 需要注意的是在这些研究中时序逻辑通常被称为时念逻辑。 时序逻辑的版本层出不穷，而我们最感兴趣的是离散和线性时间结构上的时 序逻辑。1 9 6 5 年，v w r i g h t l 5 l 提出了一种具有二元操作符“a n dn e x t ”的逻辑；随 后他又介绍了另一个带有二元操作符“a n dt h e n ”的逻辑；1 9 6 7 年，v w r j i 曲t 合 并了这两种逻辑，从而产生了具有时序操作符c ( a l w a y s ) 和。佃e x t ) 的逻辑【6 】；同 年，p r i o r l 7 第一个给出了一个完整的形式化系统，这一系统可用于验证数字计算 机的工作状态是否正常；1 9 6 8 年，k a m p i 驯介绍了一个新的二元操作符“u n t i l ”， 关于这一操作符和其对偶操作符“s i n c e ”的完整公理系统请参考文献【9 】。 时序逻辑一直用于程序特性的验证方面。1 9 7 4 年，b u r s t a l l l ”j 首先给出了如 何将模态操作符口和o 应用于程序验证的抽象方法，并且在1 9 7 7 年由p e n u l i l l l l 对 这一思想进行了详细的阐述；1 9 7 5 年，k r o g e r 则提出了一个不同的验证方法，该 2 命题投影时序逻辑的判定性和表达性 方法是通过使用操作符“a n dt h e n ”模拟串行程序中的顺序语句和循环语句来验证 程序特性的：1 9 7 8 年，k r o g c r 又将操作符o ，口和o 同时应用于串行程序的验证 领域；第二年p n u e l i l l 2 】将其应用到了并发程序中并给出了一个有限的证明系统。 自从p n u e l i 和k r o g e r 提出将时序逻辑应用于程序验证中后，该研究领域涌现出了 大量的时序逻辑版本，如m a n n a 和p n u e l i 提出的线性时序逻辑( l i n e a rt e m p o r a l l o g i c ，l t l ) ，k a r p l l 3 】提出的分支时序逻辑( b r a i l c h t e m p o r a ll o g i c ，如e r e ) ，还有 l a m p o r t 1 4 1 提出的基于活动的时序逻辑( t e m p o m ll o g i c o f a c t i o n s ，t l a ) 等。所有的 这些逻辑都是基于线性的离散点的，而我们所感兴趣的则是由m o s z k o w s k i 在1 9 8 3 年提出的区间时序逻辑【1 5 j 。区间时序逻辑是基于时间区间而不是时间点，它有一 个特殊的操作符c h o p ( ：1 。 基于c h o p 操作符( ：) 的逻辑有许多，我们统称它们为c h o p p y 逻辑。c h o p 操作 符与传统的操作符口和。不同，一个公式p ；q 在一个模型上是可满足的当且仅当 该模型可以被分成两部分，其中第一部分可以满足公式p ，而第二部分则满足公 式q 。c h o p 作为时序操作符首先是由h a r e l 、k o z e n 和p a r i k h 圳提出的，而更详细 的说明和使用则是由c h a n d r a 、h a l p e m 、m e y e r 和p a r i k h p q 来完成，且h a l p e m 、 m a n n a 和m o s z k o w s k i 还将c h o p 结构应用于基于时间的数字硬件的推理【3 8 j 中。后 来，m o s z k o w s k i 提出了一种基于c h o p ( ；) 、c h o ps t a r 、0 和投影操作符p r o j 的逻辑， 而这一线性时序逻辑就被称为区间时序逻辑【1 6 i ( i n t e r v a lt e m p o r a ll o g i c ，i t l ) ，它 是一个基于有穷模型的c h o p p y 逻辑。 区间时序逻辑是一个强有力的时序逻辑系统，因为它包含的基本时序操作符 是n e x t ( c ) ) 、c h o p ( ：) 和投影操作符p r o j ，这使它比一般线性时序逻辑具有更强的 表达能力。i t l 的一个子集已经被开发成一个时序逻辑程序设计语言称为 t e m p u r a l l 6 1 。该语言的优点是它的语言结构和编程风格与c 十分相似但其功能更 加强大，因为它包含并行操作语句。i t l 和t e m p u r a 已经在并发程序、实时系统 和混合系统的形式描述和验证方面得到了广泛的应用【蛉矧。区问时序逻辑是一个 基于区间而不是离散时间点的逻辑，它具有很强的表达性并且也是一个有用的程 序验证工具。因此，一些研究者将r r l 扩展到了混合系统中，如z h o u 、h o a r e 和 r a v n l 3 8 】为混合系统提出了一个实时逻辑即d u r a t i o nc a l c u l u s ( d c ) ；d u a n 、 h o l c o m b e 和b e l l 为混合系统提出了一个混合投影时序逻辑( h y b r i dp r o j e c t i o n t e m p o r a ll o g i c , h p t l ) 孤2 1 l ；以及出现的投影时序逻辑【1 9 , 2 5 l ( p r o j e c t i o nt e m p o r a l l o g i c ，v i i ) 和实时逻辑( r e a l t i m el o g i c ) 等。本文主要研究的是投影时序逻辑。 投影时序逻辑( p r o j e c t i o nt e m p o r a ll o g i c ，r , r l ) 是对区问时序逻辑的扩展，它 增加了新的投影操作( p l ，p m ) 两q ，这一投影操作符可以作为并行计算和i t l 中投影计算的复合，避免了因使用并行操作符在共用状态变量时可能相互影响的 情况。 第一章绪论 3 投影时序逻辑对于非规范知识的建模和处理是十分有用的。首先，我们可以 利用投影时序逻辑系统对时变数据和时空数据f 如音频、视频数据) 进行形式描述 和语义推理。基于投影时序逻辑的程序设计语言，能够支持对时变数据和时空数 据进行相关的运算，如压缩、合成、还原，还能够对时变和时空数据进行语义推 理。其次，生物系统可以被看作是一个复杂的、并行的通信与合作进程的集合， 这些进程的集合具有复杂的层次关系1 2 1 1 。对这些不同层次系统进行建模的尝试已 经证明了：正在运行中的进程基本上可以看作是成千上万的离散系统和连续系统 的混合( 例如化学反应方程( c h e m i c a lr a t ee q u a t i o n ) ) 。于是可以把这些生物系统看 作是混合系统( h y b r i ds y s t e m ) 。投影时序逻辑不但可以用来很好的对混合系统进 行建模和推理1 1 9 2 0 , 2 2 , 2 7 , 2 8 , 2 9 1 ，而且能够用来对生物系统进行描述和推理【2 l 】。 投影时序逻辑在实时和混合系统，特别是安全危急系统和嵌入式系统的形式 描述和验证方面也是极其有用的，例如，载人航天系统是一个复杂的混合实时系 统，为了保证系统的安全性和可靠性，传统的测试方法远远不能满足要求，采用 形式化的验证技术是十分有用的。因此，把投影时序逻辑应用于该领域将是十分 必要的。 综上所述，研究投影时序逻辑是十分有意义的 1 3 相关工作 在c h o p p y 逻辑中，一些c h o p p y 逻辑的判定过程和公理系统曾被研究。1 9 8 3 年p a e c h 提出了一种基于有穷区间的完整的g e n t z e n 型证明系统，它使用了c h o p 、 c h o ps t a r 和u n l e s s 时序操作符1 3 ”。1 9 8 6 年r o s n e r 和p n u e l i 给出了包含有c h o p 、 n e x t 和u n t i l 操作符的命题c h o p p y 逻辑的公理系统、基于t a b l e a u 的判定过程和完 整的证明系缭i 。1 9 8 8 年d u t e r t r e 则为一种带有c h o p 和n e x t 时序操作符且基于 有穷区间的一阶c h o p p y 逻辑构建了两个完整的证明系统 4 0 l 。1 9 9 5 年w a n gh a n p i n 和x uq i w e n 将这一逻辑扩展到了无穷区间中【4 “。 ，一 h a l p e r n 和m o s z k o w s k i 证明了基于有穷模型的无量词命题区间时序逻辑 ( q u a n t i f i e r - f r e ep r o p o s i t i o n a l lq p i t l ) 的判定性。k o n o 则为带有投影结构的 q p i t l 提出了基于t a b l e a u x 的判定过程1 3 3 j ，可是，该判定过程没有给出形式化证 明且也没有考虑所有的模型，因此，b o w m a n 和t h o m p s o n 是第一个为带有投影 结构且基于有穷模型的q p l t l 提出基于t a b l e a u x 的判定过程l ，后来，他们又给 出了该逻辑公理系统的完整证明1 ”j 。m o s z k o w s k i 为基于有穷模型的命题i t l 和 一阶i t l 提出了完整的公理系统，但是对于命题区间时序逻辑的公理系统证明过 程来说，给出的仅仅只是一个框架，虽然1 9 9 9 年这一公理系统被扩展到无穷区间 中，并且添加了投影结构1 4 2 i ，但是直到2 0 0 0 年，m o s z k o w s k i 才形式化的给出了 4 命题投影时序逻辑的判定性和表达性 基于无穷区间的i t l 的完整公理系统【州。2 0 0 4 年，g o m e z 和b o w m a n 在区间时 序逻辑和w s i s ( t h ew e a km o n a d i cs e c o n do r d e rt h e o r yo fo n es u c c e s s o r ) 之间建立 了映射关系，然后通过使用m o n a 来给出区间时序逻辑的判定过程【4 6 1 。 1 4 论文的研究意义和目的 本文之所以研究投影时序逻辑p r l j e 要是有以下几个原因：第一、扩展的 t e m p u m 语言已经形成【2 3 】：第二、区间时序逻辑i t l 中包含的许多有趣而且有用的 时序操作符也出现在p t l 中。事实上，使用时序操作符是很容易推导出程序设计语 言中的结构，如赋值语句、条件语句和循环语句等，这也就使得使用同一概念来 进行抽象的描述和具体的执行成为可能。第三、投影时序逻辑提供了一个简单的 实时模型，在这一模型中，从一个状态到另一个相邻状态所用的时间就是一个单 位时问。因此，时序可以通过测量区间的长度来获得。第四、将投影结构应用在 混合系统中【冽是非常有用的，而且我们可以将p l 、p m 看作是密集区间( 区间 上相邻状态之间的间隔相对来说比较小) 上的公式，而q 则是由那些密集区间的端 点组成的离散区间( 区间上相邻状态之间的间隔相对来说比较大) 上可以满足的 公式1 2 0 , 2 1 3 0 l ，例如采用投影结构形式化自动调温器、猫捉老鼠的情况和一个煤气火 炉的状态等【2 0 1 。 投影操作符的另一个重要的应用就是能够推导出其他的时序操作符。c h o p 操 作符( ；) 是n l 中的一个中心操作符，它可以用盯l 中的投影操作符( p r j ) 来表示。p ；q 的意思是它可以被满足当且仅当满足它的区间可以被分成两部分，p 可以在第一部 分被满足，q 可以在第二部分被满足。因此有p ；q 一( p ，q ) p r je m p t y ，其中；的定义 见2 3 节；c h o ps t a r 操作符( t ) 1 3 1 】也可以用投影操作符p 巧来定义。如果一个区间可以 被分成有限个部分并且p 可以在任一个子区间上被满足则p 可以在该区间上被满 足，也就是说如果矿可以在一个区间上被满足当且仅当存在一个正整数m 使得公式 ( p 1 p 。) p r ie m p t y 也可以在该区间上被满足，其中p l 一z p 。一p ；程序语言中的 循环结构( 如f o r i 吾句，w h i l e 语句等) 也可以使用投影操作符州推导出来1 2 3 1 ；并行操 作符0 允许并行的过程详细说明他们各自区间的情况，一个比较合适的例子就是描 述典型的多处理器粗粒度的并行性，其中每一个过程都是以各自的速度在执行。 因此，并行操作符可以被定义为p l l o ；( p a ( ( q ，t r u e ) p r je m p t y ) ) v ( q ( ( p , t r u e ) p r j e m p t y ) ) 。 公式的可满足性和有效性是逻辑模型理论的基本问题。而且，在长期用于程 序验证的模型检测方法中可满足性也起着非常重要的作用。可是，在命题投影时 序逻辑( 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 cp p t l ) 中，这一问题并没有被研究。 模型检测的方法是一种基于模型检测算法的自动机方法。在i t l ，e i t l ( e x t e n d e d 第一章绪论 5 i n l e r v a lt e m p o r a ll o g i c ) 和珂l 中，模型检测与逻辑的可满足性是非常相关的，因 此，进一步研究p p t l 公式的可满足性是非常必要的，也是非常重要的。 1 5 论文的主要工作 t a b l e a u 方法已经在标准的时序逻辑中被广泛的研究p 2 j ，而且在区间时序逻 辑中也用到了一些t a b l e a u 方法，如文献 3 3 1 ，其中与我们的研究工作最相近的就 是b o w m a n 和t h o m p s o n 所作的工作【3 4 j 。他们所考虑的工作是基于一个包含了 c h o p 操作符；和类似于原始投影结构的投影操作符p r o j b 的区间时序逻辑的。在他 们的论文中，p p r o j b q 的意思是公式p 可以反复的在一系列的子区间上执行，而 q 则是在由满足p 的区间的端点组成的区问上执行，p 出现的个数由q 的执行长 度来决定，并且p 不可以是一个只在一个点状态上执行的公式。可是，这一限制 却导致这一逻辑失去了灵活性，因为在某些情况下，公式p 必须在一个点状态上 被满足。他们还给出了一个t a b l e a u 算法，但是这一算法却相当的复杂并且不能 够处理新的投影操作符( p ，p m ) p dq 。基于以上原因，本文将就以下问题展开研 究。 假设一个命题投影时序逻辑公式中包含有穷个原子命题，公式的模型也是有 穷的。本文第二章主要介绍了命题投影时序逻辑的语法、语义及其逻辑等式。第 三章中定义了一个正则形( n o r m a lf o r m ，b y ) ，并且证明了任何一个公式都可以转 换为正则形，该证明过程是根据公式的结构进行归纳的，同时也给出了一个相应 的转换算法。为了找到满足给定公式的一个模型，本文第四章引入了正则图 ( n o r m a lf o r mg r a p h ，n f g ) 的概念，介绍了为一个公式构造正则图的算法。从而， 使得命题投影时序逻辑的判定过程转换为判断一个具有有穷模型的给定的公式的 正则图是否存在某一个特殊节点。在这一方法中，所有的公式都可以被重新转换 为一种统一的形式正则形，对于一个给定的公式，一个正则图可以通过它的 正则形来构造，因此，我们并不需要分别考虑不同形式的公式。在构造了n f g 之后，还需要移除多余的和不一致的节点，以便找到给定公式的模型。在没有冗 余节点的n f g 图中，从根节点到一个特殊的终止节点之间的一条路径就对应给定 公式的一个模型。因此终止节点是否在没有冗余节点的n f g 的节点集中成为了该 公式是否是可满足的充要条件。 区问时序逻辑是一种并发系统特性推理的形式化方法。许多年来，一些研究 者一直致力于这个领域并且提出了许多投影结构。典型的两个版本的投影结构是： 由m o s z k o w s k i 提出的原始的投影结构pp r o jq 和由段振华教授提出的投影结构 ( p l ，p ) p dq 。投影结构对于描述和验证并发和混合系统是非常有用的。为了比 较这两个版本的投影结构，使他们的语义更加清晰，我们有必要研究一下这两个 命题投影时序逻辑的判定性和表达性 版本的投影结构的表达性。 两个版本的投影结构在命题逻辑中是无法直接比较的，但是在一阶逻辑中， p r o j 可以由p r j 来定义，而p 巧只有在特殊情况下才可以由p m j 来表示。虽然，p p r o j q 和( p l ，p m ) p r jq 有共同之处，但是在程序设计中他们作为一种执行结构，拥 有许多独立特性。因此，为了更好的比较这两个版本的投影操作符的表达性，在 第五章中投影时序逻辑将被扩展到一阶逻辑中。 第六章总结全文，明确指出本文主要工作及创新点，将来这些工作将会被进 一步完善。 第二章命题投影时序逻辑 第二章命题投影时序逻辑 2 1 语法 命题投影时序逻辑( 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 ) 除了通常 的逻辑操作符或( v ) 和非( 一) 外，还包含两个时序操作符“n e x t ”( o ) 和“p r o j e c t i o n ” ( p i j ) 。 首先，我们以归纳的方式给出命题投影时序逻辑公式的语法。 ( a ) 字母表 p r o p 表示一个原子命题的可数集合。 v ，命题投影时序逻辑中的操作符：，、v 、0 和鲥。 ( b ) 命题投影时序逻辑公式的归纳定义 单个原子命题公式p e p r o p 是命题投影时序逻辑公式。 如果p 1 、p m 、p 、o 是命题投影时序逻辑公式，则，p 、p v q 、o p 、 ( p - ，p m ) p 巧q 也是命题投影时序逻辑公式。 只有有限步应用上面两个条款生成的公式才是命题投影时序逻辑公式。 然后，我们采用b a c k u s n a u r 格式( b n f ) 来精确描述上述的p p t l 公式 ( f o r m u l a s ) 的归纳定义，其中p p r o p ( - - 个命题变元) ： p ：= p i p l p l v p 2 io p i 口l ，p m ) p 巧p( 式2 - 1 ) 公式p 、一p 、p v q 、o m0 1 ，p 2 ) 埘q 都是命题投影时序逻辑公式。如果一个 p p t l 公式不包含任何的时序操作符，则称其为状态公式；否则，称其为时序公 式，如p 、一p 、p v q 都是状态公式，而o p 、( p l ，p 2 ) 鲥q 则是时序公式。在下面的 章节中，简称命题投影时序逻辑公式为公式。 2 2 语义 这一节主要介绍命题投影时序逻辑公式的语义，在此之前，首先给出关于状 态、区问和解释的基本概念。假设z 表示所有整数的集合，n 表示所有正整数的 集合且n 0 表示所有非负整数集合。 2 2 1 状态 根据k r i p k e 结构蜘的定义，- - + 状态( s t a t e ) s 是一个原子命题集p r o p 到布尔 8 命题投影时序逻辑的判定性和表达性 集b = t r u e ，f a l s e 的映射： s ：p r o p - - - - b 而s i p 表示命题变元p 在状态s 上的值。 2 2 2 区间 一个区间。是一个有穷或无穷的非空状态序列。它的长度用l a i 表示，如果该区 间长度是无穷的，则i o f 等于( o ；否则l o i 等于区间上的状态数减l 。为了使下面所介 绍的概念在有穷和无穷区间上都可以使用，方便以后工作的扩展，我们将加入到 非负整数集n 0 中并扩展成如下形式： n m = n o u 0 ) ) 同样，因为= o 谚阳对于所有的i n o ，i 0 ) ，所以可以将比较符号扩展为= 、 、 蔓、! ，其中符号! 定义为s ( ( o ，曲。为了方便描述一些特殊的区间，我们给出简化 的记法：o r 表示一个完整的区间 ，也就是从状态s o 到状态8 h 之间的一系 列有序状态，其中如果区间a 的长度是无穷的，则sb f 是无定义的；类似的，区间 q i j ) ( os j ! j s l 0 1 ) 表示一个从状态s i 到状态s i 之间的子区间 ；区间o ( 0 sk51 0 1 ) 表示的是一个从第k 个状态开始到该区间的端点之间的一段子区问 。 一个有穷区间a 同另一个区间0 7 ( 此区间可空) 的联结记为a o 。区间的联结就 是将两个区间顺序相连组成一个新的区间，且这两个区间之间没有共享状态，如o = 和o = ，贝, l j o o = ，后一个区间可以为空，此 时两个区间的联结等于第一个区间。 为了定义投影操作符的语义，引入区间的一个辅助操作符l 。令o = 是一个区间，r l 、r h 是整数( h 苫1 ) 且0 nr l s sr h - , c i o l ，则d 在r l 、 r h 上的投影( p r o j e c t i o n ) 定义为：a ( r 1 ，r h ) = ，这里t 1 、t t 是从 r 1 、r h 中通过删除所有重复项得到的结果。例如： j , ( o ，0 ，2 ，2 ，2 ，3 ) = 我们称区间a 为被投影区间，而o l ( r 1 ，r h ) 是投影区间。 2 2 3 解释 一个p p l l 公式的解释是一个三元组z = ( o ，k ，j ) ，其中。是一个区间，k 是非负 整数，j 是整数或( o ，且k ! j l o i 。s k 表示当前状态，s i 表示区问的最后一个状态， ( o ，k ，j ) | = p 表示某一公式p 可以在区间。上被解释，而且在子区间 上是可 满足的。p p t l 公式的可满足关系i = 形式化的定义如下： 第二章命题投影时序逻辑 9 z | _ p 当且仅当对于任意原子命题变元p ，s k i p 】= t r u e 。 工| _ ，p 当且仅当z 卜p 。 z | - pv q 当且仅当z i - p 或者2 - l - q 。 z i _ o p 当且仅当k j 且( q k + l ，j ) i i - - p 。 i i _ - ( p l ，p 。) p r j q 当且仅当存在整数k = r 0 r 1 s i - m ：j 使得 r 1 ，r t ) i _ n ( 1sz s m ) ，且对如下的一，有p 7 ，0 ，1 0 7 | ) | - q 。区间o 满足以下两个 条件之一： r m j 且a = a l ( 地，r r a ) 盯( ，m + 1 j ) 。 r m = j 且= 0 1 r ( r o ，r o( 0 sh s m ) 。 为了进一步说明投影结构的语义，图2 1 给出了公式口，p 2 ) 州o 的语义解释。 虽然公式q 和p 。同时开始执行，但是公式p l , p 2 和0 可能在不同的时间点终止。 图中的( a ) 展示了p 。；p 2 在q 完成之前执行完毕，然后q 继续执行直到终止，它们 在t o 、t 2 和“时刻可以进行通信；( b ) 给出的是p 1 ；p 2 和q 在同一个状态同时结束 的情况，可以通信的时刻同( a ) ；( c ) 则是q 在p 1 ；p 2 之前结束，然后p 1 ；p 2 继续执行， 在这种情况下它们只可以在t o 和t 2 时刻进行通信。 笋t 鳞ot 2 藉热 ( c ) 图2 1 ( p l p 2 ) p r io 的语义解释 原始的投影操作符pp r o jq 在【1 6 】中给出了定义，在一阶逻辑中，它可以使 用上面定义的新的投影操作符来表示，但是在命题逻辑中，原始的投影操作符和 新的投影操作符是不可以直接比较的。在原始的投影结构中，公式p 在一系列状 态紧密的子区间上反复执行，而公式o 则是在由上述的子区间的端点所形成的区 间上执行。如果一些p 反复的在长度为0 的区间上执行，则在q 的执行过程中， 同一个全局变量将多次重复出现，而且在p p r o jq 结构中，一系列的p 和q 总是 在同一时刻终止。虽然pp r o jq 承i ( p 1 ，p m ) p r iq 有一些共同的重要特性，但是 在需要考虑不同的时问规模的程序设计环境中，作为有用的补充结构，他们有着 许多各自不同的特性，应该被独立对待。 时序操作符的解释与当前状态息息相关，所谓单位时间仅仅是指时序时间而 区间长度则依赖于动作的多少和持续时间，因此，在实践中，这些公式所表示的 过程可能具有不同的长度。公式解释的一个重大应用就是可以用于证明命题投影 时序逻辑的等式。 例2 1 证明一o p ；0 一p 证明： ( a ，k ，j ) | _ 一o p 如卜_ l 如卜卜 鱼缸霹 挈挚+ ：h o n 缸卜卜如卜卜 1 0 命题投影时序逻辑的判定性和表达性 ( o ，k ，j ) | o p ( o ，k ，j ) | o p 且k j ( o ，k + l ，j ) l p 且k j bk + l ，j ) i - - p 且k j ( o ，k ，j ) | _ o ，p 2 3 联结词的扩充 前面定义了两个时序操作符，现在研究时序操作符可否扩充这类问题。在经 典的命题逻辑中，v 和一构成了全功能联结词，t r u e ，f a l s e 。a ，一和一都可以用这 两个联结词表达，特别是，t r u e 粤f p v ，p 和f a l s e 磐p 一p ，其中p 是任意公式。因 此，对于任意解释2 - ，z | _ t r u e 当且仅当z 卜f a l s e 。进一步，本节将引入一些新的 时序操作符，这些操作符由基本操作符推导出来。有利于简化公式的复杂度，使 公式更直观。 ( a ) 时序公式e m p t y ： e m p t y 的意思是当前状态是区间的最后一个状态，它可以用n e x t 操作符( o ) 和 t r u e 来表示。 e m p t y 磐，o t r u e( 式2 - 2 ) 它的语义形式化的定义为 p ，k ，j ) | - e m p t y 当且仅当k = j 0 ( b ) 时序公式m o r e ： m o r e 的意思是当前状态不是区间的最后一个状态，m o r e 可以表示为e m p t y 的 非。 m o i e 些一e m p t y m o r e 型fo t r u e ( 式2 - 3 ) 它的语义可以形式化的定义为 ( qk ，j ) | _ m o r e 当且仅当k j o ( c ) 时序操作符o ( 读作w e a kn e x t ) ： 如果p 是公式，则o p 也是公式。o ( w e a kn e x t 操作符) 可以用n e x t 操作符( 0 ) 和非操作符( 一) ( 见时序公式e m p t y 的定义) 来定义， o p 型o p v e m p t y( 式2 - 4 ) 它的语义可形式化的定义为 ( o ，k ，j ) 卜= o p 当且仅当( 嘎k ，j ) | _ o p 或者k = j 0 ( d ) 时序操作符o ”( 读作n t h n e x t ) ： 第二章命题投影时序逻辑 儿 如果p 是一个公式，n o ”p 也是一个公式。时序操作符0 8 是n e x t 操作符f o ) 的扩展，可以通过n e x t 操作符来归纳定义， 0 0 p 型p 0 “p 垫f o ( o ”1 p ) ( d n )( 式2 5 ) 它的语义形式化的定义为： ( q k ，j ) j - 0 ”p 当且仅当k + n s j 和( 羁k + n ，j ) j ：p 。 ( e ) 区间长度： 有穷区间的长度( 从当前状态到最后一个状态) 可以用操作符l e n 来描述，l e n 操 作符可以用n t h n e x t 操作符( 0 ”) 来定义， l e n ( n ) 墼f o ”e m p t y ( n n o )( 式2 - 6 ) s k i p 塑q e n ( 1 )( 式2 - 7 ) 时序公式s k i p 代表区间上的单位时间，l e n ( n ) 的语义可以定义为： ( 0 ，k ，j ) f = l e n ( n ) n j i 仅当j 且j k = n ( n 0 ) 。 ( f ) 时序操作符；( 读作c h o p ) ： 公式p ；q 的意思是它可以被满足当且仅当满足它的区间可以被分成两部分，p 可以在第一部分被满足，而q 则可以在第二部分被满足。c h o p 操作符可以用投影 操作符来定义， p ；q 墼f ( p q ) p oe m p t y( 式2 - 8 ) 它的语义可以定义为： ( a ，k ，j ) | - p ；q 当且仅当存在一个整数r 使得k 墨rs j ，( 旺k ，r ) | - p 和( o ，r ，j ) 卜q ( 曲时序操作符( 读作s o m e t i m e s ) ： 如果p 是一个公式，则o p 也是一个公式。它可以用c h o p 操作符( ；) 来表示， p 蝗f t r u e ；p( 式2 - 9 ) 它的语义同样可以形式化的定义为： ，k ，j ) i _ p 当且仅当存在整数r ，使得k 宣r i j 且( o ，r ，j ) | _ p 。 ( h ) 时序操作符口( 读作a l w a y s ) ： 如果p 是一个时序公式，则口p 也是一个时序公式。口操作符可以用o 的双重 否定来定义， 口p d e 2 一一p( 式2 - 1 0 ) 它的语义定义如下： 慨k ，j ) | - 3 p 当且仅当对于所有的整数r ，k 墨r j 使得 r , j ) j _ p 有时，我们采用p ；q 表示i _ - 口( p q ) ，我们称该等式为强等式。p q 表示 公式p 和q 在每一个模型的所有状态上它们都具有相同的真值。如果p ；p a e m p t y ， 则公式p 被称为终点公式( t e r m i n a lf o r m u l a ) 。 命题投影时序逻辑的判定性和表达性 2 4 可满足性和有效性 一个公式的模型可以是一个有穷区间也可以是一个无穷区间。 2 4 1 可满足性和有效性 如果( o ，0 ，l a l ) i _ p ，则称公式p 可以在区间。上被满足，表示为a | _ p 。如果对 于某一o ，ai _ p ，则公式p 被称为是可满足的。如果对于所有的a ，al - p ，则称 公式p 是有效的，表示为i = p 。 2 4 2 特殊模型 假设r 表示一个满足某些特性的模型集合。如果存在一个模型o 承，使得a | _ p ，则公式p 被称为是r 可满足的；如果对于所有的模型o r ，使得okp ，则公 式p 被称为是r 有效的，在这种情况下，可满足关系| _ 可以用i - r 来替换。 根据以上的定义可知，如果公式p 是有效的，则，p 是不可满足的；如果p 不是有效的，则一p 可能是可满足的，但是仅仅是可能；如果，p 是可满足的，则 p 不是有效的。 2 5 优先级 为了避免公式中出现大量的括号，给出如下优先级规则： ( a ) 一 ( b )o 、0 、口 ( c ) 、v ( d ) 一、一 ( e ) 鲥、； 其中( a ) 是最高级，( e ) 是最低级。 通过上面的优先级规则，“一p ) v ( o ( 一q ) ) ) 可以被表示为，p v 0 ，q ，但有时为 了看起来清楚醒目，也可以保留某些原可省去的括号。 2 6 逻辑定理 假设p 、q 、p 1 、p m 和r 都是p ”l 公式，w ( 可能带有下标) 是一个状态 第二章命题投影时序逻辑 公式。下面我们给出一些常用的逻辑定理，关于这些定理的证明在此不再给出， 请参见文献1 2 3 1 。 f d l d ( p q ) se p a n qf d 2 p v q ) ；p v q f d 3 o ( p q ) ；o p o q f d 4 o ( p v q ) io p vo q f d 6 o ( p a q ) ；o p o q f d 7 o 口v q ) ；q p v g q f d 9 ( r ；p v o ) ；限；p ) v ( r ；0 ) f d i o p v q ；r ) ；( p ；r ) v ( q ；r ) f e l o p i p v o o p f e 2口p ；p o d p f m 2m o r e a 一0 p i m o i e a o p f d u l 一o p o - p f d u 2 ，o p ；o pf d u 3 ，o p i 口，p f d u 4 一口p ；o p f c h l o p ；q ；o ( p ；c i ) f c h 2 w a ( p ；q ) ；w a p ；q f e p 2 e m p t y ；pip f e p 5 q ；e m p t yiq a o e m p t y p r j e l e m p t y p 0 q q p r j e 2 q p r je m p t y 。q p r j e 3 ( p 1 ，p ) 州e m p t y5p 1