BPP与有限态系统互模拟等价性问题的多项式时间解法及算法构造

理论计算机科学电子笔记138（2005）49-60www.elsevier.com/locate/entcsBPP和有限状态系统的互模拟等价性可以在多项式时间MartinKot1，ZdenekSawa2，3俄斯特拉发技术大学计算机科学系17. listopadu 15，70833 Ostrava-Poruba，Czech Republic摘要本文考虑了BPP与有限态系统互模拟等价性的判定问题我们证明了这个问题可以在多项式时间内解决，我们提出了一个算法，决定了时间O（n4）的问题。该算法还为有限状态系统的每个状态构造了BPP系统的所有状态的集合的“符号”半线性表示，这些状态关键词：互模拟等价，基本并行过程，有限状态过程1引言互模拟等价也称为双相似性，是自动验证领域中研究的最重要的行为等价之一。基本并行过程（BPP）是一类研究判定双相似性的无限状态系统。[ 2 ]证明了BPP上的双相似判定问题是可判定的，但没有给出复杂度的界。在文献 [8] 中 ， 我 们提出了这个问题是PSPACE 中的问题，而J.A.E.Hard最近在文献[4]中证明了这个问题是PSPACE中的问题，因此，1 电子邮件：martin. vsb.cz2电子邮件：zdenek. vsb.cz[3]这两位作者都得到了捷克共和国赠款机构的支持。201/03/11611571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.02.06550M. Kot，Z.Sawa/Electronic Notes in Theoretical Computer Science 138（2005）49S12S121一2是PSPACE-完整的。多项式时间算法已知用于赋范BPP的情况[3，6]。在本文中，我们提出了一个算法的特殊情况下的问题之一（无范）的过程是一个有限状态的过程。该算法的运行时间为O（n4），其中n是实例的大小。这个结果意味着可以在多项式时间内验证一个实现为有限状态自动机的系统是否等价于一个 该算法还为有限状态系统的每个状态生成本文的组织如下：在第2节中，我们提供了一些基本的定义，并制定了本文的主要结果。在第三节中，我们描述了算法的主要思想，并证明了它的正确性。在第4节中，我们分析了算法的时间复杂度。第五部分是结论和未来工作的方向。2基本定义标号转移系统（LTS）是一个元组（S，A，−→），其中S是一个（可能是无限的）状态集，A是一个有限的动作集，−→S×A ×S是一个这是一个很好的例子。 我们记为s−→asJinsteadof（s，a，sJ）∈−→。我们一起来吧符号also表示作用的有限个等式，并且对于w∈A，wewrites−w→sJ如果w = a1a2. 有一些状态s0，s1，. ，s n使得s = s0，sJ=sn和si−1 −a→i对于每个0 0}。对于p∈P，我们定义SUCC（p）={t∈Tr|PRE（t）= p}。我们还将符号PRE（t）扩展到转移集，并且对于T∈Tr，定义PRE（T）={p|t∈T：p= PRE（t）}。设P={p1，p2，.，p，k}是位置的集合。 一个标记是一个函数M：P→N，它为每个位置分配了标记的数量。标记M可以被视为向量（x1，x2，.，xk），其中xi∈ N且xi=M（pi）. 我们用M表示所有标记的集合。在M∈Mi <$M（PRE（t））>0中启用转变t 未启用的转换将被禁用。启用的转换可以执行、写入M−→tMJ在哪⎧<$M（p）−1+F（t，p）ifp =PRE（t）MJ（p）=M（p）+F（t，p）否则BPP产生LTS（S，A，−→），其中S=M，且M−→aMJi有一些t∈TrsuchthatM−→tMJ和λ（t）= a.有限状态系统（FS）通常被定义为LTS（S，A，−→）。其中S是有限的，但为了技术方便，我们将其定义为BPP，其中对于每个t∈Tr，恰好有一个p∈P，使得F（t，p）= 1且F（t，pJ）= 0如果pJ p.对于p∈P，我们定义一个标记M p，使得M p（p）= 1，对于pJ，M p（pJ）= 0p. 我们称这种标记为FS标记。给定BPP <$1=（P1，Tr1，PRE1，F1，λ1）和<$2=（P2，Tr2，PRE2，F2，λ2），其中P1，P2，Tr1和Tr2是不相交的，它们的不相交并集是BPP <$1 =（P，Tr，PRE，F，λ），其中P=P1<$P2，Tr=Tr1<$Tr2，并且PRE、F和λ以明显的方式定义。通过将所有剩余元素设置为0，可以将标记“1”和“2”问题BPP-BISIM可以公式化如下：给定两个BPP系统，101和102，具有101和102的区别标记M1和M2，M1=M2？（关系被定义为1和2的不相交并集。本文考虑了BPP-FS -BISIM问题，它是bpp - fs - bisim问题的一个特殊情况。BPP-BISIM，其中，M1是一个有限状态系统，M1是一个FS标记。我们证明了问题BPP-FS-BISIM可以在O（n4）的时间内解决，其中n是52M. Kot，Z.Sawa/Electronic Notes in Theoretical Computer Science 138（2005）49实例的大小。我们假设实例中的BPP被编码为位置和转换的列表，其中每个转换t的编码包含所有p∈SUCC（t）以及值F（t，p）的列表。我们假设数字是用二进制编码的。在本文的其余部分中，<$p =（P，Tr，PRE，F，λ）是BPP和来自BPP-FS-BISIM实例的FS的不交并，M表示其标记集，PFS和TrFS是来自该实例的FS的位置和转移的集合（PFS<$P，TrFS<$Tr），并且Mp其中p∈PFS表示标记使得Mp∈ M，Mp（p）= 1并且Mp（pJ）= 0，对于pJ/=p。 我们定义MFS={M p|p∈P FS}。符 号 ω 表 示 无 限 性 。 我 们 规 定 ， 对 于 每 个 x∈N ， x ω ，ω+x=x+ω=ω+ω=ω−ω=−ω+ω=ω ， ω·0 = 0·ω= 0 ， 对 于 每 个 x≥1 ，ω·x=x·ω=ω。我们定义Nω=N <${ω}。让你成为一个集合。 |表示U的基数。|denotes the cardinality of U . U的划分U是一个集合U ={U1，U2，.，U 1}的不相交非空类，其并集是U。3该算法本文采用JanJiang[4]中的方法，证明了在PSPACE中存在BPP-BISIM。其基本思想是构造一系列用于近似互模拟等价的范数函数。当没有其他功能可以添加时，构造停止，此时近似是精确的。首先，我们回顾一下[4]中的一些观点。设（S，A，−→）是一个LTS，C：S→D是一个映射，它从定义域D中为每个状态赋值。我们称映射C是双必要的，如果对每个s，SJ∈S，s∈SJ蕴涵C（s）=C（SJ）. 如果我们有一组函数{C1，C2， .. . 当Ci：S→Di时，我们说这个集合是双必要的，即每个Ci都是双必要的。S上的一个谓词P可以看作是一个映射P：S→{0， 1}，因此我们也可以讨论双必要谓词。注意，如果P是双必要的，那么<$P也是双必要的。设P是S上的谓词。我们定义了映射DIST（P）：S→Nω，其中DIST（P）（s）是短序列w的长度，使得s−w→sJ和P（sJ），如果没有这样的w，则DIST（P）（s）=ω。直觉上，DIST（P）表示3.1如果P是双必要的，则DIST（P）是双必要的。证据 让我们不失一般性地假设存在状态s1，s2使得s1≠s2且DIST（P）（s1）DIST（P）（s2）。<然后有一些最短的w∈A<$suchthats1−w→sJ和P（sJ）。因为用户1和用户2都是相同的，1 1 2M. Kot，Z.Sawa/Electronic Notes in Theoretical Computer Science 138（2005）4953不不suchthats2−w→sJ且sJ<$sJ。 But|W|0。不难看出，E-CARR（L）是一个陷阱.回想一下，一组位置RP是一个陷阱it：PRE（t）∈R<$（R<$SUCC（t）<$）直观地说，这意味着从陷阱中移除令牌的每一个t也会向其添加至少有一个标记的陷阱，不能取消标记。由此得出以下主张：3.2若L=NORM（Q），对于某个Q∈P且L（M）=ω，则L（MJ）=对每个MJ满足that：M−w→MJ。对于线性函数L，我们可以对每个t∈Tr计算值Σ（一）δL=−ci+1≤j≤kcj·F（t，pj）其中PRE（t）=pi。 δL值当执行转换T表示L值的Claim3.3IfM−→tMJ则L（M）+ δ L= L（MJ）。 若L（M）<ω且δ 1 =δ L然后 L（M）+ δt tL（MJ）.54M. Kot，Z.Sawa/Electronic Notes in Theoretical Computer Science 138（2005）49对于每个p∈P，如果p∈Q则cp：=ωelsecp：= 0QJ：=QT：={t ∈ Tr |PRE（t）∈ QJ}当QJ/=Q d0时设pmin指某个p∈QJ具有极小cp对于每个t∈T，使得SUCC（t）<$QJ=<$do从T中删除tp：=PRE（t）;R：=SUCC（t）dt：= 1+q∈Rcq·F（t，q）如果dt cp，则cp：=dt如果cpcpmin thenpmin：=p端如果cpmin=ωthenbreak;QJ：=QJ− {pmin}每t从T中移除，使得PRE（t）=pminend whileFig. 1. 范数（Q）函数系数的计算现在我们来描述算法。 该算法构造了一组线性函数L ={L1，L2，. . }使得每个Li表示某个位置集合的范数，并且其中每个Li是双必要的。该算法从L=0开始，依次向L中加入一个线性函数，最后不再加入新的线性函数。 对于L，我们定义M上的等价 L，使得M<$LMJi <$<$L∈L：L（M）= L（MJ）。由于每个L∈L都是双必要的，所以L也是双必要的，并且dM/<$LMj 蕴涵M/<$MJ. 另一方面，证明了若M∈ MFS且MJ∈M，则M<$LMj蕴涵M<$ MJ.主要算法如下：1. S etL=0。2. 对于每个p∈PFS，执行下面描述的S步骤3. 如果L在上一步中已更改，则转到2。步骤如下：对于给定的p，我们定义集合F LsuchhatL∈Fi<$L（Mp）<ω. 对于F，我们定义了一个等式，Trsuchhatt=FtJiλ（t） =λ（tJ）anddL∈F：δL=δL. Let[t]denotet tJ该quivalenceclassoff=Fconntainingt. L etT1={[t]|t∈S UCC（p）}，andnd设T0=Tr−T∈T1T. 我们定义集合T为T=T1<${T0}，分别当T0为空时，T=T1 注意T是Tr的一个分区。 我们扩展了M. Kot，Z.Sawa/Electronic Notes in Theoretical Computer Science 138（2005）495521J线性函数集的广义CARR的定义及定义E-CARR（F）=E-CARR（L）L∈F该算法现在对每个T∈T计算函数L=NORM（PRE（T））并将其添加到L。我们现在证明算法是正确的。引理3.4算法中的每个L加到L上都是双必要的。证据 我们用归纳法来处理步 骤 的数目。命题在一开始是微不足道的。现在假设算法执行S步对某个p∈PFS，并对某个T∈ T，给L加上范数（Q），其中Q=PRE（T）∈R-CARR（F）.由于权利要求3.1，证明零（Q）是双必要的是足够的让我们不失一般性地假设M1<$M2，-零（Q）（M1）和零（Q）（M2）。通过归纳假设，证明了L∈ L：L（M1）=L（M2）.设R （F）.由于零（R）（M2），我们有<$L∈ F：L（M2）<ω，和零（R）（M1），因为否则存在某个L∈ F使得L（M1）= ω/= L（M2）。从这个和<$ZERO（Q）（M1），我们得到<$ZERO（PRE（T））（M1）。这意味着有一些过渡t∈T，tJ JtJM1−→M1 因为M1<$M2，存在某个t使得M2−→M2其中M2<$MJ且λ（t）= λ（TJ），但tj/∈T是必要的. 这意味着有某些L∈ F使得δLδL. 通过权利要求3.3，这意味着L（MJ）L（MJ），t tJ1 2矛盾Q由于每个L加到L上都是范数（Q），对于某个Q∈P，并且P是有限的，很明显算法在某个有限步数后停止。下面的引理表明，对应于由算法计算的L的LSL与其中一个标记来自MFS的标记对的LSL重合。引理3.5设L是由算法计算的集合。 则对于每个M1∈MFS且M2∈ M，M1<$LM2蕴涵M1<$M2.证据我们证明了，MFS× M是一个互模拟。设M1∈MFS，M2∈ M，使得M1<$LM2. 设F ={L∈ L|L（M1）<ω}，设R = Ω-CARR（F）.注意，对于某些p∈PFS，M1=Mp，当算法执行步骤S时，将产生相同的F对于p.注意零（R）（M1），因为否则存在某个L∈ F使得L（M1）=ω。零（R）（M2）也是真的，因为否则存在某个L∈F使得L（M2）=ω，这意味着L（M1）/=L（M2）。设T对F的定义与S步中的定义相同。t考虑M1−→的一个跃迁M.J. 设T是T的类，t∈T。 显然T∈ T1. 现在考虑函数L1=NORM（R≠不56M. Kot，Z.Sawa/Electronic Notes in Theoretical Computer Science 138（2005）49不不PRE（T））。 必须是L1∈ L的情况，否则L1可以加到L算法还没有完成所以L1（M1）=L1（M2）.从这个，从<$ZERO（PRE（T））（M1），并且从零（R）（M2），我们有<$ZERO（PRE（T））（M2）JtJJ JL且存在某个t∈T使得M2−→M2，λ（t）=λ（t），且<$L∈F：δt=δL由这一点和权利要求3.3，我们得到了<$L∈ F：L（MJ）=L（MJ）。为每个tJ1 2L∈ L-F是L（M1）=L（M2）=ω，并且根据权利要求3.2，L（MJ）=L（MJ）=ω。1 2这意味着MJLMJ。1 2tJJ现在考虑一个跃迁M2−→M2。这种情况类似于前-显然，情况下，但我们也必须考虑的可能性TJ∈T0。设L0=NORM（RPRE（T0））.由于L0∈L（否则算法尚未完成），则L0（M1）=L0（M2）.因为L0（M1）= 0，我们得到L0（M2）= 0，和零（PRE（T0））（M2），所以tJ在M2中不被使能，这是矛盾的。Q4算法的时间复杂度算法的时间复杂度为O（n）。 在本文的其余部分，n表示输入实例的大小算法的运行时间取决于S步的实现细节。在第3节中，我们描述了如何对给定的p∈PFS计算在S步集合F中，有n-CARR（F）和T。不重新计算这些集合，而是存储它们的值，并在新的L被添加到L时对它们执行必要的更改。 因此，该算法对每个p∈ P都保持了相应的F-CARR（F）和T的FS值.注意，T总是最多包含|SUCC（p）|+1等价类。该算法还保持了对每个T∈ T和对n-CARR（F）的布尔代数，自上次调用以来是否已更改S步并增加了一个新的函数L=NORM（f-CARR（F）f-T）到L只有当f-CARR（F）或T是新的或实际上已经改变。将L添加到L包括以下步骤：1. 计算系数c1，c2，.，c k的L.2. 计算每个t ∈ Tr的δ L。3. 根据δL和λ（t）的值划分Tr4. 对于每个p∈PFS，使得L（Mp）<ω：• 将L-CARR（L）加到相应的L-CARR（F）上。• 使用步骤3中计算的划分修改相应的T。在证明中，我们需要以下众所周知的事实：事实4.1设U是一个非空有限集，设U1，U2，.是序列每个Ui+1都 是U i的精化。那么总M. Kot，Z.Sawa/Electronic Notes in Theoretical Computer Science 138（2005）4957所有这些分区中的不同类的数量小于2·|U|.证明的想法。 使用归纳法|U|.Q因此，时间复杂度为O（n），时间复杂度为O（n）。证据 让我们考虑所有调用的S步骤为一个p ∈ P FS。在函数的调用中，如果F的值发生了变化，则算法对每个T∈T向L添加一个新的函数。如果f-CARR（F）没有变化，则对每个变化的T∈TC-CARR（F）只能增长，因此当C ++= O（|P|）.因为|不|（1）如果n = 1，则n = 1，|P|）.现在考虑T.或者某个t被加到T0上，或者某个T∈T1被分裂，或者这些可能性的某种组合已经发生。由于T0只能增长，第一种可能性只能发生O（|Tr|）倍。仍然需要从T1开始估计类的总数。在O（|Tr|）如下事实4.1所示，因为在后续的STEP调用中，T 1的值序列可以通过向每个T 1添加一些类来扩展为一个细化划分序列。现在让我们对所有p∈PFS，求加到L上的函数的个数之和。在其中A-CARR（F）改变的调用中，它至多是Σ（|SUCC（p）|1）O（|P|）= O（|P|·|Tr FS|）p∈PFS在剩余的调用中添加的函数数为O（|P FS|·|Tr|），所以我们得到函数的总数为O（|P|·|Tr|）.Q现在我们考虑对于某些Q范数P，L=NORM（Q）的系数的计算复杂性。对于x∈Nω，size（x）表示以二进制编码时x的位数。我们假设size（x+y）=1+ max{size（x），size（y）}，size（x·y）=size（x）+size（y），size（ω）=O（1）。对于任意p ∈ P，size（cp）都是O（n）的。证据 设p1，p2，. ，pl是从Q开始的位置的序列，按照算法确定它们的系数的顺序进行排序，令ci是pi的系数，并且令ti是用于计算ci的转换，即， 转换such具有PR（ti）=pi和ci=di，其中我们用di代替di。Letsize（t）是t∈T的表示的比特数，即，Σ时间复杂度：O（1 + 1）|R|）·size（|P|））+其中R=SUCC（t）。p∈Rsize（F（t，p））58M. Kot，Z.Sawa/Electronic Notes in Theoretical Computer Science 138（2005）49不不不通过归纳总结，提出了以下几点建议直接遵循： 对于每个i，1≤i≤l，size（ci）≤1≤j≤isize（tj）。这因为c1总是1或ω，所以假设i>1。让R=SUCC（ti）。注意di= 1 + Σq∈RΣi−1cq·F（ti，q）≤1+j=1cj·F（ti，pj）因为当计算di时，每个cq都是已知且有限的，所以它要么是0，要么是从c1到ci−1的1。size（cj·F（ti，pj））=size（cj）+size（F（ti，pj））。所有这些乘积的总和可以写成最大值加上小于他们的行为（由于添加而导致的）。此大小小于n大小（max{cj|1≤j i}）+i−1size（F（t，p））.第二个被加数（和）小于j=1i j然后是size（ti）。通过归纳假设，最大cj可以写在计数中，第一个i-1转换所需的位数。因此，d i（因此c i也是）可以写在表示转换t1，.，t i. Q命题4.4 L = NORM（Q）的所有系数都是在O（n2）内计算的。证据最耗时的步骤是计算所有di。在计算中，乘法比加法更耗时。因此，它的表面上显示，所有乘法的聚合复杂度是在O（n2）.在我们的算法中，每个di只计算一次。 在计算di时，我们需要确定所有乘积F（ti，pj）·cj，其中pj∈SUCC（t）。从命题4.3我们知道，对于每个cj，size（cj）都是O（n）。因此，一个乘积的计算时间为O（n·size（F（ti，pj）。如果我们对所有转换和转换给出标记的位置的此类乘积的复杂度求和，我们得到所有乘法Σ ΣO（（n·size（F（ti，pj）=O（n·size（F（ti，pj）=O（n2）i，j i，j.Q命题4.5对于给定的L=NORM（Q），由所有transi引起的变化δL时间复杂度为O（n2）。证据 对于每个过渡t，值δ L使用表达式1计算从第3节。 如果某个cj无穷大，则δL也是无限的。所以我们做只计算有限值的总和。 加法的复杂度由乘法的复杂度cj·F（t，pj）决定。每个这样的乘积只计算一次。这样的话，时间复杂度是O（n）的。每个F（t，p，j）只使用一次，并且是我们表示的一部分M. Kot，Z.Sawa/Electronic Notes in Theoretical Computer Science 138（2005）4959不关于BPP因此，我们可以类似于命题4.4中的系数推导出所有乘法的聚合复杂度是O（n2），由此得出以下结果。Q这个算法的时间复杂度为O（n2）。证据这样，时间复杂度为O（n2），时间复杂度为O（n2）。步骤3的运行时间也是O（n2），使用字符串的字典排序的标准算法之一（参见[1，7]），因为δL的值可以表示为二进制数，即，作为0和1的字符串。而且如果仔细执行的话，第4步的运行时间是O（n2）Q定理4.7存在一个求解BPP-FS-BISIM的算法，时间复杂度为O（n4）。证据我们已经描述了算法。引理3.4和3.5保证了算法的正确性。 由于增加新的L到L是算法中最耗时的操作，因此从引理4.2和4.6可以得出算法的运行时间是O（n4）。Q5结论与未来工作在本文中，我们已经提出了一个算法，以确定BPP和有限状态系统之间的双相似性的时间复杂度为O（n4）。然而，该算法的时间复杂度可能不是最优的，并且可以进一步改进。可以使用本文中使用的来自[4]的技术的其他问题是确定BPP系统的正则性的问题，即，对于给定的BPP过程是否存在双相似有限状态过程的问题这个问题已知是可判定的[5]和PSPACE-hard [8]，但没有上限已知的问题。我们推测，这个问题是在PSPACE，我们计划在未来展示它引用[1] Aho，A.五、J. E. Hopcroft和J.D. Ullman，[2] 克里斯滕森，S.，Y. Hirsfeld和F. Moller，互模拟对于所有基本并行过程是可判定的，在：Proc.CONCUR143-157[3] Hirsfeld，Y.，M. Jerrum和F. Moller，一种判定赋范基本并行过程，计算机科学中的数学结构6（1996），pp.251-259[4] JanP.，在Proc中，在BasicparalelprocessesisPSPACE-complete中，Strongbismil aryyynbas icpa ra l elp r oce s i s P S P A CE-complete。 18thLiCS（2003），pp. 218-22760M. Kot，Z.Sawa/Electronic Notes in Theoretical Computer Science 138（2005）49[5] JanP. 和J。 因此，Decidingitenesofetrinesuptobis imul ation，in：P roc. *ICALP'96，LNCS1099（1996），pp. 478-489.[6] JanP. 和 M.Kot ，B是 一个非线性的最小的基函数，它的概率可在O（ n3） 中 确 定 ， 在 R.Bharadwaj ， 编 辑 ， Proceedings of the Third International Workshop on AutomatedVerification of Infinite-State Systems[7] 佩奇河和R.E. Tarjan，三种分区细化算法，SIAM计算杂志16（1987），pp. 973-989.[8] Srba，J.，基本并行过程的强双相似性和规则性是PSPACE-困难的，在：Proc. STACS535-546.