模计数和群量化器中具有模计数和群量化器的线性时态逻辑的一阶逻辑表达完备性

可在www.sciencedirect.com在线获取理论计算机科学电子笔记278（2011）201-214www.elsevier.com/locate/entcs具有模计数和群量化器A V Sreejith1数学科学研究所，CIT校园，Taramani，印度钦奈摘要坎普证明了线性时态逻辑对于词上的一阶逻辑是表达完备的 我们给出了一个Gabbay式证明，证明了用模计数和群量化器扩展的线性时态逻辑（由Bazira mwa bo，McKenzie，T′erien引入）对于模计数的一阶逻辑是表达式完备的。cou nting （ 由 Straubing 、 T 'erien 、 Thomas 介 绍 ） 和 groupquan ntiers （ 由 Barrington 、 Immerman 、Straubing介绍）。关键词：线性时序逻辑，一阶逻辑，模计数，群量化器1引言Kamp证明了在线性序上，线性时态逻辑LTL（Prior [14]，Pnueli [13]，Gabbay，Pnueli，Shelah和Stavi [5]）对于具有一元谓词的一阶逻辑FO是表达完备的。KampGabbay [6]给出了这一结果的另一个证明，强调了分离性：每个LTL公式都有一个等价公式，可以分离为纯过去、现在和纯未来公式。更精确的定义将在本文后面出现。对于词模型，McNaughton和Papert [15]表明这些逻辑也对应于无星正则语言类。翻译算法不是基本的，从Meyer和Stockmeyer [16]我们知道我们不能做得更好。已经提出了各种扩展，以将时态逻辑在词模型上的表达能力扩展到所有正则语言（ Wolper [18] ， Banieqbal 和 Bar-ringer[1] ， Hodkinson[9] ， Baziramwabo 和McKenzie和T'erien[3]，Henriksen1电子邮件地址：sreejith@imsc.res.in1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.10.016202A.V. Sreejith/电子笔记理论计算机科学278（2011）201和Thiagarajan [8]）。HodkinsonJanin和Walukiewicz（[10]）在分支上下文中的后期工作也通过自动机。Barrington，Immerman和Straubing [2]使用有限幺半群的Krohn-Rhodes de-composition证明，正则语言也可以用FOGRP描述，FO grp是用广义量化器扩展的一阶逻辑，它执行COM。在有限的群体中。这推广了FO模，一阶逻辑扩展为m odulocou n ting ， definedbyyStraubing ， T 'erienandThomas （ [17] ） .Baziramwabo，McKenzie，T′erien[3]利用Krohn-Rhodesdecomposition 给出了一个LTL群计算公式，并将LTL推广为群计算形式.因此，他们还建立了FO组的三变量性质。他们还表明，逻辑LTL模是表达完整的FO模。本文给出了后一个表达式完备性结果的基于Gabbay [6]分离性的证明，证明了LTLGRP和LTLMOD具有分离性.作为技术说明，逻辑LTLGRP和LTLMOD的当前定义使用比[3]和我们自己早期工作（[12]）中更简单的模态。我们还研究了一元时态逻辑UTL（[4]），它是没有Until运算符的LTL。我们扩展 了 Etessami ， Vardi 和 Wilke （ [4] ） 的 技 术 ， 以 表 明 具 有 群 运 算 符 的 UTL（UTLGRP）具有与仅使用两个变量的FOGRP我们工作的动机是进一步推动基于逻辑的方法在我们看来，一个有趣的开放性问题是，人们是否可以第2节提供了LTL和一阶逻辑的语法和语义，其扩展。 第3节给出了我们的主要定理的证明。2预赛2.1线性时序逻辑使用以下语法建立一组命题P上的线性时态逻辑φ：：= p ∈ P |¬ φ |φ1∨ φ2|Xφ |Yφ |Fφ |Pφ |φ1U φ2|公司简介我们用真来表示陈述aa。则Fφ，Pφ可以定义为真Uφ真Sφ。线性时态逻辑（LTL）公式被解释为字符串上的字母表n = 2P，P的所有子集的集合。 我们用下式表示字符串u的第i个字母： u（i）和u的长度，|u|. u中的位置从0编号到|u|-1。我们只考虑有限的词语。给定一个字符串u∈ u+，一个位置i<|u|和线性时序逻辑公式φA.V. Sreejith/电子笔记理论计算机科学278（2011）201203Pr，qr，qr，qr，q在P上，我们记为（u，i）|= φ意味着φ在u中的位置i为真。逻辑的语义如下所（u，i）|=p如果 p∈ u（ i）且 p∈ P（u，i）|=如果不是（u，i）|= φ（u，i）|=φ 1<$φ 2if（u，i）|= φ 1或（u，i）|= φ 2（u，i）|=X φ，如果i<|u|− 1和（u，i +1）|= φ（u，i）|=Y φ if i> 0 and（u，i − 1）|= φ（u，i）|=φ 1U φ 2如果存在j> i且（u，j）|= φ 2且对于所有k，如果i< k< j，则（u，k）|= φ1（u，i）|=φ 1S φ 2，如果存在aj φj−1<$φj我们说一个LTL组（LTL模）公式是一个纯未来公式，如果唯一使用的模态是X，U和未来组运算符（未来模运算符）。类似地，我们说一个LTL组（LTL模）公式是一个纯过去公式，如果唯一使用的模态是Y，S和过去组运算符（过去模运算符）。纯现在公式是那些不使用任何模态的公式。 式FMODP α既不是一个纯粹的过去公式，也不是一个纯粹的现在公式，也不是一个纯粹的未来公式。在这种情况下，我们称这个公式不纯。注意until、since、group和modulo运算符的语义是严格的，也就是说它不依赖于当前位置。我们归纳地定义未来深度（过去深度）。所有纯过去（未来）公式的未来（过去）深度为0。 公式φ1Uφ2，Xφ1，G Fφ1，.，φ k比公式φ 1，.的未来深度的最大值大一，φ k。 类似地，公式φ1Sφ2，Yφ1，G Pφ1，.， φ k is比公式φ1，...， φ k。公式的深度是其未来深度和过去深度的总和。类似地，公式的交替深度是其未来和过去模态的交替次数。2.3一阶模群量化逻辑设A是一个有限的字母表，V是一个有限的变量集。 一个词模型超过（v，V）是一对（u，s），其中u∈v，s：V → {1，.，m}，其中|u|= m。 让我们介绍单词模型的一阶逻辑的语法。我们使用一组有限的变量V ={x1，. }，一个二元谓词和一元谓词a，a ∈n，对于有限字母表n。<α：：= a（x i），a∈ φ |x1 y > x是这样的位置，使得b在y处为真，a在区间（y，z）中的所有位置为真，z满足β。也就是说z是aSb<$β为真的地方。参见图2。观察到（y，z）是满足Sb公式的状态块。我们的想法是得到在这个区间内计算的群值。我们考虑x不满足公式aSb的情况。我们给出的解决方案也可以进行修改，以考虑到这一点设Θ =φ1，...，φ k现在我们给出一个公式g，它在满足b a U β的所有位置上都是真的，并且为a s的块计算群值，直到β是g。g：=b因此，在yi处，g为真，则区间（y，z）中的群值为g。设γ=<$（aUβ）。下面的公式等价于α。G F（γ φ1）g，.， （γ φ k）该公式仅在位置不满足Uβ时计算φis。否则，其中一个数组将计算整个块的组值。（2、3、4）： 设当前点满足公式G P<$γ1，.γ k， I'm sorry.γ kγ和Ggj′πγ1， . ，γkε. 让我们假定gj=gl.gj′。当一个新的点在未来将满足G P<$γ，...，γi it also satisfies G Fγ，.是的。这让我们取代了过去的组操作符与未来的组操作符，反之亦然。参见图3。（5，6，7，8）：这些公式是通过将1，2，3，4中的公式中的过去运算符替换为未来运算符而得到的，反之亦然通过上述相同的论证，我们可以证明这些公式也可以分离。Q引理3.5以下的翻译是等价的。(i) α1S（α2<$α3） α1Sα2α1Sα3(ii) （α1<$α2）Sα3<$ α1Sα3α2Sα3（孟加拉国g = gJgJJ−1 ）¸ GJ X`˛）208A.V. Sreejith/电子笔记理论计算机科学278（2011）201GGGGGG/g=giGiG/g=giGi(iii) <$（aSb）<$（<$bS<$a）<$H<$b（iv）<$G Pφ1，.，φ kφ kG Pφ1，.， φ k(v) α1U（α2<$α3） ≡ α1Uα2α1Uα3(vi) （α1<$α2）Uα3≡ α1Uα3<$α2Uα3(vii) <$（aUb）<$（<$bU<$a）<$G<$b（viii）<$G Fφ1，.，φ kG Fφ1，.， φ k证据很容易看出第四条和第八条陈述是正确的。其余的陈述可以如[6]中所Q引理3.4和引理3.5让我们用嵌套在未来运算符中的过去运算符重写公式。观察到存在对偶引理，其中过去算子被未来算子替换，反之亦然。利用这两个引理，我们给出了一系列引理来证明LTL群中的公式是可分离的。这些引理证明使用归纳的公式的结构引理3.6（i）设a，b是命题公式。设α，β和φ1，...，φ k是唯一模态为Ub的公式。那么αSβ，G P<$φ1，.，φ k可以是分居了（ii）设a，b是命题公式。 设α，β和φ1，...，φ k是公式， 唯一的模态是Sb。那么αUβ，G F<$φ1，.， φ k可以分离。证据 注意，第（ii）次声明是第（i）次声明，过去的模态被未来的模态取代，反之亦然。我们现在证明（i）Gabbay [6]展示了如何分离公式αSβ。因此，让我们考虑公式G P<$φ1，...，φ k 设每个φ i是一个Ub和命题的布尔组合。 重写G Pφ1，...， φ k表示纯Future和纯Past的布尔组合公式，我们重复应用引理3.4中给出的变换，这给了我们一个分离的公式。Q引理3.7（i）设a1，.，a k是命题公式。 设α，β和φ1，...，φk是仅具有模态G F a，...，a. 那么αSβ，G P<$φ，...，φ⟩可以分开。g1kg′1k(ii) 设a1，...，a k是命题公式。设α，β和φ1，...，φ k是仅具有模态G Pa，.的公式，a.那么αUβ，G F<$φ，.，φ可以是愤怒g1kg′1k证据反复应用引理3.4和引理3.5，我们得到一个分离的公式。Q现在我们来看一下一个until情态（since情态）嵌套在一个past情态（future情态）中的公式。引理3.8（i）设a1，…，a n，b1，.，b n是命题公式。设α，β和φ1，...， φk是只有阶数满足n的公式：Ui=aiUbi. ThenαSβ，G Pφ1，.，φ k可以分离。A.V. Sreejith/电子笔记理论计算机科学278（2011）201209GGGGGGGGg′1Kg′1Kg′1K（ii）设a1，...，a n，b1，.，b n是命题公式。设α，β和φ1，...，φ k是仅具有模性的公式，条件是：Si=aiSbi。 ThenαUβ，G Fφ1，.，φ k可以分离。证据我们证明（i），并声称（ii）的证明是类似的。当α=αSβ时，这可以通过Gabbay的参数来分离。 所以设φ = G Pφ1，.，φ k 令{U1，...，U n}是φ i s中使用的 n 个 Until 公 式 。 我 们 首 先 将 Until 替 换 为 mulasU1 ， ... ，Un−1bynewpropoitionsp1，.， pn−1。 我把新的穆拉贝叫做阿玛尼。 由引理3.6我们知道，我们可以找到一个分离的mulaequivalentttoa. 现在我们用u n − 1代替公式中的pn−1，并再次应用引理3.6。注意到当我们分开的时候，我们没有引入任何新的Untils。在n轮之后，我们得到一个分离的公式。Q引理3.9（i）设a1，.，a n，b1，.，b n是命题公式。 设α，β和φ1，...，φ k是仅具有模态G Fa1，.的公式， 是的。然后是αSβ，G Pφ，.，φ可以分离。(ii) 设a1，...，a n，b1，.，b n是命题公式。设α，β和φ1，...，φ k是仅 具有模态GPa，...的公式， a. 那么αUβ，G F<$φ，.， φ φ n can分开g1kg′1k证据 这个证明类似于引理3.8的证明。 在（i）中，我们替换了1，我们重复地将引理3.10应用于嵌套最深的210A.V. Sreejith/电子笔记理论计算机科学278（2011）201⇐过去的模式。在每次应用引理之后，过去模态的深度减少，因此在n步之后，我们得到一个分离的公式。Q现在我们考虑可以将Future模态嵌套在Past模态中的公式。引理3.12设α是一个公式，使得没有过去（未来）模态嵌套在未来（过去）模态中。 那么α可以被分离。证据 证明是通过归纳未来（过去）模态的深度n。n= 1由引理3.11证明。当n >1时，我们用新命题pi替换未来（过去）深度≥2的所有未来（过去）模态。设m ula的结式为eα。我们观察到，α的Future（Past）深度为1，因此可以由引理3.11分离。现在用我们替换它们的Future（Past）modalites替换所有的pis。注意，我们已经减少了未来（过去）的深度。我们重复上述过程，直到得到一个独立的公式。Q最后证明了任何公式α∈LTLGRP都是可分离的。定理3.13设α是LTLGRP（LTLMOD）公式。 那么α可以被分离。证据这涉及到公式α的交替深度n的归纳。在引理3.12中证明了n= 1。当n> 1时，我们用命题suc h代替模态，使得对于具有迭代深度的模态a，我们得到a. 公式3.12将给出一个单独的αj，用于值等于α的mula。现在用我们先前替换的模式来替换αJ中的命题我们得到的公式是交替深度小于α的。因此，我们可以重复这个过程，直到我们得到一个分离的公式。Q推论3.14每个LTL组（LTL模）公式最初等价于一个只有未来模态的公式。证据设α是LTLGRP（LTLMOD）公式。根据定理3.13，α可以被分离。我们现在可以用false替换past公式，因为所有关于past的陈述在第0个位置都是false与α等价的结果公式现在只包含未来模态。Q3.2LTL群的表达完备性引理3.15 LTLGRP（LTLMOD）具有分离性质，且它对于FOGRP（FO MOD）是表达完全的。证据（）：设α是LTLGRP（LTLMOD）公式。 我们现在可以在自由变量x上写一个一阶逻辑公式αJ（x），使得它等价于α。一阶逻辑公式可以使用相对化来分离。这可以通过对公式结构的归纳来证明。原子的例子是微不足道的。形式为φyφ（x，y）的公式可以替换为<$y（（y x）<$φ（x，y））<$φ（x，x）<$（<$y（y> x<$φ（x，y）A.V. Sreejith/电子笔记理论计算机科学278（2011）201211我现在，一个类型为y（y > x<$φ（x，y））的公式可以被一个纯未来的LTLGRP公式所取代（因为LTLGRP对于FOGRP是表达式完备的）。类似地，我们可以用纯过去和纯现在的LTL组公式代替纯过去和纯现在的FO组对于群量化器也可以给出类似的证明现在，由于LTLGRP（LTLMOD）对于FOGRP（FOMOD）在表达上是完整的，因此每个分离的公式都可以用LTLGRP（LTLMOD）公式替换。这给了我们一个单独的公式。（3）：我们证明了对于一个自由变量的FOGRP（FOMOD）公式，我们可以给出一个等价的LTLGRP（LTLMOD）公式。设P1，...，Pn是一元谓词。 证明是通过归纳法在quantifier深度。 对于基本情况，我们假设没有量化器的公式。这包括形式为Pi（x）的公式的布尔组合。这个公式的翻译将是形式为pi的公式的布尔组合。现在让我们假设所有具有一个自由变量和量化器深度为 x的所有子公式分别用T，n，n代替. 现在我们重写如下（这里v∈ {0， 1}n）：（x）=v={ 0， 1}nn（（Pi（x）惠vi）惠v（x））i=1在这里，V_v（x）用T_i代替形式P_i（x）的子公式的所有出现，T_i取决于v_i。现在，每个包含x的函数中的子公式都将是x z，x> z，x=z的形式，其中z是函数中的其他变量。我们通过引入三个新的一元谓词R，R>，R=并将x op z替换为Rop（z）（op：={<，>，=}）来去除这些公式由此产生的公式bv将不包含任何x的出现。此外，如果我们假设Rop的解释，它将等价于旧公式。现在让v=Qyαv（y）。情形1，Q= α v（y）：由于αv（y）是一个具有一个自由变量和更深的量化深度的< k，我们可以应用归纳假设得到一个具有新命题r<，r>，r=的LTL群公式γ。 我们现在记为β = Pγ <$γ <$Fγ。由于LTL组公式可以分离，我们现在可以将β分离为纯过去、纯现在和纯未来公式的布尔组合最后，在所有的纯过去公式中，我们分别用T，，代替r，r>，r=类似地，我们可以用T、纯未来的T和纯现在的T来代替所有的rop情形2，Q = G g：所以令v= G gyα1（y），.， α k（y）由于αv（y）s是具有一个自由变量和量化器深度，r=的LTL群公式φis。让我们用Φ = φφ1，...， φ k 那么我们可以写β=GPΦ <$rl（Φ）<$GFΦ，i，j，lgigj因此，Gi，Gl，Gj=G，βv=β. 如果（<$l<$φj）<$φl，则Her rl（Φ）为真j=1我们现在可以将β分解为纯过去、纯现在和纯未来公式的布尔组合。最后，在所有的纯过去公式中，我们替换r，r>，r=212A.V. Sreejith/电子笔记理论计算机科学278（2011）201分别用T，，表示类似地，可以用T，在纯粹的未来和纯粹的现在公式中。所以我们证明了公式f（x）有一个等价的LTLGRP公式。用pi替换Pi（x）在剩余的公式中的位置，将得到一个等价于π的LTLGRP公式。Q引理3.15与定理3.13一起给出了定理3.16LTLGRP（LTLMOD）对于FOGRP（FOMOD）作为推论，我们得到推论3.17每一个有一个自由变量的FO组（FO模）公式都有一个等价的使用三个变量的公式。证据设φ（x）是一个FOGRP（FOMOD）公式。 由定理3.16我们知道存在一个等价的LTLGRP（LTLMOD）公式 我们现在从图中归纳出一个FOGRP（FOMOD）公式，如下所示。归纳地给出了平移t：LTLGRP×{x，y，z} → FOGRP tx（α）， ty（α）， tz（α） 分别表示t（α，x），t（α，y），t（α，z）。对于公式α，我们给出平移tx如下LTL组FO组pP（ x）α∨ βtx（ α）<$ tx（ β）¬α<$tx（α（x））αU βy（y > x<<） = α t z（α（z））αS βy（yx）G Fφ1，.， φ kGG g y <$（x< y）<$t y（φ1（y）），.，（x y）ty（φk（y））G Pφ1，.， φ kGG g y <$（x> y）<$t y（φ1（y）），.，（x> y）ty（φk（y））显然，这种转换只使用了三个变量，因此我们得到了一个等价的三个变量的FOGRP（FOMODQ4UTLgrp和FOgrp的两个可变片段在这里，我们表明，UTLGRP是表达完整的两个变量的逻辑片段的FOGRP，（写为FO2GRP）。定理4.1UTLgrp对于FO2grp是表示完备的.证据 翻译是递归的。对于原子公式，布尔组合和存在公式，我们遵循Etessami等人的证明[4]。我们在这里给出群quantifier的翻译（类似的翻译可以给出A.V. Sreejith/电子笔记理论计算机科学278（2011）201213我我我我我GGG我我我G1G2G3模量化器）。让φ（x）：= G g y <$φ1（x，y），.， φ k（x，y）φj（x，y）的Each，对于j≤k，可改写为φj（x，y）：=τj（γj（x，y），.， γj（x，y），α j（x），.， αj（x），βj（y），.，βj（y））1r1s1t这里τjs是布尔命题公式。γjs是形式为xy，x=y，x > y的序公式。群量化器内部的后继关系可以被移除，因此我们在这里不考虑它。αjs和βjs是我我quantifier深度小于φ（x）的quantifier深度。 此外，αjs和βjs为我我原子的、存在的或群量化的类型。我们先把αjs取出来集团量化器。对于向量v =（v1，.，v sk）∈ {0，1}sk我们定义j（x，y）=τj（γj（x，y），.， γj（x，y），vj，1，.， vj，s，βj（y），.，βj（y））v1r1t设对g ∈ G，g ∈G为G g y∈G1（x，y），.，k（x，y） 然后我们可以将φ重写为：V Vφ（x）：=（αj（x）惠vj，i）g（x）v∈{0，1}ksj≤k，i s注意，γjs是有序公式。设Γ ={xy，x=y，x > y}是x和y之间所有序关系的集合。对于任何序关系，o∈Γ，γjs将被求值为{T，F}。 设γj为γ g（x）中的T/F，取决于顺序O。 注意，x并不出现自由的。 从而得到φ（x）：=（αj（x）惠vj，i）yxv∈{0，1}ksj≤k，isg1g2g3=g因为公式是不包含自由变量等效UTL组公式存在.公式αj（x）具有等价的UTLGRP公式，因为它们的quantier深度小于φ（x）的quantier深度。因此，我们得到了一个与φ等价的UTLGRP公式。Q引用[1] 巴涅克巴尔湾和H.Barringer，Temporal logic with fixed points，in：Temporal Logic in Specification（1987），pp. 62比74URLhttp://portal.acm.org/citation.cfm?电话：+86-647236.720405/+86-647236.720405[2] 巴林顿湾一、N. Immerman和H. Straubing，关于NC1中的均匀性，计算机与系统科学杂志41（1990），pp. 274-306[3] Bazira mwa bo，A.， P. McKenzie和D. T 'erien，M odulartem po rallgic，in：P roc.14thLICS（1999），p. 344.[4] Etessami，K.，M. Y. Vardi和T.Wilke，一阶双变量逻辑和一元时态逻辑，Inf.Comput。179（2002），pp. 279-295.214A.V. Sreejith/电子笔记理论计算机科学278（2011）201[5] Gabbay，D.，A. Pnueli，S. Shelah和J. Stavi，公平性的时间分析，在：第七届ACM程序设计语言原则研讨会论文集，ACM，1980年，第100页。163-173.[6] Gabbay，D. M.，声明式过去和命令式未来：交互式系统的可执行时态逻辑，在：规范中的时态逻辑（1987），pp。409-448.URLhttp://portal.acm.org/citation.cfm?电话：+86-647236.760143传真：+86-647236.760143[7] Gabbay，D. M.，I. Hodkinson和M. Reynolds，[8] Henriksen，J.G. 和p.动态线性时间时序逻辑，北京：计算机科学出版社.纯应用逻辑96（1999），pp. 187-207[9] 霍德金森岛M.，关于GabbayComput. Sci. 139（1995），pp.1-25[10] Janin，D.和I. Walukiewicz，关于一元二阶逻辑的命题μ演算的表达完备性，在：第七届国际并发理论，CONCUR263-277。URLhttp://portal.acm.org/citation.cfm?电话：+86-646731.703838[11] 坎普，J. A. W.，“时态逻辑和线性顺序理论”，博士。加州大学洛杉矶分校毕业论文（1968年）。[12] 洛达亚湾和A. Sreejith，LTL可以更简洁，在：Proc.8th ATVA，新加坡，LNCS6252，2010，pp. 245-258[13] Pnueli，A.，程序的时序逻辑，见：focs77，1977，pp.46比57[14] Prior，A.N.，[15] R. McNaughton和S.《无计数器自动机》，麻省理工学院出版社，剑桥，美国，1971年[16] 斯托克迈耶湖J. 和A.R. Meyer，Word问题需要指数时间（初步报告），在：Proceedings of the fifth annual ACM symposium on Theory of computing，STOC一比九URLhttp://doi.acm.org/10.1145/800125.804029[17] Straubing，H.，D. T 'erien和W. Thomas，Regularlanguagesdefine ed ededwithgene raliz edquantiers，Inf. Comput. 118（1995），pp. 389-301.[18] Wolper，P.，时间逻辑可以更有表现力，Inf.- 是的56（1983），pp.72比99