无限域下推自动机与Petri网弱双相似性问题的讨论

11理论计算机科学电子札记98（2004）5-19www.elsevier.com/locate/entcs不可判定双相似问题JirSrba1，2奥尔堡大学计算机科学系Fredrik Bajersvej 7E，9220 Aalborg，Denmark摘要1我们建立了无限域弱双相似性检验的完备性（在层次分析中）下推自动机和并行下推自动机产生的状态过程。这些结果暗示了Petri网弱双相似性的完备性，并否定了J.A.A. P.（CAAP'9.5）的公开问题：“对于Petri网，弱双相似的概率是否是极小的？1#21011;保留字： 弱双相似，不可判定性，进程代数。1介绍给定两个（无限状态）进程，等价性检验问题是判断这两个进程在某些行为等价性方面是否等价。这个问题已经被深入研究了各种类型的无限状态系统（参见例如[1，8，12]的概述）。双向模拟等价的概念无论在理论上还是在实践上都具有特殊的意义已知Petri网（PN）的强（和弱）双相似性检验是不可判定的[6]。在强双相似性的情况下，问题在算术层次中是100-完全的（参见例如[5]），并且在弱的情况下，它是高度不可判定的[5]（即，它超越了算术层次）。1电子邮件：srba@brics.dk2 这项研究得到了GACR的部分支持，批准号为201/03/1161。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2003.10.0036J. Srba / Electronic Notes in Theoretical Computer Science 98（2004）5-11111=（另一方面，下推过程（PDA）的强双相似性检查仍然是可判定的[11]，而语言等价性则不是。PDA的弱双相似性问题最近被证明是不可判定的[14]，我们证明了这个问题超出了算术层次。在本文中，我们证实了这一猜想，我们加强了PDA和PN的弱双相似性的高不可判定性的结果，不仅在算术层次中的ω-硬度，而且在分析层次的第一级（ω1-硬度）。在Petri网的情况下，我们的证明推广的结果Jannovecar[5]also在另一种方式：结果是确定为PN的一个适当的子类称为并行下推过程（PPDA）或也多集自动机。至于上界，很容易观察到弱双相似。问题包含在[1]中（见[5]）。弱的完备性1 1建立PDA和PPDA（和PN）的双相似性一个有趣的观察是，PDA，PN和PPDA不是图灵强大的（例如。可达性仍然是可判定的[9]），但是弱双相似性问题仍然令人惊讶地高度不可判定。这些结果与理论中的其他结果相反。例如，PDA和PN的（弱）迹等价性检查仍然是完全的（参见[5]）。另一方面，对于称为基本并行进程的PN的无通信子类，强双相似性是PSPACE完备的[7，13]，弱双相似性很可能是可判定的，而其他等价，包括（强和弱）迹等价是不可判定的[4]。其实（强的和弱的）迹等价是0-完备的[5]。类似的令人惊讶的结果也适用于无状态PDA（称为基本进程代数），其中强双相似性在2-EXPTIME [2]中是可判定的，弱双相似性也被证明是可判定的，而（强和弱）迹等价是不可判定的（形式主义准确地描述了上下文无关语言的类别）。同样，（强和弱）迹等价的问题可以被看作是完全的使用[5]中的构造。2基本定义标号转移系统是一个三元组（S，Act，−→），其中S是一组状态(or 过程），Act是一组标签（或动作），− →S× Act×S 是一transit ionrelat ion，当α−→a时β，对于r（α，a，β）∈−→.假设动作集合Act包含一个特殊的无声动作τ。通过定义dy=a，我们可以转换为关系式=adef −→τ ）−→a◦（−τ→）π如果a∈Actz{τ}的def⇒=（−τ→）如果a=τ。设（S，Act，−→）是一个标号迁移系统. 二元关系R，且=J. Srba / Electronic Notes in Theoretical Computer Science 98（2004）5-73−i1J2S×S是一个弱互模拟i ∈，只要（α，β）∈R，则对于每个a∈ Act：若α−a→αJ，则nβ=αaβJ，其中βJ满足hat（αJ，βJ）∈R;且ndifβ−→aβJnα=π对于某个αJ使得（αJ，βJ）∈R.过程α和β是弱存在弱互模拟R使得（α，β）∈R.弱双相似性在互模拟博弈中有一个很好的刻画。一对进程α1和α2上的互模拟博弈是一个“攻击者”和“防御者”之间的两人博弈。 比赛分几轮进行。 在每一轮中，玩家根据以下规则改变当前状态β1和β2（最初为α1和α2(i) 攻击者选择ani∈ { 1， 2}，a∈ Act和βJ∈S使得aJiβi−→ βi。(ii) 通过选择aβJ∈S，满足β3−=π，我3− i.(iii) 状态βJ和βJ成为现在的国家。一局棋是由参与者根据上述规则形成的状态对的最大序列，并且从初始状态α1和α2开始。 防守者是每场比赛的胜利者。被卡住的玩家会输掉一场有限的比赛。下面的定理是一个标准的定理（见例[16，17]）。定理2.1当防御者有获胜策略时，过程α1和α2是弱双相似的（当攻击者有获胜策略时，过程α 1和α 2是非双相似的）。在下面的内容中，我们将经常使用一种叫做“防守者的选择”的技术。其思想是，在从α和β开始的双模拟博弈中，防御者可以迫使攻击者进行以下意义上的某种转移：如果攻击者采取任何其他可用的转移（从α或β），防御者总是可以以这样的方式回答，即所得过程是弱双相似的（因此攻击者输了）。一个典型的情况可能看起来像α，β，ACCCCca，a、、、，a一个，scJcJJ，vzJ vzαα1α 2β1β2其中αi<$βi，其中1≤i≤ 2（通常αi和βi在语法上是偶数）。很容易看出，在从α开始的互模拟博弈中，β使Δ cker（DC）进行α−→aαJ的转换。在所有可能的行动中，他立即输了。令Q={p，q，.. . }，r ={X，Y，.. . }和Act={a，b，.. . }是有限的集合分别控制状态、堆栈符号和动作，使得Qr =一一 β8J. Srba / Electronic Notes in Theoretical Computer Science 98（2004）5-一=我1==τ∈Act是著名的无声作用。 下推自动机（PDA）是一个关于p−→aqα或pX−→aqα的有限集合，a∈Act，p，q∈Q，α∈Γπ，X∈Γ.def一个下推自动机生成一个带标号的转移系统T（T）=（Q×Γ，Act，−→）其中Q×Γ是状态集3，Act是动作集，而跃迁rγ−→d是由预改写规则pγ−→a定义的qαγ若（p−→qα）∈α，则andpXγ−→aqαγif（pX−→aqα）∈<$，对所有的γ∈Γ<$.并行下推自动机（PPDA）的定义与PDA相同。唯一的区别是PPDA系统生成的转移系统的状态被认为是栈符号合成的算子的模交换性。因此，而不是顺序访问堆栈（如在PDA的情况下），我们有一个并行访问存储在堆栈中的所有符号和堆栈可以被视为一个多组堆栈符号。Example2.2Letdef{pX−→aq}。F或PPDAt这里是跃迁pYX−→aqY，但当将qY解释为PDA时，没有这样的转变。备注2.3为技术方便（和w.l.o.g.）PDA和PPDA重写规则以比通常稍微更一般的形式引入一不同的定义只使用pX−→qα形式的规则。然而，尽管如此，用标准的方法，可将f_p−→a_qα的规则转化为该f_qα.设N0def={0，1，2，3，.. . }。 在下面的内容中，我们将使用符号A表示序列i∈NA∈ Γ的出现，即，A0defA和Ai+1defAiA。 通过#A（γ）我们表示A∈ Γ在序列γ∈ Γ中出现的次数。3弱双相似的高不可判定性在这一节中，我们证明了PPDA和PDA的弱双相似性检查是101-困难的。证明是通过还原的nondetermistic Minsky机的递归问题。我们首先描述了一个一般的想法减少，然后显示它如何适用于PPDA和PDA。3.1总体思路一个具有两个非负计数器c1和c2的非确定性Minsky机R是一个有限的指令序列R =（I1，I2，.，In），使得n≥1，并且每个指令Ii，1≤i≤n，是以下三种类型之一3我们写pα而不是（p，α）∈ Q×Γε，其中p是控制状态，α是堆栈内容。状态p <$∈Q×Γ<$，其中<$代表空栈，写为p。0J. Srba / Electronic Notes in Theoretical Computer Science 98（2004）5-9111C1C2C1C C C CC 1 1 11C CC 2 22CC 22A a a aA221122增量i：cr：=cr+1;转到j测试并递减i：如果cr= 0，则转到j，否则cr：=cr−1;转到k不确定性 分支i： goto（j或k）其中1≤r≤ 2且1≤j，k≤n。备注3.1W.l.o.g. 我们可以假设I1是“增量”类型R的一个构形是一个三元组（i，v1，v2）∈ {1，.，n}×N0×N0其中i是要执行的指令的标签，v1和v2分别是计数器c1和c2的值。配置之间的计算步骤<$→以自然的方式定义。下面的递归问题Prec是n =1-完全的[3]：被执行了无数次吗“我们减少问题Prec弱双相似性检查PPDA和PDA。给定Prec的一个实例P，我们构造了一个PPDA（PDA）系统，以及一对进程p1和PJ所以问题P的答案是是的，当且仅当p1≠pJ。直觉是，一个配置（i，v1，v2）对应于一对亲，当eγ，γJ∈{C1，C2，A}满足chtat#C（γ）=#C（γJ）=i1 1v1，#C（γ）= #C（γJ）=v2，且#A（γ）= #A（γJ）是上界在指令I1被执行之前的步数。为了检查对于γ和γJ是否包含相同数目的C1、C2和A，我们将引入下列规则。等于−c→1等于−c→2等于等于−→a相当于平等C1−→C平等平等C2−τ→等于A−→τ等于C1平等C1−τ→等于C2−→C平等平等A−→τ等于C2等于C1−τ→等于C2−τ→等于A−→c相当于Lemma3. 2Letγ，γJ∈{C1，C2，A}<$. It使t等于γ当且仅当#C（γ）= #C（γJ），#C（γ）= #C（γJ），且#A（γ）= #A（γJ）时，γ j等于γj。是不管规则是解释为PPDA还是PDA。证据在第一轮中，攻击者通过执行动作c1、c2或a来选择要测试的符号。在连续的回合中，在操作c下，所选符号的每个出现都变得可见。τ规则简单地删除剩余的符号（这些规则仅在PDA的情况下需要Q10J. Srba / Electronic Notes in Theoretical Computer Science 98（2004）5-我我我J1我们的目标是设计一组重写规则，使得攻击者和防御者都有可能迫使对手忠实地模拟R的计算。机器R的单个计算步骤（i，v1，v2）<$→（iJ，vJ，vJ）是sim。1 2由互模拟游戏中的有限轮数决定，piγ和P JγJ满足chtatγ，γJ∈{C1，C2，A}，其中# C（γ） =#C（γJ） =v1，iJ J1 1#C2（γ）= #C2（γ）=v2和#A（γ）= #A（γ）。 这种模拟包括两个阶段：计数阶段和执行阶段。在计数阶段，参与者从p-控制状态piγ和pJγJ移动到q-控制状态qiδ和qJδJ，使得符号A的出现次数改变，而C1和C2的出现次数保持不变。这相位取决于i是否= 1（在这种情况下，防御者可以将任意数量的符号A添加到γ和γJ上），或者 i>1（在这种情况下，从γ和γJ中删除一次A）。在从q-控制状态qiδ和qJδJ开始的执行阶段中，玩家执行相应的指令Ii，并相应地修改C1和C2的出现次数（因此达到新的一对p-控制J J J J J J J状态PIJω和PIJω使得#C1（ω）=#C1（ω）=v1，#C2（ω）=#C2（ω）=v2以及#A（ω）= #A（ωJ）= #A（δ）= #A（δJ））。在非确定性分支的情况下，游戏的继续由防守者决定（使用DC）。这结束了R的一个计算步骤的模拟，博弈从piJω和piJω在此步骤中执行）。（指令IiJ将是由于参与者可以强迫彼此遵循上述两个阶段，我们可以如下论证我们的简化的正确性• 如果存在R的无限次计算，其中I1被无限次执行，那么让我们修正这样的计算。防御者现在可以迫使攻击者在互模拟博弈中从p1模拟这个计算，J （最初两个计数器都是空的）。 此外，辩护人是 能够每当指令I1被执行时，添加足够数量的符号A，因此总是可以在不同于I1的指令的计数阶段中删除A的一次出现。互模拟博弈变得无限，因此防守方获胜。• 如果R不存在I1无限频繁出现的无限计算，那么攻击者可以迫使防御者模拟一个特定的计算（由防御者选择），并且在无限多轮之后，指令I1无法从该点执行（与非确定性分支的选择无关）。现在攻击者继续模拟R的计算。每一步计算都会减少JpJ. Srba / Electronic Notes in Theoretical Computer Science 98（2004）5-1111不1Q111一11JJ符号A的出现次数。因此，在无限多轮之后，攻击者获胜（A的所有出现都被删除，这可以被检查）。3.2PPDA弱双相似性的X1-完备性我们现在将向读者提供上述结构的必要细节PPDA重写规则以这样的方式构造，使得它们能够稍后快速适应PDA规则我们从计数阶段开始（即， 从p-控制状态转移到q-控制状态）。准备执行I1的规则如下。p1−→ar1pJ −→aJp1−→aTJtJ−→τtJAtJ −→τrJ1 1 1 1 1r1−→as1rJ−→aJs1−τ→s1As1A−τ→s1s1−τ→q1rJ−→aS1q1c−h→eck等于qJc−h→eck等于考虑一个从p1γ和PJγJ开始的互模拟对策，其中γ，γJ∈{C1，C2，A}表示C1，C2和A在γ和γJ中的同时数是平等的。在第一轮中，攻击者被迫采取p1γ−→r1γ（DC）策略，defenderrcananswerbypJγJ=aJlJj，对于somel，J∈N和h，e和d，n1r 1A γ0任意数量的符号A。如果防守方处于形式tJAlJγJ通过使用tJ−→τrJ的规则来实现对s的约束，并且1 1 1由于从r1γ开始没有τ-移动，两个参与者都可以迫使另一个参与者到达一对状态rγ和JlJ，并且是防御者选择lJ∈N。1r1A γ0在下一轮中，攻击者被迫选择JLJJ−→ajlJJ（DCr1A γτq1A γ– here the ruler1γ=α 对于somel∈N0，q 1 A l γ（如果symbolsAfromγ可以被删除，但在这种情况下，攻击者赢了，正如后面在这篇文章中所讨论的那样。段）。 如前所述，如果防御者保持在攻击者使用的s1规则s-τ→q 由于没有τ规则jlJ Jthe11q1A γ博弈从一对q-控制状态qAlγ和jlJ. 如果l/=lJ1q1A γ那么攻击者就有可能执行动作检查，他就赢了因为引理3.2。这意味着，在无限多轮之后，玩家可以强制操作-12J. Srba / Electronic Notes in Theoretical Computer Science 98（2004）5-1我我我AA我J我我我我我我我到达一对状态q1Alγ和qJAlγJ的分量，并且允许防御者选择A的出现次数。以下规则将A的出现次数减一，并准备执行指令I2，.，In. 在以下规则中，i的范围超过{2，...，n}，并且让停止是不可能从其转换的特定控制状态。pAc−ou→ntqpJAc−ou→ntqJ我我我pc−h→eckstoppJAc−h→eckstop考虑一个从piγ和PJγJ开始的互模拟博弈，其中γ，γJ∈{C1，C2，A}n且1i≤n，证明了C1，C2，A的同时数的个数A在γ和γJ中是相等的。如果#A（γ）= #A（γJ）>1，则在一轮之后，参与者执行该动作计数并达到对q δ和qJδJ，使得Aδ=γ和AδJ=γJ。我我如果攻击者选择动作检查，防御者立即获胜。另一方面，如果#（γ）=#（γJ）=0，那么攻击者通过使用规则pc−h→eckstopto获胜，而防御者r没有获胜。执行阶段（即：从q控制状态转移到p-控制状态）。对于每个i，1≤i≤n，使得I是i：cr：=cr+1;转到j我们有以下规定。q −in→c pjCrqJ−in→c pJCr在从qiδ和qJδJ开始的一轮博弈中，参与人只有JiJ一种方式继续并到达pjCrδ和pjCrδ对。因此，他们忠实地模拟机器R的相应计算步骤。对于每个i，1≤i≤n，使得I是i：goto（j或k）我们有以下规定。q−→aq−→aq−→a选择我左我权我qJ−a→qJ−a→左我权我q选择左左左J左右i−→pjqi−→pjqi−→pkq选择权对对J权左i−→pkqi−→pkqi−→pjQQQQQJ. Srba / Electronic Notes in Theoretical Computer Science 98（2004）5-13我我我我我我我我考虑一个从qiδ和qJδJ开始的互模拟博弈，其中δ，δJ∈{C1，C2，A}我使得C1，C2和A在δ和δJ中是平等的。我们声称经过两轮博弈，参与者可以迫使对手要么达到pjδ和PJδJ要么达到pkδ和PJδJ，它就是防守者JK在这两种选择在第一轮中，attacker被迫使ayqδ−→aq选择δ（DC）和JJA左J我我JJA右J防御者回答：（i）qiδ −→qiδ 或（ii）qiδ−→qiδ。在第二轮从（i）q选择δ和q左δJ或（ii）q选择δ和q右δJ开始，我我我攻击者被迫（DC）在情况（i）中向左打动作，或在情况（ii）中向右打动作。情况（ii）。这意味着在两轮之后参与者达到对（i）pjδ和PJδJ或（ii）pkδ和PJδJJK“测试和递减”指令的规则与非确定性分支的规则类似。首先，防守方可以选择确定相关的计数器是否为空，然后根据这个决定继续比赛。在防御者移动之后因此，对于每一个i，1≤i≤n，使得Ii的类型为i：ifcr= 0then gotojelsecr：=cr−1;gotok我们有以下规定。q−a→qchoiceq−a→qleftq−a→qrightqJ−→aqJ−→a左我权我q选择左左左J左右i−→zeroiqi−→zeroiqi−→非零iq选择权对对J右左i−→nonzeroiqi−→nonzeroiqi−→零iQQ14J. Srba / Electronic Notes in Theoretical Computer Science 98（2004）5-我我ppRRR我RRRR我KRJKR零我 −ze→ropzeroJ−ze→roJ非零iC−d→ec p非零JCr−d→ecJ零c−h→eckzzeroJc−h→eckzJ我ZrCr−→bRi停止zJCr −→cR停止z C−τ→zA−τ→zzJC−→τzJzJA−→τzJr3−r r r rR 3 −rrrr非零c−h→ecknnonzeroJc−h→ecknJ伊里伊里n−→b停止nrCr −→c停止nJCr −→b停止nJ −→c停止考虑一个从qiδ和qJδJ开始的互模拟博弈，其中δ，δJ∈{C1，C2，A}表示C1，C2和A在δ和δJ中的共现数是平等的。与前面相同的论点适用于表明，在两轮游戏之后，玩家可以迫使对手达到（i）零iδ和零JδJ或（ii）非零iδ和非零JδJ根据防御者我我攻击者现在可以通过播放动作检查来验证防御者决定的正确性从（i）zr和ZJ或（ii）nr和NJ开始。以下两个引理证明在这种情况下，攻击者获胜，当且仅当防御者作弊。Lemma3. 3Letδ，δJ∈{C1，C2，A}ε，r∈{1，2}. Itholdsthatzrδ$>zJδJ当且仅当0 =#C（δ）=#C（δJ）. 不管规则是否R r解释为PPDA或PDA。证据 明显QLemma3. 4Letδ，δJ∈{C1，C2，A}ε，r∈{1，2}. 在PPDA情形下，nrδ<$NJδJ当且仅当1 ≤ #C（δ），#C（δJ）. 它也包含（在Rr r在PDA的情况下），nrδ <$nJδJ当且仅当δ和δJ都以Cr开始。证据 明显Q为了完成“测试和递减”指令的模拟(ii)非零iδ和非零JδJ。 在情况（i）中，它们执行动作零，并且iJJ达到一对新的状态pjδ和pjδ。（二）执行行为dec并将C r的出现次数减少1。在此之后，它们从对pkω和PJωJ继续，使得Crω=δ和CrωJ=δJ。JKJ. Srba / Electronic Notes in Theoretical Computer Science 98（2004）5-151111为了得出结论，我们还记得，在不确定分支的情况下，双方参与者都可以迫使对手忠实地模拟机器R的计算步骤，而防守者则可以选择。此外，每当执行指令I1时，防御者可以生成足够的符号A，以确保在再次执行指令I1之前他不会输。如果机器R的计算无限次访问I1，那么防御者在互模拟博弈中模拟这样的计算，并且他赢了（因为攻击者决定在模拟过程中不合作另一方面，如果沿着每条计算路径，指令I1只执行有限次，那么攻击者获胜，因为防御者生成的符号A最终将被耗尽。因此，对于给定的不确定明斯基机的递归问题的答案是肯定的，当且仅当p1<$pJ。定理3.5 PPDA（和PN）的弱双相似性检验是π 1-完全的。证据问题的难度来自上述结构，并且在[ 5 ]中建立了PN（和PPDA）的问题在[1]中的遏制。Q3.3PDA弱双相似性的X1-完备性我们现在将继续展示如何为该案例调整PPDA规则的PDA。显然，上面定义的所有不从堆栈中删除任何符号的PPDA规则也可以用于PDA。但是，有三种情况会将符号从堆栈中删除第一，有一个规则在指令I1的计数阶段，s1A−τ→s1。因为它是足够的，该规则仅移除在前一轮中添加的A的出现（并且因此在堆栈的顶部），在这种情况下不需要改变符号被移除的第二个位置是在指令I2，.的计数阶段。，In和第三位是在对应计数器的非零值的情况下的“测试和递减”指令的规则（回想一下，I 1是注释3.1的“递增”类型）。幸运的是，所列出的问题可以通过结构中的一个修改来解决。这个想法是，在每个计数阶段之前，防守者被允许重新排列堆栈的内容（同时保留C1，C2和A的出现次数），以使堆栈相等（为了应用DC）并且符号A在它们的顶部。如果执行阶段继续执行16J. Srba / Electronic Notes in Theoretical Computer Science 98（2004）5-pA−→我我不我R我我u我我我我我我我1222221122我我我我我我我我我我我在A之后。这是正式描述如下。对于所有i，1

下载后可阅读完整内容，剩余1页未读，立即下载