多项式时间内的二元自动机A_（？）ne壳

理论计算机科学电子札记98（2004）89-104www.elsevier.com/locate/entcs二元自动机的A_（？）ne壳在多项式时间J'er dumberomeLeroux1LaboratoireSp'ecicationtV'erif ication，CNRS UMR 8643& ENS de Cachan，61av. 如果我告诉你我儿子，94235 Cachan cedex，法国摘要我们提出了二元自动机类，它是Nm的子集的一种新表示，自然地扩展了NDD（[25]，[10]）。我们证明了一个二进制自动机表示的向量集的一个可计算的外壳是在多项式时间内。作为应用，我们证明了计数器系统（广播协议的扩展[16]，[13]，[12]，重置/转移Petri网[15]，[11]和线性系统[18]），在多项式时间内是可计算保留字：Presburger，一个布尔壳，NDD，二进制自动机，位置不变量。1导论.一个无限状态系统是通过定义一个系统，其可达集可以包含无限数量的配置。因此，对于这样的系统，不可能仅仅通过枚举它的元素来表示这个集合。为了克服这个问题，符号模型检查器实现了适应于所表示的无限集合的结构的符号例如，工具TRE X[24]，[4]实现了SRE [1]用于表示在子词关系[2]下闭合的词的无限集合，工具BABYLON[5]，[3]使用CST [14]表示向上闭合集合[19]，等等。在本文中，我们感兴趣的是NDD [25][26]（也称为DFA [10]，[23]，[21]，[20]），符号模型检查器1电子邮件：leroux@lsv.ens-cachan.fr1571-0661 © 2004由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2003.10.00790J. Leroux / Electronic Notes in Theoretical Computer Science 98（2004）89-FAST[6]，[17]和LASH[22]表示Nm一个有限的自动机。这些工具在不同的实现级别上使用NDD：• 代表输入系统。事实上，这些工具分析计数器系统，使得每个动作由NDD表示，该NDD表示可以触发动作的配置集（LASH要求该集合是凸的[18]），并且由一个与动作触发前后的计数器值相关的函数表示• 表示输入系统必须保证的属性。这个属性实际上是一个NDD，它代表了系统必须避免的一组坏配置• 加速转型（[18]，[9]，[8]）。在某些代数条件下（满足[18]，[6]），可以计算表示动作序列的传递闭包的NDD• 来表示可达性集的子集。在这些工具中，没有对计数器系统进行结构分析以简化可达集的计算。然而，在Petri网[7]或更一般的自/修改Petri网[11]的情况下，位置不变量是一个有用的工具：• 用于减少系统的真实计数器的数量[14]（回想一下，在实践中，我们在工具FAST和LASH中受到十几个计数器的限制• 用于帮助终止可达性集合。事实上，我们可以计算一个配置的过近似，从（[14]）可以达到一个坏的配置，并将可达集的计算与这个过近似相交。我们在这篇文章中证明了一个有趣的结果：位置不变量可以扩展到FAST和LASH中使用的计数器系统，并且在多项式时间内保持可计算性。为了得到这个结果，我们证明了另一个结果：由NDD接受的向量集的A-壳是在多项式时间内可计算的。我们的贡献• 我们引入了二进制自动机类，NDD的自然扩展。而NDD对应于一个字一个字的表示，我们表明，类的二进制自动机是一个位的位表示。• 我们证明了一个二进制自动机表示的向量集的一个可计算的外壳是在多项式时间内。J. Leroux / Electronic Notes in Theoretical Computer Science 98（2004）89-91我• 我们介绍了计数器系统类，广播协议类的扩展，重置/转移Petri网和线性系统。• 我们将位置不变量的定义扩展到这个类，并证明它们在多项式时间内仍然是可计算的• 我们展示了位置不变量和可达性关系的可达性外壳之间的联系.文件计划在第2节中，我们回顾了一些常用的符号，在第3节中，我们解释了为什么本文中使用的所有操作都可以通过使用高斯消去算法来完成。在第4节中，介绍了二进制自动机，在下面的部分中，提供了一个算法，用于计算一组向量的一个二进制自动机接受的包。最后，在第6节中，证明了这个包对于计算有效计数器系统的位置不变量是有用的，有效计数器系统是最后一节中介绍的模型。2符号。一个有限集合X的基数记为卡（X）。有理数、整数和正整数的集合分别记为Q、Z和N。在集合X中具有m个分量的向量的集合记为Xm。向量x∈Xm的第i个分量记为xi∈X;我们有x =（x1，...，xm）。 对于任意向量v，vJ∈Qm，且对于任意t∈Q，我们定义t.v（t.v）i=t.vi和（v+VJ）i=vi+VJ.Qm的向量子空间V是一个非空子集V<$Qm，使得对于每个v，vJ∈V和对于每个t，tJ∈Q，我们有t.v+tJvJ∈V。Qm的一个非空子空间A是Qm的一个子集（最终为空），使得对每个a，AJ∈A和对每个t，TJ∈Q使得t+TJ= 1，我们有t.a+TJ.AJ∈A.由于任何一个交线空间仍然是一个交线空间，Qm的子集X被很好地定义为包含X的最小一个双曲空间;这个双曲空间被写为一个双曲空间（X）。 回想一下，对于任何集合X，存在一个有限子集XJ<$X使得a（X）= a（XJ）。特别地，对于任意的a-空间A，存在一个有限子集XJ<$A使得A= a <$（XJ）。回想一下，一个a-logne空间A的维数是最小整数，dim（A）∈ {− 1，.，m}使得存在一个有限子集X<$A满足a <$A（X）= A和card（X）− 1 = dim（A）。 这样的子集X称为A的基。Q上的方阵集记为Mm（Q）。函数f：Qm→92J. Leroux / Electronic Notes in Theoretical Computer Science 98（2004）89-称Qm是一个方阵，如果存在一个方阵M∈Mn（Q）和一个向量v∈Qm使得对任意x∈Qm，f（x）=M.x+v. 函数f：Qm→Q如果存在一个向量v∈Qm，则对于每个x∈Q m，有f（x）=Mi=1 第五章因此，线性函数的集合是向量空间同构于Qm。在一个有限的字母表上的一组单词被写为。在中，两个单词σ和σJ的连接被写作σ.σJ。 The empty word in Σ∗ is writtenϵ.一个有限自动机ffi是一个元组ffi=（Q，Q0，F）;Q是有限状态集，是有限字母表，Q× ×Q是转移关系，Q0Q是初始状态集，FQ是最终状态集一个有限自动机ffi被称为完备的和确定的，如果集合Q0被简化为一个元素Q0={q0}，并且如果存在一个函数δ：Q× Q→Q使得Q ={（q，δ（q，a））;q∈Q;a∈ N}.有限自动机ffi中从状态q到状态QJ的路径P是有限序列q = q0，（q0，a1，q1），q1，.，（qn−1，an，qn），qn= qJ其中n ≥0使得（qi−1，ai，qi）是n中的跃迁。P的标号是σw〇rdσ=a1. . 。 an∈N。 如果ch是一条路，则记为q−→qJ。集合X上的二元关系R是X×X的子集;如果元组（x，xJ）∈ R，我们写xRxJ。在X上的恒等关系写为IX或I，它定义为xIxJi <$x=xJ。3关于复杂性的问题。在这篇文章中，我们经常考虑两个a-mne空间的并的a-mne壳，a-mne函数对a-mne空间的映象，并且我们经常检验两个a-mne空间的包含。我们通过用A中至多m+1个向量的有限集合X表示一个A-维空间A，使得A= a-维（X），来简单地研究这些运算的复杂性。首先注意，如果A和AJ是分别由X和XJ表示的两个A-N空间，那么通过使用高斯消去法，我们可以在多项式时间内计算X <$Xj中至多m +1个向量的有限子集P，使得a <$（A <$AJ）= a <$（P）。此外，我们还将空间f（A）定义为一个空间A= A_x（X）被一个空间函数f（x）=M.x+v（其中M∈M_m（Q），v∈Qm由集合f（X）表示。最后，注意到通过使用高斯消去法，对于Qm中至多m+1个向量的任意两个 集 合 X 和 XJ ， 我 们 可 以 在 多 项 式 时 间 内 检 查 是 否 a <$ （ X ） <$a<$（XJ）。J. Leroux / Electronic Notes in Theoretical Computer Science 98（2004）89-93RRR4二进制自动机二进制自动机被证明是NDD的一个自然的扩展，通过提供Nm的向量的位表示，而NDD是一个字的字表示。回想一下，NDD是字母表上的确定性和完全自动机，r−1}，其中r≥ 2称为分解基，使得自动机接受的任何单词的长度都可以除以由m.这种表示非常适合表示N的子集，因为任何x ∈ N都可以表示为一个有限的“位”序列。一个向量x∈Nm也很容易用一个词 b1b2来表示. bn.m，使得eachxi表示d bybibi+m. 。 。 bi+（n−1）. M. 用这种表示法，我们注意到，由b1b2..bn.m与表示d bybm+1bm+1. . . 的 向 量 x 有 关 。 。 bn. 他跟着我的翅膀走xJ= r.x+（b1，...，b（m）出于这个原因，我们声称NDD是一个字接一个字的表示，需要读取m-位的m-位来计算所表示的向量。这种限制似乎与由二进制自动机表示的向量集的多项式时间计算相矛盾，这是由于卡（Kr）m的指数大小。为了克服这一限制，我们建议关联到任何词σ∈εεNm中的向量，对σ的长度没有任何限制。让我们引入一个为任何词定义的函数λσ：Qm→Qm对于任意位b∈R，通过以下归纳：λb（x1，.，Xm）=（X2，.，xm，r.x1+ b）λb.σ=λ b<$λ σ定义4.1向量x∈Nm的二进制表示是词σ∈Nm使得x = ρ（σ），其中ρ（σ）= λσ（0，.，0）。定义4.2二元自动机ffi是在alpha- bet上的有限自动机。由二元自动机ffi表示的向量集是Nm的子集ρ（L（ffi））。我们现在可以用我们的符号给出NDD的定义，它等价于原始定义，因为对于任何单词b1. bm，对于任意x∈Qm，我们有λb1. bm（x）= r.x+（b1，.，bm）。94J. Leroux / Electronic Notes in Theoretical Computer Science 98（2004）89-R000定义4.3[9] NDD是一个确定性的完全二进制自动机，使得m整除任何可接受的单词的长度注4.4NDD还允许通过考虑2补数表示来表示Zm为了简化本文的介绍，我们没有考虑这个特殊功能。然而，通过考虑2-补数表示或通过将其标记为任何向量x ∈ Zm，存在一个字σ ∈ Z m使得x = λσ（−1，. ，−1）.Rr r看起来，这个较晚的表示，比2-补更代数第一，也更简洁（这是一项正在进行的工作）。显然，正如下面的命题所证明的那样，二元自动机和NDD表示Nm的相同子集。命题4.5子集X<$Nm可由二元自动机表示当且仅当X可由NDD表示。证据首先注意，如果子集X<$Nm由NDD表示，那么X由二元自动机表示，因为NDD是二元自动机。相反，让我们考虑一个由二进制自动机ffi表示的子集X<$Nm。我们首先证明，我们可以假设L（ffi）。0= L（ffi）。 由于L（ffi）和0是两种正则语言，所以语言L（ffi）。0也是正常的。因此，我们只需要证明ρ（L. 0）= ρ（L）对于任何子集L。从包含LL。0 <$，我们推出ρ（L）<$ρ（L. 0分）。让我们证明逆包含。设x∈ρ（L. 0分）。存在i≥0且σ∈L使得x=ρ（σ. 0i）。 从x=ρ（σ. 0 i）=λσ。0i（0，.，0）= λσ（λi（0，.，0））=λσ（0，.，0）=ρ（σ）∈ ρ（L），我们推出ρ（L. 0）ρ（L）。 因此，我们可以假设L（ffi）。0=L（ffi）。注：我们还可以假定ffi =（Q，r，δ，{q0}，F）是决定的和完备的. 我们用[i] ∈ {0，.，m-1}是i除以m的剩余部分。让我们考虑二进制自动机ffiJ=（QJ，Δ r，δJ，{qJ}，F J），定义为：QJ= Q × {0，. ，m − 1}吉吉δ（（q，i），b）=（δ（q，b），[i+1]）qJ=（q0，0）FJ=F× { 0}注意ffiJ是NDD。所以我们只需证明ρ（L（ffi））=ρ（L（ffiJ））。通过构造，我们有L（ffiJ）<$L（ffi）。因此，我们有ρ（L（ffiJ））<$ρ（L（ffi））。让我们证明逆包含。设x∈ρ（L（ffi））.存在σ∈L（ffi）使得x=ρ（σ）.作为L（ffi）。0 = L（ffi），我们有σ。0 m−[|σ|]∈L（ffi）. 作为J. Leroux / Electronic Notes in Theoretical Computer Science 98（2004）89-950σ的长度0 m−[|σ|]可以被m整除，我们证明了σ. 0 m−[|σ|]∈L（ffiJ）.从x = ρ（σ）= λσ（0，.，0）= λσ（λm−[σ]（0，.，0））= ρ（σ. 0m−[σ]）∈ρ（L（ffiJ）），我们推出ρ（L（ffi））<$ρ（L（ffiJ））.因此，ffiJ是表示X的NDD。Q5由二元自动机表示的向量集的一种可压缩包。证明了由二元自动机ffi表示的向量集的A-壳是多项式时间可计算的。这是通过用一些a-drone空间标记ffi的状态得到的a-drone壳：a-drone覆盖。定义5.1二元自动机ffi=（Q，R， R，Q0，F）的一个复盖是一个复盖空间序列（Aq）q∈Q，Qm使得：• 对于每个状态qf∈F，我们有（0，.，0）∈Aqf，且• 对于每条路径q−→σqJ，则有λσ（AqJ）<$Aq。任何二元自动机ffi都至少有一个α-复盖（Aq）q∈Q，因为对每个q∈Q，Aq=Qm在α-复盖中。因此，下面的序列（cov（ffi）q）q∈Q被定义。cov（ffi）q=Aq（Ap）p∈Q是一个复盖引理5.2对于任意二元自动机ffi，序列（cov（ffi）q）q∈Q是ffi的一个非线性覆盖。证据我们记S为ffi的一个复盖的集合。由于任何一个交空间都是一个交空间，所以（cov（ffi）q）q∈Q是一个交空间序列。此外，对于每个qf∈ F，我们有（0，. ，0）∈ cov（ffi）q因为对于每一个（Ap）p∈Q在S中，我们有（0，.，0）∈Aqf。现在，letusconsiderap athq−→qJ.由于λσ是一对一函数，我们有λσ（cov（ffi）qJ）=λσ（（Ap）p∈Q∈SAqJ）=（Ap）p∈Q∈Sλσ（AqJ）<$（Ap）p∈Q∈SAq= cov（ffi）q.Q Q如前一引理所证明的，序列（cov（ffi）q）q∈Q是一个非线性覆盖。σF96J. Leroux / Electronic Notes in Theoretical Computer Science 98（2004）89-σ−−→FF定义5.3二元自动机ffi的最小覆盖是覆盖空间（cov（ffi）q）q∈Q的序列。从二元自动机的最小一个复盖，下面的命题5.4证明了我们可以计算二元自动机接受的向量集的一个复盖。命题5.4对于任何二元自动机ffi，我们有：（1）A（1）A（ 2）A（q0∈Q0cov（ffi）q0）我的律师。 对于q∈Q，我们成立X={ρ（σ）;q−→q;q∈qf fF}Nm. 首先证明了对任意q∈Q，cov（ffi）q= a ∈（Xq）.为了证明cov（ffi）q∈a <$a <$（Xq），我们证明了（a <$（Xq））q∈Q是一个α-覆盖. 对于每个qf∈ F，我们有（0，. ，0）= ρ（λ）∈ Xqf. 让我们considerap athq−→σqJJσJ和一个向量x∈XqJ。 存在一个状态qf∈F，Jap a thq−→qfsuchth a tx=ρ（σ）。 注：λσ（x）=λσ（λσJ（0， . 。，0））=ρ（σσJ）。As qσ.σJqf是一条路，我们有λσ（十） = ρ（σσJ）∈Xq.因此λσ（XqJ）<$Xq.因此a <$（λσ（XqJ））<$a <$（Xq）。由于λσ是一个α-σ，表示“功能”之义因此，我们有a <$（λσ（XqJ））=λσ（a <$（XqJ））。 我们证明了（a ∈（Xq））q∈Q是一个α-覆盖.利用序列（cov（ffi）q）q∈Q的极小性，证明了对任意q∈Q，cov（ffi）q∈a <$（Xq）.为了证明对每个q∈Q，a ∈（Xq）∈cov（ffi）q，我们证明Xq∈σcov（ffi）q，其中q∈Q. Letx∈Xq. 这里ex是一条路径q−→qf，其中hqf∈F使得x=ρ（σ）. 当（cov（ffi）q）q∈Q是一个非线性覆盖时，我们有（0，. ，0）∈ cov（ffi）q和λσ（cov（ffi）q）<$cov（ffi）q. 因此x = ρ（σ）=λσ（0，.，0）∈ cov（ffi）q.因此Xqcov（ffi）q。当cov（ffi）q是一个a-n空间时，我们证明了一个a-n（Xq）≠cov（ffi）q.因此，对于每个q∈Q，我们有一个（Xq）= cov（ffi）q。现在，请注意：（1）A（1）A（ 2）A（q0∈Q02016年01月03日@上午11时05分（q0∈Q02016年01月03日@上午11时05分（q0∈Q0J. Leroux / Electronic Notes in Theoretical Computer Science 98（2004）89-97Xq0）a（Xq0））cov（ffi）q0）因此，我们结束了Q98J. Leroux / Electronic Notes in Theoretical Computer Science 98（2004）89-我RBR算法1计算由a二进制自动机1：输入：二进制自动机ffi=（Q，R， R，Q0，F）。第二章： 输出量： a_n空间a_n（ρ（L（ffi）.3：{0，.，0）}如果q∈ F4：设（Aq）q∈Q是定义为Aq=q否则，5：当有existsq−→b时 QJ其中λb（AqJ）/<$Aq满足6： Aq<$a <$（Aq<$λb（AqJ））7：返回一个字符串（q0∈Q0Aq0）通过使用定点算法，我们在多项式时间内计算二元自动机的覆盖，如以下定理所证明的定理5.5算法1在多项式时间内计算二元自动机ffi接受的向量集的一个包。证据 我们首先证明第6行最多执行（m + 1）。卡（Q）次。 事实上，注意每执行一次第6行，a-logne空间Aq的维数严格增加。当一个Qm的空间的维数在有限集合{− 1，.，m}，我们得到了结果。为了证明该算法的复杂性是多项式的，我们证明了由该算法计算的空间的表示是集合{0，...， R2. 卡（Q）−1}m。我们证明了用该算法计算出的A的空间A的表示X是{ρ（σ）;σ∈ [ 1]中至多m+1个向量的有限子集n ≤（m+1）。卡（Q）}。为此，我们表示为（Ai）A型空间序列rqq∈ Q（Aq）q∈Q在第5行上，是i≥0的次数的函数，循环已执行。 我们用Xi表示Ai的表示。 让我们Q Q通过在i≥0上的归纳法证明了对任意q∈Q，Xq是{ρ（σ）;σ∈ φ≤i}中至多m+ 1个向量的有限子集.注意，归纳在秩i= 0时为真。假设归纳在秩i≥0时为真，让我们证明归纳在秩i+1上保持为真。Remarkthatthereexistsq−→qJinsuch对每一个p∈Q/{q}，我们有Ai+1=Ai和Ai+1= a <$（Ai<$λb（AiJ））。p p q q q因此，对于每个pi=q，我们有Xi+1=Xi和Xi+1<$Xi<$λb（XiJ）。通过p p q q q利用秩i上的归纳法，我们得到了Xi+1<${ρ（σ）;σ∈<$≤i+1}，对于每个p rp∈Q。 在那里，我们证明了秩i+ 1的归纳。 我们已经证明感应。特别地，当i ≤（m +1）时。卡（Q）的方法，我们证明了用该算法计算的代数空间的表示X是{ρ（σ）; σ∈ φ ≤（m+1）中至多m + 1个向量的有限子集。卡（Q）}。J. Leroux / Electronic Notes in Theoretical Computer Science 98（2004）89-99RRFB现在让我们证明{ρ（σ）; σ∈Σ ≤ （m+1 ） 。 card （ Q）}{0，.，R2. 卡 （ Q ）−1}m。让我们考虑σ ∈ φ ≤（m+1）。卡（Q）。 存在i ≥ 0使得σ。0 i是长度为m的字。二、卡（Q）。因此，ρ（σ）∈ {0，.，R2. 卡（Q）− 1}m。我们证明了用该算法计算的空间至多由{0，.，r2。卡（Q）}m. 因此，算法的复杂性是多项式的。为了证明算法的正确性，我们首先证明以下断言是一个不变量：“A q cov（ffi）q，对于每个q ∈ Q和（0，.，0）∈Aq，对任意qf∈F“.注意，在第4行执行之后，断言为真。因此，假设在执行第6行之前断言为真，让我们前提是这一点在之后仍然是正确的。Letq−→qJe是跃迁在1999年。当（cov（ffi）q）q∈Q是一个非线性覆盖时，我们有λb（cov（ffi）QJ）λcov（ffi）q。从这个断言我们推出λb（AQJ）cov（ffi）q。此外，该断言还给出了Aqcov（ffi）q。因此Aq<$λb（AqJ）<$cov（ffi）q。通过考虑前一个包含的a-壳，我们得到了一个<$（Aq<$λb（AQJ））<$cov（ffi）q.因此，断言是算法的不变量。特别地，在第7行，我们有Aqcov（ffi）q，对于每个q∈Q和（0，..，0）∈Aqf，对每个qf∈F.然而，在这条线上，while condi-第5行不再有效。 因此，对于每个q−→bq，j，我们有σJλb（AqJ）<$Aq. 利用归纳法，对每条路径q−→q，得到λσ（Aqj）<$Aq.此外，作为（0，.，0）∈Aqf，证明了（Aq）q∈Q是一个α-覆盖. 因此，对于每个q∈Q，我们有cov（ffi）q<$Aq。 我们对第7行上的每个q∈Q，推出Aq= cov（ffi）q1.5.4在第7行上，我们有一个boundary（q0∈Q0Aq0）= a（ρ（L（ffi）.Q6应用程序.我们研究Petri网的一个自然扩展，有效的计数器系统，一类系统，它包含了所有的计数器系统研究的FAST和LASH。对于这些系统，我们自然地扩展了位置不变量的定义，并证明了这些不变量的计算保持多项式。在第6.1小节中，我们证明了可以在多项式时间内一步计算计数器系统的可达关系的可达关系的可达壳的函数。这个多项式时间复杂度将在下一节6.2中解释。 事实上，我们展示了一个计数器系统的可达性关系和一个自然扩展的地方不变量之间的多项式时间联系。在6.3小节中，我们证明了有效计数器系统的位置不变量可以在多项式时间内计算。100J. Leroux / Electronic Notes in Theoretical Computer Science 98（2004）89-SSnSS6.1计数器系统可达关系的一个可达壳在这一小节中，我们证明了计数器系统的可达关系的可达壳可以在多项式时间内以可达关系的可达壳的函数一步计算计数器系统是一种通用模型，用于表示使用m个整数变量，并且具有有限的动作集合n，使得在执行动作a∈n之后计数器的新值xJ∈Nm与计数器的当前值x∈Nm通过Nm上的二元关系xRaxJ相关。定义6.1计数器系统S是一个元组S=（Nm，n，（Ra）a∈n），其中n是有限作用集，（Ra）a∈n是Nm上的二元关系序列.与计数器系统S相关联的一步可达性关系是二元关系记作RS，定义为RS=a∈<$Ra。 达性与计数器系统S相关联的二元关系是二元关系R=一步可达关系的自反传递闭包注：xR<$xJi <$n中存在n≥0个作用的有限序列（ai）1≤i≤n，Nm中存在向量序列（xi）0≤i≤n，使得x=x0，x0Ra1x1，.xn−1Raxn且xn=xJ。可达性问题包括决定计数器系统S和Nm中的两个向量x和xJ，如果我们有xR<$xJ。 回想一下，这个问题对于重置/转移Petri网类是不可判定的[15]，这是反制由于这个原因，我们感兴趣的可达性关系的过近似的计算，很容易计算。下面的命题证明，I_R_S提供了可达关系R_S的一个可达壳。命题6.2对于Qm上的任何二元关系R，我们有a（R）= a（IR）证据从I<$R <$R <$，我们推出一个<$（I<$R）<$a<$（R<$）。为了证明这个逆，我们首先证明了一个A（IR）是一个传递关系。让我们考虑（x，xJ）和（xJ，xJJ）在一个矩阵（I<$R）中。注意，如果x=xJ=xJJ，则（x，xJJ）=（xJ，xJ）∈I<$a<$（I<$R）.因此，我们可以假设x xJ或xJ/=xJ。则下列线性系统的秩等于2，因此至少有一个解（α，β，γ）∈Q3。。α+β.x+γ.xJ=xα+β.xJ+γ.xJJ=xJJJ. Leroux / Electronic Notes in Theoretical Computer Science 98（2004）89-101SSSSS设δ= 1−（α+β+γ）。由α + β + γ + δ = 1，当（1，1），（x， XJ），（XJ，XJJ）和（0，0）都在一个空间a ∈（I∈ R）中时，我们推出（x，XJJ）= α. （1，1）+ β。（x，xJ）+ γ. （xJ，xJJ）+ δ. （0，0）∈a ∈（I∈R）.因此，我们证明了关系a（IR）是传递的。由Ra（IR）和a（IR）的传递性，我们推出R aa bcd e 因此，一个（R）a（IR）。Q前面的命题表明，R的a ne壳等于S一艘“伊尔-S”号潜艇的船身。 由a <$（I<$RS）= a <$（Ia∈<$a<$（Ra）），我们推出下列推论：推论6.3计数器系统S的可达关系的可达壳可以在多项式时间内由a可达空间序列（a可达（Ra））a∈A计算。6.2位置不变量的定义。在这一节中，我们将展示一个空间（R）和位置计数器系统的不变量。我们以一种自然的方式稍微扩展了[11定义6.4计数器系统S的位置不变量是一个线性函数l：Qm→Q，使得对于每个a∈Q，并且对于每个满足xRaxJ的（x，xJ），我们有l（x）=l（xJ）。计数器系统S的位置不变量的集合被写为inv（S）。注6.5计数器系统S的位置不变量的集合是一个α空间（甚至是向量空间）。下面的命题证明了inv（S）和a rm（Rrm）之间的联系，通过证明位置不变量的集合inv（S）可以在多项式时间内从rm（Rrm）计算，并且rm（Rrm）可以在多项式时间内从S Sinv（S）.命题6.6对于任何计数器系统S，我们有：。a_i（R_i）={（x，x_J）;l（x）=l（x_J）<$l∈inv（S）}inv（S）={线性函数l：Qm→Q;l（x）=l（xJ）<$（x，xJ）∈a <$（R<$）}证据 我们首先证明等式a ∈（R ∈）={（x，xJ）; l（x）=l（xJ）<$l∈inv（S）}。设（x0，xJ）∈a（R），证明对任意l∈inv（S），有0秒l（x0）=l（xJ）。 由命题6.2，我们有（x0，XJ）∈a <$（I<$RS）。0 0102J. Leroux / Electronic Notes in Theoretical Computer Science 98（2004）89-SS000SSSSr∈存在t∈Q，序列e（t∈a）a∈Q，向量r（x，x）∈I，序列d（（xa，XJ））a∈Ra，使得t +ta= 1且（x0，XJ）= t. （x，x）+J.J.a∈0a∈A. （xa，xa）。 设l∈i nv（S）. 通过对虚拟现实中的场景的定义，l（xa）=l（xJ），对每个a∈n. 因此，我们有l（x0）=l（t.x+ta.xa）=拉瓜t.l（x）+Σta.l（xa）=t.l（x）+Σta.l（xJ）=l（t.x+a∈ta.xJ）=l（xJ）。a∈a∈a∈a0因此，我们证明了包含a <$（R<$）<${（x，xJ）;l（x）=l（xJ）<$l∈inv（S）}。 让我们证明相反的情况。让我们考虑（x0，XJ）/∈a <$（R<$）。 在这种情况下，存在一个a0秒函数f：Qm× Qm→ Q使得对每个（x，XJ）∈ a ∈（R ∈），f（x，xj）=0，且使得f（x0，XJ）= 0. 当f是一个线性函数时，存在两个线性函数l和lJ以及一个有理函数c ∈ Q，使得对于每个（x，xJ）∈ Qm× Qm，我们有f（x，xJ）= l（x）−lJ（xJ）+c。从（x，x）∈I<$a <$（R <$）我们推出0 =f（x，x）= l（x）−lJ（xJ）+c。因此，l=lJ，c= 0。此外，对于每个a∈R，对于每个（x，xJ）∈Ra，我们有0=f（x，xJ）= l（x）− l（xJ）。因此l∈inv（S）。 从f（x0，xJ）0，我们推出l（x0）/= l（xJ）. 我们有证明了包含{（x，XJ）;l（x）=l（XJ）<$l∈inv（S）}<$a <$（R<$）.我们推导出第一个等式a（R）={（x，xJ）;l（x）=l（xJ）<$l∈inv（S）}。现在，让我们证明第二个等式。设l∈inv（S）.根据前面的等式，我们有l（x）=l（xJ），对于每个（x，xJ）∈a（R）。 因此，inv（S）{线性函数l：Qm→Q; l（x）= l（xJ）<$（x，xJ）∈ a <$（R <$）}.对于逆包含，让我们考虑线性函数l，使得l（x）=l（xJ），每个（x，XJ）∈a ∈（R∈）.从RS<$a <$（R<$），我们推出，对于每个a∈<$S S对每个（x，XJ）∈Ra，有l（x）=l（XJ）.因此l∈inv（S）。我们证明了第二个等式。Q6.3有效的计数器系统。在这一小节中，我们定义了有效计数器系统的类，并证明了可达关系的A-壳是多项式时间内可计算的。 作为推论，我们证明了一个E-1的位置不变量的集合， 动态计数器系统在多项式时间内是可计算的。最后，我们提出的结果，通过实施这些结果在我们的工具FAST。像FAST或LASH这样的工具将一类计数器系统作为输入，使得每个二元关系Ra由BA-a双线性函数fa表示。定义6.7一个BA-一个多项式函数f是一个元组（ffi，M，v），使得ffi是一个二元自动机，M∈Mm（Q）是一个方阵，v∈Qm是一个向量。与BA-a-n关系f相关联的关系Rf定义为：xRfxJxJ=M.x+v且x∈ρ（L（ffi））定义6.8有效计数器系统S是一个计数器系统S=（Nm，N，Rm）一J. Leroux / Electronic Notes in Theoretical Computer Science 98（2004）89-103S使得每个二元关系Ra要么由二元自动机ffia表示，使得Ra=ρ（L（ffia））<$N2.m，要么由BA-a-函数fa表示，使得Ra=Rfa。对于有效计数器系统，计算位置不变量的复杂性，已知是多项式时间的Petri网仍然是多项式时间。定理6.9一个有效计数器系统的可达性关系的一个可达性壳是在多项式时间内可计算的。证据由定理6.2，我们证明了a（R）等于a（I<$RS）。S注：a（I<$RS）= a（Ia∈a <$（Ra））。设a∈n;二元关系Ra可以用二元自动机ffia表示，也可以用BA-a的双线性函数fa表示。如果Ra由二元自动机ffia表示，定理5.5证明了一个可计算空间a_n（Ra）在多项式时间内是可计算的。假设Ra由BA-α双线性函数fa=（ffia，Ma，va）表示。定理5.5证明了a（ρ（L（ffia）在多项式时间内是可计算的。因此，a ∈（Rfa）=（a ∈（ρ（L（ffia）×Qm）<${（x，xJ）∈Qm×Qm;xJ=Ma.x+va}是多项式时间可计算的。因此，我们可以在多项式时间内为每个动作a ∈a计算aa∈ a（Ra）。我们已经证明了我们可以在多项式时间内计算出一个R（R）。Q从命题6.6和前面的定理出发，我们推出一个有效计数器系统的位置不变量是多项式时间可计算的。推论6.10一个有效计数器系统的位置不变量的集合在多项式时间内是可计算的。我们已经实现了一个二进制自动机作为我们的符号模型检查器Fast的插件的覆盖计算的一个简单的。用FAST计算40个计数器系统的位置不变量需要1分钟到1小时。然而，这种时间复杂度并不对应于优化算法的时间复杂度。事实上，我们非常确定计算这些位置不变量所需的时间可以减少到不到一秒。因此，没有提供基准。一旦该算法在快速网页www.lsv.ens-cachan.fr/fast/上进行优化，具有不变量的FAST将立即可用结论我们已经提出了一类二进制自动机，一个新的表示子集的Nm，自然扩展的NDD。我们已经证明，104J. Leroux / Electronic Notes in Theoretical Computer Science 98（2004）89-由二进制自动机表示的向量集的外壳是可计算的 多项式时间。我们介绍了有效计数器系统的模型。我们已经证明，我们可以将位置不变量的定义扩展到这个新类。对于这类有效计数器系统，位置不变量的计算仍然是多项式时间。所有的算法都已经在C++中实现，作为FAST的插件，它们应该很快就可以使用了。引用[1] Abdulla ， P. A. ， A. Bouajjani 和 B. Jonsson ， On-the-fly analysis of systems withunbounded，lossy FIFO channels，in：Proc. 10th Int. Conf. Computer Aided Verification（CAV305-318[2] Abdulla，P. A.和B. Jonsson，具有不可靠信道的非线性程序，在：Proc.8th IEEE Symp. Logicin Computer Science（LICS '93），Montreal，Canada，June 1993（1993），pp. 160-170.[3] Ammirati，P.，G. Delzanno，P. Ganty，G. Geeraerts，J. F.拉斯金和L. V. Begin，Babylon：参数化系统规范和验证的集成工具包，在：G。德尔赞诺，S. Etalle和M. Gabbrielli，editors，Specification，Analysis and Validation for EmergingTechnologies in Computational Logic，Datalogiske Skrifter94，2002，p. （未分页）。[4] Annichini，A.，A. Bouajjani和M. Sighireanu，TReX：复杂系统的可达性分析工具，在：Proc.13th Int.Conf.Computer Aided Verification（CAV368-372.[5] 巴比伦，http://www.ulb.ac.be/di/ssd/lvbegin/CST/index.html网站。[6] Bardin，S.，A. Finkel，J. Leroux和L. Petrucci，FAST：符号转换系统的快速加速，在：Proc.15th Int.Conf.Computer Aided Verification（CAV118-121[7] Berthelot，G.， 适用议定书”。是的，乌尼夫。第五部分，1983年，无争议，第16页。[8] Boigelot，B.，在可识别的整数集上迭代线性变换，理论计算机科学。出现。[9] Boigelot，B. ，“用于E x p l o r i