数据字上的混合时序逻辑：HTL与LTL对表达能力比较及简洁性研究

可在www.sciencedirect.com在线获取理论计算机科学电子笔记278（2011）115-128www.elsevier.com/locate/entcs混合时序逻辑的数据字Ahmet Kara1，2Thomas Schwentick1，3TU Dortmund，德国摘要数据字上的混合时序逻辑（HTL）可以被认为是LTL逻辑的扩展↓[3]《易经》云：“天之道也，地之道也。 本文比较了HTL和LTL↓对数据词的表达能力。它表明，有属性的数据字，可以表示在HTL与两个变量，但不是LTL↓。另一方面，可以用HTL中的一个变量表示的每个属性也可以用LTL↓中的一个变量表示。本文进一步研究了HTL与LTL↓相比的简洁性，并证明了HTL的变量数层次是无限的。保留字：混合逻辑，时态逻辑，数据字。1介绍在本文中，数据字是一个有限的位置序列，它携带一个数据值和一组命题。近年来，关于数据字的逻辑已经被研究了很多在[2，3]和许多后续文件。在本文中，我们考虑混合时态逻辑的数据字。 作为一个例子，公式G = G（p<$↓x. F（qx））表示，对于每一个携带命题p的位置，具有相同数据值并携带命题Q的未来。量化器↓x将变量x绑定到当前位置，并且x将当前数据值与绑定到x的位置处的值进行比较。该逻辑还允许公式为@x. x（在位置x处计算x）和x（如果x是当前位置，则为真）。混合时序逻辑首先在[13]中被考虑，并在线性结构上进行了深入研究，例如， 在[1，9，15]中。 之前已经注意到，在[3]中引入的数据字上的逻辑LTL↓本质上是混合时序逻辑[4，5，19]。在1我们感谢德国DFG根据SCHW 678/4-1号赠款提供的财政支持2 电子邮件：ahmet. cs.uni-dortmund.de3电子邮件：thomas. cs.tu-dortmund.de1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.10.010116A. 卡拉，T.Schwentick/Electronic Notes in Theoretical Computer Science 278（2011）1151事实上，LTL↓可以被认为是混合时序逻辑的语法片段，没有形式为@x. x和x的公式。形式上，在LTL↓中，变量绑定到数据值而不是位置。然而，只要引用变量x的唯一方式是通过原子公式x，差异就不重要了。因此，上述公式可以被视为LTL↓公式。本文研究了在数据字上引入将来时态算子和过去时态算子的混合时态逻辑，并与LTL↓的表达能力进行了比较。HTL和LTL↓一方面与自动机有对应关系另一方面，数据词的模型。如[4]所示，LTL↓中的所有性质都可以由一个交替寄存器自动机来决定。另一方面，逻辑HTL由卵石自动机捕获这直接来自于HTL只能表示一阶属性，即使是确定性的单向卵石自动机也可以表示数据字的所有一阶属性[12]。LTL↓和交替寄存器自动机之间的关系以及[12]中的先前结果立即产生LTL↓和HTL之间的分离事实上，在[12]中，定义了数据字的一阶可表达属性，由交替寄存器自动机决定，因此不能用LTL↓表示。另一方面，不难证明HTL可以表达数据字的所有一阶属性，因此也可以表达这个特定属性。我们通过证明仍然不能用LTL↓表示的类似性质可以用只有两个变量的HTL公式表示来加强这一结果，从而建立LTL↓/≤ HTL2。有趣的是，当我们将公式限制为一个变量时，HTL和LTL↓我们的主要结果表明HTL1= LTL↓。我们进一步表明，• HTL1-公式可以指数地比LTL↓-公式更简洁，HTL-公式甚至可以非初等地比LTL↓-公式更简洁;• HTL在数据串上的变量层次是无限的。为此，我们证明了Rossman我们的大多数结果也适用于无限数据字（参见。第5节）。我们已经在上面提到了相关的工作。本文的结构如下。在第2节的讨论之后，我们在第3节中给出了至少有两个变量的HTL的结果，在第4节中给出了HTL1的结果。我们在第5节结束。由于篇幅所限，我们不能详细介绍所有证据。特别是，一些公式翻译的正确性证明缺失。然而，我们总是试图设计翻译的公式，以便读者可以轻松验证其正确性。我们感谢Thomas Zeume和一位匿名评论者提供的许多有用的建议。[4]在形式上，这只在[ 12 ]中针对空命题集上的有限数据词进行了证明。然而，证明只是通过数据字。A. 卡拉，T.Schwentick/Electronic Notes in Theoretical Computer Science 278（2011）115117我我2预赛数据字。设A是命题的有限集合，D是数据值的有限集合。一个字符串是一个有限的序列的元素从2<$。 一个在D上的数据字是一个来自（2× D）的元素的有限序列数据字表示为w = P1···Pn，其中P1，.，Pn∈ 2 π且d1，.，dn∈D. 如果p∈Pi，我们说i是d1dn标记为p，i是p位置。我们称di为位置 i。如果Pi是一个单例集合{p}，我们写p而不是{p}。D d逻辑。基于数据字的混合时态逻辑（HTL）是对线性时间逻辑LTL（参见例如，[7]通过过去的操作符和变量。HTL的语法如下。：：= p |X |↓x.|阿克斯|@ x. |X轴|U|X −X| U −|¬ϕ |ϕ ∧ ϕ其中p∈n，x是来自无穷多个变量的VAR集合的变量。像往常一样，我们考虑其他逻辑运算符，→和Participate以及其他时间运算符F： =T U，F−：=T U−，G：=和G−：=作为缩写。算子X， U， F，G， X-， U-， F-， G-称为时间算子。我们将算子X、 U、 F、 G称为未来算子，四个是过去的运营商对于数据字w，|W|=n赋值是一个映射g ：VAR→{1，.，n}。 对于赋值g、变量x和w中的位置i，gx表示映射定义为gx（x）：=i和gx（y）：=g（y）对于所有yX. 的语义我我对于数据字w=P1···Pn，a，位置i在w中，赋值g为w。• w，g，i |= p if p ∈ P i• w，g，i |= ↓x. if w，g x，i |=• w，g，i |= x if g（x）= id1dn• w，g，i|如果d i= d g（x），则= x• w，g，i |=@ x. if w，g，g（x）|=• w，g，i |=<$i if w，g，i |=• w，g，i|如果w，g，i，则|= n和w，g，i|=• w，g，i|= X if i 1且w，g，i − 1，|=• w，g，i|= U−if 有一个j，其中1 ≤ j ≤ i，w，g，j|=和w，g，k|对于所有k，j 1时，D是D上的（m-1）-超集的有限集。为了简单起见，我们假设D是自然数的集合我们把m-超集Hm（w）与数据字w除以{z，b，e，.，b 得双曲余切值. }如下。 数据字w=b1z···ze1，其中d1 1m mdn1nj d′和DJ是任意数据值，表示1-超集H1（w）={n1，.，n j}。 如果对于某个m≥2和l≥0，每个数据字uj，1≤j≤l，表示一个（m-1）-hyperset，则数据字u=bmu···你好表示m-超集D1H m（u）={H m−1（u1），.，H m-1（ul）}，例如，利迪H. b2 b1 z z e1 b1 z z z e1 b1 z z e1 e2 n ={{1，2}，{7，8，9}，{2，5}}。如果u不表示任何m-超集，则记为Hm（u）=Hm（u）。对于每个m≥1，我们定义集合Lm（带有附加命题s）为Lm={u sv|Hm（u）=Hm（v）=f∈D}.命题3.2（[12]）对于m≥ 4，Lm不能由双向交替寄存器自动机决定.这个命题可以沿着与上述结果相同的路线来显示。事实上，[12]的结果很容易推广到Lm和[3]中定义的双向交替寄存器自动机定理3.3对于每个m ≥ 1，集合L m可在HTL 2中定义。证据 对于任意m ≥ 1，我们定义一个公式：m∈ HTL 2（X，U），使得w|当且仅当对于所有数据字w，w ∈ L m。公式m是几个子公式的合取。下面的三个子公式一起表示w具有us v的形式，其中Hm（u）/=m且Hm（v）/=m。• 一个简单的公式χone表示“每个位置都只携带一个来自{ z，s，b1，. ，b m，e1，. ，e m}。”• w的形式为u s v，u和v以b m -位置开始，以e m -位置结束，并且没有携带bm，e m或s的其他位置。χmain=bmX[<$（bmsem）U（emX（sX（bm（<$（bmsem）U（em<$XT））][5]实际上，[3]和[12]中的双向交替寄存器自动机的定义并不完全一致然而，不难看出，[3]的结果也适用于[12]的无命题数据词上的自动机。120A. 卡拉，T.Schwentick/Electronic Notes in Theoretical Computer Science 278（2011）115DD• “<每一个bi-位置后面直接跟着一个bi −1 -或一个ei-位置，每一个z -位置后面直接跟着一个z -或一个e 1 -位置，对于im，每一个ei-位置后面直接跟着一个bi-或一个ei +1-位置。”这里，b0表示z。Mχhyp= G（z→X（z<$e1））<$（bi→X（bi−1<$ei））<$i=1m−1（e i→ X（b i∈ ei+1））。i=1接下来，我们构造了一个实际上表示Hm（u）=Hm（v）的公式。• 如果x和y被绑定到b个1-位置，则公式R1检查两个1-超集，它们的编码分别从x和y开始，是相等的。1=@x。X. .e1 @y。X（<$e1U（<$e1x））Ue1@ y。X. .e1 @ x。X（<$e1U（<$e1y））Ue1• 同样，对于2≤i≤m，公式i表示，如果x和y被约束到bi-位置，分别从x和y开始的i-超集相等：i=@x。. .bi−1→↓x。@y。（<$eiU（bi−1 <$↓y. i−1））@ y。. .bi−1→↓y。@ x。（<$eiU（bi−1 <$↓x.<$i−1））<$Uei<$最后，所需的公式为：m= χ oneχ mainχ hypo↓x。F（s <$X↓y. m）。每个词w=us v∈Lm通过构造满足χone、χmain和χhyp作为u和v表示相同的超集，则矩阵m的两个部分也都满足如果一个数据字w满足m，则公式χone、χmain和χhyp确保w的形式为us v，并且u和v编码m-超集。m的两个部分确保了在u中编码的每个（m-1）-超集也出现在v中，反之亦然。因此，遵循的完整性和正确性的矩阵Q推论3.4 HTL 2/≤ LTL ↓。对定理3.3的证明进行更仔细的考察，可以得到进一步的见解。第一，公式m不使用任何过去运算符，也不使用形式为x的原子公式。另一方面，正如在[15]中已经观察到的，@x. x形式的公式可以被FF-（x<$x）形式的公式代替，因此，在存在过去运算符和原子公式x的情况下，不需要@-运算符。因此，在本发明中，我们得到定理3.3证明的下列推论。推论3.5LTL↓不能表达所有可表达的性质(a) HTL2（X， U），没有形式x的原子式，并且在(b) HTL 2没有@ x. x形式的子公式。但是，如果没有past运算符，@-运算符就不能再模拟了事实上，没有@-运算符的HTL的future片段与LTL↓ 的future片段对于封闭公式一样具有表达A. 卡拉，T.Schwentick/Electronic Notes in Theoretical Computer Science 278（2011）115121性。122A. 卡拉，T.Schwentick/Electronic Notes in Theoretical Computer Science 278（2011）115K.ΣK命题3.6每个不带@ -算子的闭HTL（X，U）公式都可以转化为等价的LTL ↓（X，U）-公式。证据对于k≥1，设k是HTLK（X， U）的闭公式，其中@不出现.在不失一般性的情况下，我们假设至多变量x1，.，x k出现在k中。其思想是，在公式↓x.中，原子公式x只有在某个时态运算符“移动”了“当前位置”时才求值为真。因此，是跟踪是否在绑定到变量的位置上计算子公式。根据这一点，原子公式xi可以被T或代替。作为一个例子，公式↓x i. X x i等价于公式↓x i。X.我们在S上定义一个映射，对于{x1，.，xk}，HTL k（X，U）-公式，使得对于每个数据字w，w的每个赋值g和每个位置i，w，g，i |=优惠w，g，i |= onS（n），如果S被选择为{x，j|g（x，j）= i}.转换定义如下（我们省略布尔运算符）。• 关于S（p）=p，对于命题p.T，ifxi∈S否则，• 关于S（xi）=xi• 在S（↓ x i. x）= ↓ x i. 关于S<${xi}（x）• onS（XX）=Xonn• onS（χUχJ）=onS（χJ）<$onS（χ）<$X（on<$（χ）Uon<$（χJ））最后 ， 对 于 多 个 节 点 ， 对 于 多 个 节 点 （X，U），等式为L T L ↓（X，U）。Q最后，我们注意到，对于数据字上的HTL，可以像[9]中的线性框架上的HTL一样进行类似的观察。特别地，当k≥1时，每个HTLk公式都可以转化为一个初始等价的HTLk+2未来公式。 这个想法是将第一个附加变量，比如x，绑定到单词的第一个位置。在[19]中，在分支时间逻辑的上下文中使用了类似的技术引理3.7当k≥ 1时，每个HTLk公式都可以转化为初始等价的HTLk+2（X，U）公式。证据设x和y是两个附加变量。我们使用以下HTLk公式<$k到HTLk+2公式<$J的转换。• （X）J=XJ• （Uχ）J=J UχJ• （X-X）J= ↓y。@ x。F（XyJ）• （U −χ）J：↓y。@ x。F（Fy<$xJ<$ $>（y<$XG（Fy→<$J）在这里，省略了琐碎的情况。然后，每个HTLk公式<$1最初等价于HTLk+2（X， U）公式↓x.<$J。Q• 关于S（xi）=A. 卡拉，T.Schwentick/Electronic Notes in Theoretical Computer Science 278（2011）115123k+1K2i+83.2层次结构结果在本节中，我们将展示HTL-和LTL↓-层级都有无限多个层级。更准确地说，不存在k>0使得对于每个i，HTLi<$ HTLk或LTL↓< $LTL↓。事实证明，这可以从罗斯曼Ik一个定理，一阶逻辑在有序图上的变量层次是严格的[14 ]第10段。在下文中，我们用FOk来表示一阶逻辑对至多k个变量的公式的限制。定理3.8（Rossman [14]）对任意k≥ 1，有限无规则有序图上的FO k≠ FO k+1。我们用数据字定义了有限无向有序图的规范编码，并给出了以下两个引理。引理3.9对于每一个公式f∈FOk，都有一个公式F∈LTL↓使得对于每个无向有序图G和 G的每个标准编码w，G|=优惠w=0.0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000|引理3.10对于每个公式f_J∈HTL_k，存在一个公式f_j∈FO_2k+6，使得对于每个无向有序图G和G的每个标准编码w，|= 100G| = 0。这两个引理和Rossman定理3.11（a）数据字上的LTL ↓-层次是无限的。（b）数据字的HTL k-层次结构是无限的。证据 为了避免矛盾，让我们假设存在某个i，使得对于每个j > i，LTL ↓=LTL ↓，或者使得对于每个j > i，HTL j= HTL i。让我们J I是FO2i+7中有序图的任意公式。根据引理3.9，有一个公式<$J∈LTL↓使得G|=惠w=0.0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000|假设有6个a公 式 j ∈ HTL i 使 得 对 于 每 个 数 据 字 w ， 它 保 持 w = 100 美 元 =0.0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000||根据引理3.10，有一个公式n∈FO2i+6，使得对每个无向有序图G和G的每个标准编码w，它成立w| = 100G| = 0。因此，请原谅。由于从FO2i+7中任意选择了f，我们可以得出结论：FO2i+7124A. 卡拉，T.Schwentick/Electronic Notes in Theoretical Computer Science 278（2011）115我= FO2i+6，即所需的矛盾。Q它只剩下定义规范编码和证明两个引理。在下文中，我们只考虑没有自环的图。这与Rossman我们说一个数据字w是一个有限有序无向图G=（V，E，<）的规范编码，如果以下条件成立。• w具有|V|+2|E|位置，· 一个节点位置p（u），对于每个u∈V，· 对于每7个边缘（u，v），边缘位置q（u，v）。6如果我们认为LTL↓-hierarchyclapsanwegefora rar b e egee f or ar a r b e egee fo r ar a r然而，在HTLi.7 每个边（u，v）产生两个位置，q（u，v）和q（v，u）。A. 卡拉，T.Schwentick/Electronic Notes in Theoretical Computer Science 278（2011）115125一BCD.Σ我• 节点位置p（u）具有唯一的数据值并携带命题p。• 对于每个u，v，（u，v）∈E，边位置q（u，v）和q（v，u）具有相同的数据值（并且该值不会在其他情况下出现）并且不携带任何命题。• 对于每个u，uJ，v，vJ∈V，位置的顺序遵循以下规则：· p（u）↓x.<$J.我们通过对λ的大小的归纳来说明这一点。由于等效• ↓x. pp，• ↓x. x T，• ↓ x. 你好，• ↓ x. @ x.↓ x.，• ↓ x. <$<$↓x.，• ↓ x. （χ）↓x. ↓x.χ我们可以假设，X是以下形式之一：（1）<$U x，（2）X<$，（3）<$U−x，（4）X−<$。我们将情况区分为（1）和（2）。 Let−→Bleb e asguaranteedbyLemma4. 1 .一、因此，对于每个数据字w和w的所有位置i，l，w，l，i |= ↓x.优惠−→（w，i）T（m） 我|=−→ 。例如，将重新编程为mulapx的mu l apxin−→nulap x的mulap−→在由（w，i）T（n）[i，. . ）通过将来自不具有f-→ f的可变值的数据值放回。智能化，重新规划针对Mula的自动化通过公式↓x.J（其中J是等效于通过归纳获得的的LTL ↓-公式）计算p ↓ x.，也不会改变有效性。我们将所得公式用表示。剩下的只是把p类的原子公式从n中去掉。每−→赋值α：T（k）→ {T，k}设kα是由k得到的公式，J=−→α：T（ε）→{T，ε}ϕα∧−→@x.∈T（）α（@ x.λ）=T吉吉−→@x.∈T（）α（@ x. λ）= λ130A. 卡拉，T.Schwentick/Electronic Notes in Theoretical Computer Science 278（2011）115你好，A. 卡拉，T.Schwentick/Electronic Notes in Theoretical Computer Science 278（2011）115131111i=11其中，J也是一个等价于通过归纳法得到的的LTL ↓ -公式，不再使用任何额外的命题。（3）和（4）是完全相似的。所得公式的大小由（至多）f − → f的三重指数大小z e决定。消除@ only限制是一种扩展性因素，最多有三倍指数大小的公式。Q4.2简洁性尽管HTL1表示 LTL↓，但HTL1可以比LTL↓，甚至LTL↓，以指数方式更简洁地表达一些属性。命题4.4 HTL 1（F）比LTL ↓更简洁。证据该证明实质上遵循[8，定理3（1）]的证明，即 FO2比一元LTL指数地更简洁。 设En是性质“在命题p1，p2，.上一致的词的任何两个位置。，p n也同意命题p0。”设Ln是填充En的数据字的集合，其中所有位置具有相同的数据值。对于每个n≥1，Ln表示为（2）在O（n）的情况下，函数的长度为G↓x。G xG[↓x. G（n （p i参与@ x.p i）→（p0参与@x.p0））]。现在让我们假设，对于每一个n，有一个LTL ↓-公式n表示L n，|卢恩|= 2 o（n）.这个公式可以转换成一个大小大致相同的公式χn，它表示没有数据的单词的En如[18]中所示，o（n）对于每一个，一个不确定的数据是针对大小为2的任何数据的|χn|=22. 然而，它可以在[8]中证明，对于En，需要至少22n个状态，想要的矛盾。Q5讨论本文比较了混合时态逻辑与LTL↓对数据词的表达能力。虽然HTL通常更强大，但如果只允许一个变量，则两个逻辑本文的主要结果结转到无限长的数据字。对于推论3.4和定理3.11，这仅仅是因为分离语言可以很容易地通过填充无限数量的位置而变成ω定理4.3到无限数据字的推广也是直接的。在这里，重要的是[11]的结果已经针对ω-弦给出了。显然，所有考虑的逻辑都有一个不可判定的满足性问题（对于LTL↓这是在[3]中显示的）。 然而，模型检查仍然在很大程度上未被探索，特别是对于无限数据字的情况。正如在第3节中已经提到的，我们推测HTL和LTL↓的变量层次都是严格的。132A. 卡拉，T.Schwentick/Electronic Notes in Theoretical Computer Science 278（2011）115引用[1] 卡洛斯 槟榔， 帕特里克 布莱克本， 和 Maarten 马克思混合时态逻辑的计算复杂性。LogicJournal of the IGPL，8（5）：653[2] Mikolaj Bojanczyk，Anca Muscholl，Thomas Schwentick，Luc Segou Finn，and Claire David.关于带数据的词的双变量逻辑在LICS中，第7IEEE计算机学会，2006年。[3] 斯蒂芬·德姆里和兰科·拉齐奇 使用冻结量化器和寄存器自动机的LTL。 在LICSIEEE计算机协会。[4] 我是你的朋友，我是你的朋友，我是你的朋友。 LTLwithefreezequan itieri s t erautoata. ACMTran s.Comput. Log. ，10（3），2009.完整版本[