《理论计算机科学电子札记》52卷第1期（2001年）网址：http://www.elsevier.nl/locate/entcs/volume52.html11页CTL中时间连接词的适当集艾伦·马丁1;2加拿大渥太华大学数学系摘要一个合适的CTL时间连接词集是逻辑时间连接词的子集，它足以表示所有CTL公式的等价物在本文中，所有这样的充分集的特征。特别地，它表明，CTL的时间连接词的子集是适当的当且仅当它包含一个fAX; EXg，一个fEG; AF; AUg，和EU。除其他外，证明需要分析某类模型，即反应模型。这些模型具有令人满意的特性，即多个连接词变得多余，从而简化了分析。1引言回想一下适当的连接词集合的定义定义1.1一个逻辑的适当的连接词集合是它的连接词的子集S，使得这个逻辑的每个公式都等价于由S生成的子逻辑的某个我们为什么要对适当的集合感兴趣有几个原因。一个是在证明和实现的表达能力和难度之间的权衡例如，用：、^、_和来表达 典 型 的 命 题 句 肯 定 更 容易！ 而不是使用一个单一的足够的连接词，如舍儿笔画（NAND）。但是，如果连接词更少，归纳证明和计算机实现就会更简单因此，有兴趣的是有办法表达公式使用一个更大的一组连接词在一个较小的集合。1 研究部分由NSERC和渥太华大学支持2 电子邮件地址：martin@igs.netc2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。马丁2连接词的适当集合也与由连接词的子集生成的子逻辑的分类问题有关。确定这些中哪些是不同的，直到公式的等价性，等价于描述每个子逻辑的适当的连接词集合。在实践中，通常只需要考虑原始逻辑和它的一些子逻辑。大多数合理的逻辑都有一个替换定理，它指出用任意公式统一替换原子保持有效性和等价性。如果是这种情况，那么一组适当的连接词不仅可以用来表示公式的等价物，而且可以用来表示公式方案的等价物。在本文中，我们特别感兴趣的计算树逻辑，或CTL，分支时间时序逻辑由于克拉克和爱默生[1]。分支时间时序逻辑[4，7]的一些早期工作允许将路径量化器应用于线性时间时序逻辑（LTL）公式。一个非常通用的这样的逻辑是CTL*（见，例如，[6]），具有良好的表达能力，但一个NP完全模型检查问题的逻辑[1]。CTL是作为一种逻辑开发的，它提供了很强的表达能力，但与CTL* 不同的是，它允许一种高效的模型检查算法。CTL已被用作模型检测系统的基础在实践中。模型检查器SMV [9]基于CTL，并且它已被用于验证各种系统的属性，例如IEEE总线架构标准的高速缓存一致性协议（参见[2]）。在本文中，我们将使用BNF定义CTL的公式：：=原子j > j？j：j^J_J ！J AjE**= XJ FJ GjU这里定义了状态公式，同时定义了路径公式。 这种相互递归的定义是从CTL* 导出的，CTL是CTL * 的一个子逻辑;只有状态公式才被认为是CTL公式，但路径公式的使用简化了语义。因此，CTL的时间连接词被认为是路径数量词A和E与情态连接词X、F、G和U的组合。也就是说，有一元连接词fAX;AF;AG;EX;EF;E G g和二元连接词fAU;EU g。CTL的模型M由状态集合S、标记函数L：S！原子，和一个跃迁关系Tran S S，使得对于每一个s2S，都有s 2Ssuchthat（s;s0）2Tran.满足关系j=由状态公式和路径公式的相互递归定义，根据以下规则，其中M是模型，s 2 S，并且=（s 0！s 1！s 2！）是M中的路径：M;s j= A 当且仅当对于M中从s开始的所有路径0，M;0 j=.M;s j= E当且仅当存在一条路径0 在M中，从s开始，使得M;0 j=.M; j=X'当且仅当M;s1j='。M; j=F'当且仅当存在i0，使得M;sij='.马丁3M; j=G'当且仅当对所有i0，M;sij='.M;j= U当且仅当存在i 0使得M; s i j=且对于所有jsu ch使得0jU']（5）EF'E[>U']（6）A['U]：E[：'U（：'^：）]^AF马丁4--1 2 21p我的天啊“s0 ！“s1！“s2！图1.一、模型M证明了S1的不足对于这些和类似等价的证明，见，例如，[6]。给定定理2.1中规定的任何一组联结词S和任何一个对公式“的CTL，我们可以用公式（1）写出AX和EX中的哪一个不出现在S中，就另一个而言。然后，如果EG或AF中的一个出现在S中，则我们可以使用等式（2）和（6）来将EG、AF和AU全部用EU表示，否则，AU出现在S中，我们可以使用等式（2）和（4）将EG和AF写成AU。最后，我们可以使用等式（3）和（5）来用EU表示AG和EF在所有的情况下，我们已经找到了一个公式'0的子逻辑产生的S，这是等价的given为穆拉'。2另一个方向则更加艰难。我们必须证明，任何不满足定理2.1条件的时态联结词集合都是不充分的。由于适当集合的超集是适当的，所以只考虑三组时间连接词就足够了：S1：=CnfAX;EX gS2：=CnfEG;AF;AUgS3：= C n f EUg其中C：=fAX;AF;AG;AU;EX;EF;E G;E U g是所有CTL术语口语连接词的集合。引理2.3项连通性的集合S1：=Cn fAX;EX g不是自等的.证据我们考虑CTL公式EX p和模型M，如图1所示。只有一条路径，=（s 0！s 1！s 2！s 2！），从s 0开始，同样只有一条路径0 =（s！s！s！） 从s开始。我们有M; s0 j= EX p和M;s1 j= EX p。但我们主张，如果'是a，对于不使用AX或EX的公式，则M;s0j=“i fandon l yi fM;s1j=”，soinparticular“不能等价于EX p。这将表明S1不是一个充分集.我们将通过结构归纳法来证明这一主张。 我们可以通过等价式（1）{（6）来假设，其中仅使用时间连接词EG和EU。基本情况是如果'是一个原子，>，或？。在这种情况下，声明是显而易见的，因为s0和s1被相同地标记。马丁5如果'有一个命题连接词作为它的主要连接词，那么这个主张从归纳假设中平凡地得出。马丁6s0s0s00J0101我的天啊#s3 #s2-#s1-#s0-p“！“！“！“！“啊！3 “啊！2“啊！1图二、模型M证明了S2的不足如果'=EG，则M;s0j='当且仅当M;sij=for i2f0;1;2 g，并且M;s1j='当且仅当M;sij=for i2f1;2 g。 但根据归纳假设，M; s 0 j=当且仅当M;s1 j=;，因此我们可以得出结论：M;s0j='当且仅当M;s1j='。如果'=E[ U0]，则M;s j='当且仅当存在i0这样M;ij=0，对于所有j，0j< i，M;j= . (Here我 表示第i状态 ，从零开始编号。） 使用归纳假设，0 每个在s和s处具有相同的真值。我们考虑的情况：如果i 2，然后M; s0j=0，如果我2，则M;sj=M; s2j=0的情况。其中的Each意味着M;s0 j='，所以我们可以得出结论， j='如果并且只有在这些条件之一成立的情况下。我们可以做一个类似的案例分析且M;s1j='当且仅当M;s1j=0或M;sj=M; s 2 j=. 但是再次使用归纳假设，0条件是等价的，所以我们再次得出结论，M; s 0j='当且仅当M;s1j='。 这就完成了归纳。2我们已经看到了证明集合S是不充分的所需的第一种技术：为mula'找到一个CTL，其中该CTL不等于由S生成的子逻辑中的任何公式。然后，对于任何给定的CTL公式，具有来自S的时间连接词，nd两个状态（在相同或不同的模型中），使得'在一个为真，在另一个为假，但在 两 个 都 具有相同的真值。（Lamport使用了类似的技术[7]。马丁7我我引理2.4项连接的集合S2：=Cn fEG;AF;AU g是不充分的。证据 在这种情况下，我们将考虑一个在夜间模型M。它的状态是si对于i和s对于i 0。所有状态都标记为;，除了s这是标记为FPG。有从si到s一期+1，从s0到s一期+1，从s0 到s0 对于i<0，从s到s。该模型的部分如图2所示。ii 0 0有一条从任何状态si开始的唯一路径，它最终到达 s 0 which satis esp. 所以我0，M; si j= AF p。 但是从任何一个状态s0，有许多路径可能保持在s0 一段时间以来我我马丁8我我我我我我我我'我我'我我我我'我但最终过渡到si+1并继续到s0，以及常数路径在s0处剩余在…之前。后一条路径不满足Fp，所以对于所有i0，M;s0 j=AFp. 但我们主张，对于任何一个不使用EG、AF或AU的公式，都不存在在所有状态下具有相同真值的任何一个子集s和s0关于in'，所以特别是不能等价于AF p。这证明S2不是一个充分集再一次用结构归纳法对“。 我们可以假设，使用等价式（1）{（6），that '仅使用时间连接词EX和EU。 基本情况，其中'是原子，>，或？，是微不足道的。 如果'的主连接符是比例连接符，则我们可以将n'设为该连接符的操作数的n个值的最小值，并且该权利要求显然成立。如果'=EX，令n'：=n1. Forin'，M;sij='当且仅当M; sj=，且M;s0 j='当且仅当M;s0 j=或M; sj= 0。i+1i ii+1但根据归纳假说，在si和s上有恒定的真值0对于in，in'意味着i+ 1n。因此，我们可以得出结论，si上的相同真值这个说法成立。S0 对于in作为在siS0 对于in得双曲正弦值.如果'= E[U0]，然后通过归纳假设，有一个不变的真理si上的值S0因为我n得双曲正弦值.0 在sS0因为我n0的情况。让我们：= min（n; n0）。 如果0 在美国，S0为“是的，”他说。否则，我们可以假设0在所有这些状态下都是假的，因为它在这些状态上有一个恒定的真值在这种情况下，我们认为. 如果在状态Si处为假，S0 对于in，那么，这个说法成立。 所以我们也可以假设在所有这些国家都是如此。如果任何一个州，或s0 因satis es'，那么从那个状态的路径满足U0 必须经过n'+1，我们必须有M; sn+1j='。但每个州都是或s0 关于in'具有到% sn'+1 沿着每一个状态满足;那么所有这些状态都满足。所以要么所有这些状态或者都不满足，无论哪种情况，结论都成立。这就完成了归纳。2这一次，我们需要一个稍微不同的方法。 对于任何固定的nite n，每个CTL公式在至多n个状态的模型上等价于只使用下一次连接词AX和EX的某个公式。(This可以使用xed点技术来显示;例如，参见[6]。因此，当证明一组包含AX或EX的时间连接词是不充分的时，有必要考虑任意大的模型。（同样，类似的技术在[7]中使用。要证明S3是不够的，我们将使用我们已经看到的两种技术.但首先我们需要一些关于反应模型的结果。'马丁93 Reexive模型定义3.1模型M是自反的，如果它的转移关系是自反的，即，如果在每个状态上存在循环。马丁10R rr由于各种原因，对反应模型感兴趣。在模态逻辑中，反应性对应于一个有意义的公理，而在计算模型中，反应性对应于允许空转。但是我们对这个性质的兴趣仅仅在于，它将消除证明S3不是一个充分集所涉及的许多困难。当考虑模型的一个子类时，很自然地会询问相对于这个子类的等价性（和有效性）。由于等价意味着在所有模型中具有相等的真值，因此较小类别的模型产生较粗糙的等价关系。定义3.2设和为CTL公式。设对所有自反模型M和M的状态s，M;sj ='当且仅当M; sj ='.然后我们会说'和在reexive模型上是等价的，我们会写'r。像往常一样，有一个替代定理：定理3.3如果' '0，0，且p是任何原子，则'[=p]'0[0=p]。命题3.4下列等价性在自反模型上成立，其中'和'是任意CTL公式：(7)EG'r'(8)AF'r'（9）A['U]r证据设M是一个自反模型，s是M中的一个状态。则M; sj = A['U]当且仅当对于每一条从s开始的路，M; j='U。特别地，在s处的常数路径（由于M是自反的，所以它必须存在）满足： 如果M; sj=，则显然M; sj=A[U]。所以我们证明了（9）。其他案件也是类似的。2我们已经证明了连接词EG、AF和AU在反应模型上是冗余的。这将使证明S3不是一个适当的集合的工作容易得多。另一方面，连接词AG、EF和EU在任意模M及其自反闭包M0上的行为完全相同（其中h具有与M相同的状态）。 也就是说，任何仅使用这三个时间连接词的CTL公式在M和M0的相应状态上具有相同的真值。 这可以通过归纳法来证明;基础案例和案例AG和EF是显而易见的。欧盟的情况更有趣。设和在M和M0的相应态上具有相同的真值. 显然，对于M中的一条ny路，M; j='U当且仅当M0; j='U。如果为0，则可以进行比较 i是M 0中的一个pathi满足“U”，通过从0 直到第一状态满足 .这给出了M中的nite路径，因为M0的所有非loop边 是M的边，它可以马丁11RR0我显然，M; sj=E[pUq]和M0;s0 j=E[pUq]对于所有i0。的确，K可以任意扩展到一个不动点路径。很明显，我们有M;j= U。使用E的满意度定义，EU的归纳步骤如下。引理3.5时间连接词的集合S3：= Cn fEUg是不充分的。证据我们将考虑公式E[p U q]。假设'是一个不使用连接词EU的任意公式;我们想证明它不等价于E[p U q]。这将表明S3不是一个适当的集合，从而完成定理2.1的证明。我们可以假设，使用我们前面的等价式（1）{（6），“只使用连接词EX，EF和AU。(We我们不能用等价（5）来消除EF，因为它会给我们留下EU，我们也不能用等价（6）用另一个连接词来代替AU。）现在利用等价式（9）和定理3.3，我们可以用AU的第二个操作数代替AU在'中的每一次出现，从而仅用连接词EX和EF与' ' 0得到公式' 0。我们可以进一步假设，在反应模型中，具有主联结词EF的'0的子公式都不等价于？，不失一般性，因为我们可以用？但仍有“0”。设“;”;：“为”0“的子公式 主要联系人EF。1 2m根据假设，它们都不等于？在反应模型中，设M i是一个反应模型，ti是模型状态，满足Mi;tij=“i"，1. 现在我们将定义新的exive模型M和M0 如下：M将由M i的状态的不相交的并集组成，以及对于0 i m的状态ri和对于i 0的状态si。 来自Mi的 状 态 的 标 记 将保持不变，状态r i的标记将为;，并且状态s i的标记将为fpg。M i的跃迁将被保留，并且对于1 i，也将存在从ri到ti的跃迁m，从s i到s i+1 对于i< 0，从s 0到r i，对于0 i m，以及从每个状态到其自身。该模型如图3所示。M0 将与M相同，其状态不同by素数，除了r0的标记 将是fq g。我我在前一种情况下，从si开始的每条路径要么必须保持在sj之间，要么最终达到其中一个rj，在任何一种情况下，它都不满足p U q。在后一case，路径s0 ！s0！！s0！r10的！r10的！从s0开始萨蒂什p Uq。i i+1我但我们认为，对于一个为0的ny子模，存在n0个such的在所有状态siS0与in. 我们再次使用归纳法。原子的基本情况，>，或？是微不足道的。 同样，在引理2.4的证明中，如果有一个命题主连接词，我们可以取n为这个连接词的操作数的n个值中的最小值。所以只剩下暂时的情况了。如果= EF0，然后===对于一些K。 在这种情况下，M; tkj=和马丁12KKKM0;t0 j=0。但这意味着有状态s和s0 可从t而t0 特别是M; sj=0 M0;S0 j=0。但由于建筑业，马丁13--数量“啊！R1我的天啊数量“啊！t1M数量不...“啊！“啊！.“啊！R2“啊！t2MS1s0。.2..数量“啊！r10的#“！Rm.#“！tmM图3.第三章。模型M证明了S3的不足-1M马丁14我R rr任何i0，t k是从s i通过路径s i可达的！s i+1！！s 0！r k！t k，所以通过连接路径，s可以从s中读取;类似地，s0 可以从s0。所以M; sj=和M0;s0j= 据我所0;所以我们可以取n：= 0，我我我索赔得到满足。最后，我们得到了case = EX0。 但是这种情况与引理2.4的证明中的EX情况相似，并且同样的论点成立。这就完成了归纳。由于我们的模型M和M0是可重构的，我们可以得出结论， 6E[pU q]。由于是一个等价关系，这意味着'6 E[p U q];更有必要，' 6 E[p Uq]。2这样，我们就完成了定理2.1的证明。Laroussinie [8]给出了引理3.5的一个更直接的证明，只使用了一个CTL模型，而没有使用反应模型的结果。这里给出的证明是作者独立发展的4其他问题我们的特点是适当的时间连接词的CTL集。我们该何去何从？有几种可能性。描述由连接词子集生成的子逻辑。我们已经确定了时间连接词集合C中适合CTL的子集，但是由不适合CTL的子集生成的子逻辑呢？其中一些在表达能力方面是等同的，另一些则不是。等价式（1）{（6），连同定理2.1，马丁15对描述这些子逻辑有很大帮助关键的事实是，如果S;S0 C是生成等价子逻辑的两个连通集，则S[S00S0 [S00为n y S 00生成等价nt子逻辑 C. 这意味着由CTL本身组成的非等价子逻辑对与引理2.3，2.4和3.5的不充分集合一起诱导出由更小的连接集合生成的额外的非等价子逻辑对。然而，仍然有一些更多的工作要做，特别是要确定S和S [fAUg]是否可以生成包含EG或AF但不包含EU的S的非等价子逻辑。考虑其他类型的子逻辑。还 有一 个问 题是 ， 子逻 辑不 是由 连接 的子 集 生成 的。 例 如，Etessami和Wilke在[3]中对这个问题进行了研究，其中LTL的子逻辑通过限制某些连接词的嵌套深度来定义。定义这样的子逻辑的可能性似乎是无穷无尽的。其中一些逻辑本身就很有趣，如[3]，而且是否可以系统地处理这些子逻辑也可能是一个有趣的问题。考虑时态逻辑和线性逻辑的组合。另一种可能性是考虑改变基本逻辑的效果，特别是使用Girard的线性逻辑[5]代替经典逻辑。类似CTL的语义可以使用树来定义，树的节点用线性逻辑的模型（例如相空间）来标记。表达能力和足够的连接词子集的问题也适用于这种情况，考虑到线性逻辑的独特属性，如资源敏感性，这可能是一个有趣的问题。引用[1] Clarke，E. M.，和E. A.李文生，应用分支时间时序逻辑设计与合成同步框架 ， \Logics of Programs Workshop ， ”Lecture Notes in ComputerScience131， Springer Verlag，1981，52{71.[2] Clarke，E. M.，O. Grumberg 和D. A. Peled ，\Model Checking ，”The MITPress，Cambridge，Massachusetts，1999.[3] Etessami，K.，和T. Wilke，An until hierarchy and other applications of anEF game for temporal logic，preprint，1998，26页。[4] Gabbay，D.，A. Pnueli等人，公平性的时间分析，第七届ACM程序设计语言原理研讨会，1980.[5] Girard，J.-是的，线性逻辑，理论计算机科学50（1987），1{102。[6] Huth，M.，和M. Ryan，\Logic in Computer Science：Modeling and Reasoningabout Systems，”Cambridge University Press，Cambridge，UK，2000，387pp.相关网站http://www.cs.bham.ac.uk/research/lics/。马丁16[7] 兰波特湖，有时候”是有时\否从来没有。” 月7 1980年ACM程序设计语言原理年会。[8] Laroussinie，F.，关于CTL组合子的表达能力，信息处理快报54（1995），343{345.[9] McMillan，K. L.，\Symbolic Model Checking：An Approach to the StateExplosion Problem，”Kluwer Academic Publishers，1993.
我的内容管理
展开
