《理论计算机科学电子札记》52卷第1期（2001年）网址：http://www.elsevier.nl/locate/entcs/volume52.html20页Rewrite Systems withConstraints（约束重写系统）马萨里克大学信息学院博塔尼克68a，60200布尔诺，捷克共和国摘要我们扩展了一个广泛使用的重写系统的概念，一个单元持有一种全局信息，可以在UENCE，可以在UENCE重写。 该单元类似于并发约束编程中使用的存储，也可以被视为一个特殊的（弱）状态单元。 我们介绍了这个扩展如何改变Mayr的PRS层次结构中包含的重写系统类的表达能力[8]。新类（fcBPA、fcBPP、fcPA、fcPAD、fcPAN、fcPRS）将被描述并插入到层次结构中。1引言并发理论的基石是标记转换系统的概念。Caucal [4]使用与Chomsky层次结构相关的顺序重写系统族提出了一种优雅的转换系统分类。Caucal的分类已经被Moller [11]推广到并行和顺序重写系统。Moller的方法被Mayr [8]进一步推广，他定义了使用顺序和并行组合的重写系统的动力学。由此产生的模型被称为过程重写系统（PRS）。并发约束编程（CCP）[14]是并发和部分信息计算思想的最有效应用之一。在CCP中，进程与共享存储并行工作，这被视为对变量可以表示的值的约束。在计算的任何状态下，悬挂物都是由直到该时刻所建立的约束给出的。CCP提供了两个操作来处理存储，告诉和问。 tell通过添加一个约束来单调地更新存储（假设存储保持一致）。ask是对存储的测试，只有当当前存储足够强以需要指定的约束时才能执行它。如果这1 这项工作得到了捷克共和国赠款机构的部分支持，赠款号为：201/00/0400。2 电子邮件地址：xstrejc@fi.muni.czc2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。斯特雷日切克2一一如果不是这种情况，则进程挂起（等待存储器通过其他进程的贡献积累更多信息）。我们将CCP的一些原则移植到进程重写系统中。以前，我们在[15]中介绍了纯顺序和纯并行重写系统的类似修改。在这两种情况下，其目的是为了了解这些系统的表达能力的变化。 PRS的机制是扩展与存储，其中可以包含一些全球（单调发展）的信息。我们为每个重写规则添加两个约束。只有当实际存储足够强以需要rst约束时，才可以应用规则;当使用扩展规则时，第二个约束被添加到存储中（如果存储保持一致，则该规则适用）。扩展的过程重写系统被称为具有nite约束系统的过程重写系统3通过研究哪些标号转移系统（直到互模拟）可以用PRS系统的特定类表示，得到了一些有趣的结果（与众所周知的形式主义如Nite状态系统 、 基 本 进 程 代 数 （ BPA ） 、 基 本 并 行 进 程 （ BPP ） 、 进 程 代 数（PA）、下推进程、Petri网等一致）.以及相应的fcPRS类。通过增加存储，nite状态系统、下推过程和Petri网的表达能力保持不变。这在本案中不成立当表达能力严格增加时，BPA、BPP、PA、PAD和PAN类的变化，从而得到一些新的类。因此，这个新的框架可以用来解决一些有趣的开放问题，例如，检查已经维护的过程层次结构中的可判定性边界（在双相似性的情况下，已知边界线在BPP和它的"状态扩展”版本MSA之间，在（赋范）PA和它的“状态扩展”版本MSA之间继续，等等）;我们的新工艺类别处于这一灰色地带。2基本定义在这一节中，我们回顾了标记转换系统的概念，由这样的系统生成的语言，以及互模拟等价。定义2.1标记转换系统（LTS）L是元组（S; Act;！; 0），其中S是一组状态或进程，Act是一组原子动作或标签，！SAct S是一个转换关系（书面！而不是（;a;）2！），02S是一个可区分的初始状态。 状态2S是终端（或d e a dl ock e d，写作6！）如果没有一个2法案和2S苏克H！.过渡关系！可以同态扩展为nite3注意，fcPRS系统的规则也可以被视为SOS规则的新的特殊“格式”（在[6]的意义上），其附带条件涉及全局（单调）存储。然而，这一观点在本文中没有审查。斯特雷日切克3一0一行动顺序2行动，以写！“和！每当！！对于某个国家来 说 。一 组状态，使得0！对于初始状态0和某个2 Act，称为可达状态集。定义2.2由标号转移系统L生成的语言是集合L（L）=L（），其中L（）=fw2Actj 9：w！ 六！G. 国和系统L的语言等价，它们生成相同的语言，即L（）= L（）。在并发理论的框架中，语言等价通常被认为过于粗糙第二个等价，互模拟等价，也许是巢行为等价研究。互模拟等价由Park [13]定义，并由Milner [9，10]在CCS工作中使用定义2.3关于标号转移系统的状态的二元关系R是互模拟i，只要（;）2 R有，如果0然后！一0对于一些0与（0的整数;0）2R，如果a！0然后0对于一些0与（0的整数;0）2 R.和是互模拟等价或互相似的，我 （;）2 R对于某个互模拟R.3过程重写系统（PRS）本节总结了Mayr的论文“Process Rewrite Systems”[8]的第一部分。Mayr提出的过程重写系统（PRS）是重写形式主义的一个非常一般的术语，它为可能的Nite变迁系统提供了一种Nite描述方法。该形式化体系涵盖了许多广为人知的模型，如nite-state进程（FS）、基本并行进程（BPP）、上下文无关进程（BPA）、下推进程（PDA）、进程代数（PA）、Petri网（PN），并提供了这些模型的统一视图。PRS的定义比Caucal [4]（仅顺序组合）和Moller [11]（仅纯顺序和纯并行重写系统）给出的重写系统的定义更一般设Const = fX; Y; Z; g为可数无穷过程常数集.过程项的集合T由抽象语法t =“j X j t1：t2 j t1 kt2;其中“是空项，X2 Const是过程常数（用作原子过程），”k“表示并行，“分别表示顺序组合。我们总是处理平行复合的模交换性和结合性以及顺序复合的模结合性我们还定义ne“：t = t = t：“和tk”= t。斯特雷日切克411111一一一一1集合Const（t）是在过程项t中出现的所有常数的集合。我们区分了四类过程术语。\1”由单个过程常数（如X）组成的术语。\S”连续项-没有并行组合。例如X：Y：Z。\P”并行项-没有顺序组合。例如，XkY kZ。\G”具有任意嵌套的顺序和并行组成的通用术语，如（X：（Y kZ））kW。我们也让“2 S; P; G，但“62 1。定义3.1设Act = fa;b;g是原子作用的可数无穷集，2f1;S;P;G g满足。（;）-PRS（预写系统）是一对（R; t0），其中R是一组形式为t的重写规则！一t2，其中t12，t16 =“，t2 2 是过程术语，第二幕是原子动作，t0 2这是一个初始状态。A（G; G）-PRS简称为PRS。a a我们写（t 1！t 2）2而不是（t 1！t2）2R，其中 =（R; t0）。对于给定的，我们定义Const（）为重写规则或初始状态中出现的所有常量的集合，而Act（）为重写规则中出现的所有动作的集合。Const（）和Act（）都是nite集合。每个进程重写系统表示一个表示其动态的标记转换系统（LTS）。设 = （ R;t0 ） 为 （ ; ） -PRS 。 由 y 表 示 的 LTSL 是 元 组 （ S;Act（）;！;t0），其中S=ft2jCost（t）Const（）g是状态集，t0是初始状态和转移关系！是满足推理规则4的最小关系（t 1 ！t2）2;ta！的t0;t！的t0;不 ！ 不一tkt！t0ktt：t！t0：t其中t1，t2，t01 22吨。1 21 21 21 2我们所说的“进程重写系统”是指由进程重写系统产生的带标号迁移系统。显然，可以假设（w.l.o.g.）（;）-PRS的初始状态t0是一个单一的常数，因为只有nitely许多项，使得测试0 一个！我蒂岛图1示出了（;）-PRS的层级的图形描述，简单地称为PRS层级。层次结构中包含的一些类对应于广泛已知的模型：（1; 1）-PRS等价于nite-state系统（FS）。每个过程常数对应于一个状斯特雷日切克5态，状态空间由jConst（）j限定。每个nite-state系统可以编码为（1;1）-PRS。4注意，并行组合是可交换的，因此，并行组合的推理规则在t1和t2交换的情况下也成立。斯特雷日切克6（G; G）-PRSPRS垫、、、、、 潘（S; G）-PRS、、、、、PDAPA（P; G）-PRSPN（S; S）-PRS（1; G）-PRS（P; P）-PRSBPA、、、、、 BPP（1;S）-PRS、、、、、FS（1;P）-PRS（1; 1）-PRSFig. 1. PRS层级（1; S）-PRS等价于[1]中定义的基本过程代数过程（BPA），BPA是与Greibach范式（GNF）上下文无关文法相关联的转换系统，其中只允许最左边的导子。（1;P）-PRS等价于无通信网，它是Petri网的子类，其中每个变迁在其预设中只有一个位置[3]。这类Petri网等价于基本并行过程（BPP）[5]。（1; G）-PRS等价于PA-进程，具有顺序和并行组合的进程代数，但没有通信（详见[1]）。很容易看出下推自动机可以被编码为子类（S; S）-PRS（规则左侧最多有两个常数）。Caucal [4]证明了任何无限制的（S; S）-PRS都可以表示为下推自动机（PDA），在这个意义上，转移系统直到状态的标记都是同构的。 因此（S; S）-PRS等价于下推过程（由下推自动机描述的过程）。（P; P）-PRS等价于Petri网（PN）。每个常数对应于网络中的一个位置，一个常数在一个项中出现的次数对应于这个位置上的令牌数量。这是因为我们的工作与类的条款模交换并行组成。中的每一条规则都对应着网络中的一个变迁。（S; G）-PRS是下推过程和PA-过程的最小通用推广。他们被称为PAD（PA+ PDA）[8]。（P; G）-PRS在文献[7]中被称为PAN-过程。它是Petri网和PA-过程的最小通用概括，并且严格地包含了它们（例如，PAN可以描述所有的Chomsky-2语言，而Petri网不能）。斯特雷日切克7最一般的情况是（G; G）-PRS（这里简称为PRS）。在[8]中引入了PRS。它们包含了前面提到的所有类。等级制度并不严格。语言对等例如，BPA和PDA都定义了（“-free）上下文无关语言。等级制度的严格性。互模拟等价性从前面的结果[2，11]和证明中得出，存在不与任何PAN系统互相似的PDA系统（在示例3.2中描述）和不与任何PAD过程互相似的Petri网（在示例3.3中描述）例3.2让我们考虑下面的PDA系统，初始状态为U：X。a a aU：X！U：A：XU：A！U：A：AU：B！U：A：BbB bU：X！U：B：XU：A！U：B：AU：B！U：B：BcC cU：X！V：X U：A！V：AU：B ！五：BdD dU：X！W：XU：A！W：AU：B ！W：Bea BV：X！ VV：A！ VV：B！Vfa BW：X！ WW：A！ WW：B ！W例3.3考虑如下的Petri网：（P; P）-PRS，初始状态为XkAkB。g一X！ XkAkBY KA！ YC bX！ YY kB！ YD dXKA！ ZY KA！ ZD dXKB！ ZY kB！ Z4带节点约束系统的PRS（fcPRS）在本节中，我们扩展了PRS形式主义与单位（称为存储）的能力以保持一种全局信息，该全局信息可被该术语的所有并行线程访问。 这是相当令人惊讶的是，这个单位（这是不一样强大，一个通用的nite-state控制单元，它甚至给PA类赋予图灵能力）增加了像PAN和PAD这样的类的表达能力。本文用一个约束系统，即一组具有代数格结构的约束来描述具有有限约束系统的PRS所使用的悬挂物的状态空间和可能的演化。定义4.1一个约束系统是一个有界格（C;`;^;tt;ff），其中C是约束集，`（称为蕴涵）是这个集上的一个序，^是lub操作，tt（true），ff（false）是最小和最大的斯特雷日切克8、一一一C的元素表示存储的状态，C的元素（ff` tt和tt 6= ff）。在代数中，符号^通常表示glb运算，而lub运算则用符号_表示。 我们的lub操作符号对应于逻辑合取（如CCP中）。我们说约束m与约束ni m^ n 6= ff是一致的存储的状态不能是ff，因为我们需要初始化为tt的存储的一致性我们用C表示Cr fffg。例4.2设C“是平凡约束系统（ftt;ffg;`;^;tt;ff），其中`=f（ff;tt）;（tt;tt）;（ff;ff）g，且Cmn为约束系统Cmn=（ftt;m;n;ff g;`;^;tt;ff），其中`=f（f f;tt t）;（m;tt）;（n; tt t）;（f f;m）;（f f;n）g[f（o;o）j o2C g. 这些约束系统描述如下。ffff，，m，，TT，、、、nTT定义4.3设;2f1;S;P;G g满足. （;）-fcPRS（具有nite约束系统的PRS）是元组（C; R; t0），其中C=（C;`;^;tt;ff）是一个描述空间的有限约束系统，R是一组重写规则，其形式为（t 1！ t 2; m; n），其中t 1 2，t1 6=“，t2 2是过程项，a 2 Act是原子动作，m; n 2 C是约束，t0 2是一个特殊的初始过程项。A（G;G）-fcPRS简称为fcPRS。我们使用人类可读的缩写fcFS 、fcBPA 、fcBPP 、fcPA 、fcPDA 、fcPN、fcPAD、fcPAN和fcPRS来表示类（1; 1）-fcPRS、（1; S）-fcPRS、（1;P）- fcPRS、（1; G）-fcPRS、（S; S）-fcPRS、（P; P）-fcPRS、（S; G）-fcPRS、（P; G）-fcPRS、和（G; G）-fcPRS。同样，代替（t1一！t 2; m; n）2 R，其中=（C; R; t0），我们通常write（t 1！ t 2; m; n）2.sets Const（）的含义（过程常量在重写规则中使用）和Act（）（在重写规则中发生的动作）与PRS情况相同。同样，可以假设（;）-fcPRS的初始项t0是单个常数。每个带结点约束系统的PRS表示一个标号变迁系统.设=（C;R; t0）是（;）-fcPRS。由表示的LTS L具有形式（S;Act（）;！;（t0;tt）），其中S=ft2jConstt（t）Constt（）gC是状态集，（t0;tt）是初始状态和转移关系！ 是-ned作为满足推理规则的最小关系（t1 ！ t 2; m;n）2斯特雷日切克9一（t 1; o）！（t 2;o^n）如果o` m和o^ n 6= ff;斯特雷日切克1011111一一一和（;）-fcPRS=（C“;R;t0）是同构的，假设R0=（t ; o）（t kt; o）（t0;p）;（t0kt;p）（t; o）！（t：t;o）！（t0;p）;（t0：t;p）1 21 2 1 21 2其中t1;t2;t02T和m;n;o;p2C。第一个推理规则中的两个边条件与CCP中使用的原则非常接近第一个（o`m）确保规则（t 1！t 2; m; n）2仅当存储的当前状态o需要m时才能使用（它类似于CCP中的ask（m））。 第二个条件（o ^n6= ff）保证了存储在应用规则后保持一致（类似于在CCP中处理tell（n）时的一致性要求）。一个重要的观察是，悬挂物的状态（从tt开始）只能在格点C中从tt向上的一个方向上移动。 这可以很容易地从以下事实看出：存储o的实际状态只能通过应用某些重写规则（t1！ t 2; m; n）2，并且在此应用之后，存储的新状态o^n总是需要o。直观地说，部分信息只能添加到商店中，而不能收回。我们说商店是单调的。请注意，当系统（存储上有o）执行由规则（t1！t 2; m; n）2，则对于存储的每个后续状态p，满足条件p`m和p^n 6= ff。第一个条件p` m来自存储的单调行为。第二个条件来自这样的事实，即规则中的约束n仅在规则的第一次应用中可以改变存储，并且对于每个后续状态p，p^ n = p的值成立。另一方面，某个规则是适用的（因此蕴涵和一致性是令人满意的）这一事实并不意味着这个规则永远适用。潜在的问题是一致性要求。商店可以演变到与来自规则的第二约束不一致的状态关于fcPRS和PRS之间的关系的第一信息由以下引理提供。引理4.4Let;2f1;P;S;G g. 系统（;）-PRS0=（R0;t0）a a英尺1！ t 2j（t 1！ t2; tt; tt）2 Rg.证据 很容易检验，如果我们从由fcPRS生成的LTS的状态中去除tt，我们得到对应于PRS0 的同构系统。2上面的引理说PRS类可以被看作是具有平凡约束系统的fcPRS类。该引理可以在两个方向上使用，以表明指定形式的任何fcPRS具有等价的PRS以及用于构造与给定PRS等价的fcPRS。一一斯特雷日切克11、、..、、、、、一fcPRS. . . .、、. . . .PRS、、. . . .. ..、、、、、fcPAD. . .. .，fcPAN，。，。，。、、、.PAD，，、、、、、、潘、、、、、FCPA，。，。、 、.fcPDA=PDA。. .PA、，f，cPN=PN. . . .. .. .......fcBPA. .. .，fcBPP. . . .BPA，、、、、、、、、、BPP. . . . .. . . .fcFS=FS图二. fcPRS层次结构5fcPRS层次结构图2显示了PRS和fcPRS类的层次结构，简称为fcPRS- hierarchy。在层次结构中描述的关系部分来自类的定义和引理4.4。本文的其余部分致力于三个等式（fcFS = FS，fcPDA = PDA和fcPN = PN）和层次结构的严格性。定理 5.1（i）设为fcFS。存在FS0，表示一个与下式同构的标号转移系统.(ii) 做个fcPDA。存在PDA0，表示一个与下式同构的标号转移系统。(iii) 让做一个fcPN。存在PN0，表示一个与下式同构的标号转移系统。证据(i)构造是显而易见的，的每个状态（X; m）被转换为0的状态X（m）。(ii) 证明的思想是基于这样一个事实，即我们可以添加与存储的实际状态对应的特殊过程常数，fcPDA的每个状态一个。然后存储的内容将由这样的特殊常量表示。令=（C;R;t0），其中C=（C;t;t;f f）。 设S=fS（m）jm2Cg为特殊过程常数集. 一个PDA0被构造为（R0;S（tt）：t0），其中S（t t）：t0是初始项，特殊常数保持初始商店的状态。 我们替换所有的规则（t1 ！ t 2; m; n）2R根据一套规则（S（o）：t1）S（o^n）：t2）2R0斯特雷日切克12对于满足蕴涵条件o` m和相容性条件o^ n6 = ff的任意o 2 C.新规则的构造遵循与原规则相关的蕴涵和一致性条件和0的同构是明显的，因为每个状态S（m）：t的0正好对应于系统的状态（t; m）。(iii) 证明是相同的（ii），如果我们取代每一个顺序组成的并行组成。2由于PRS层次结构不严格，语言等价，fcPRS层次结构也不能严格的语言表达水平。然而，fcPRS层级是严格的w.r.t.互模拟等价，可能有一个例外：PRS和fcPRS之间的关系（这种情况将在后面讨论）。为了证明类fcBPA、fcBPP、fcPA、fcPAD和fcPAN中的每一个与对应的标准类不同，我们提出了两个fcPRS系统。第一个是fcBPA系统，它不是任何PAN系统的双相似。第二个系统将是fcBPP，它与任何PAD系统都不是双相似的。例5.2让我们考虑一个fcBPA系统，它具有例4.2中的约束系统Cmn和初始过程项U：X。a a（美国） ！U：A; tt; tt）（A ！“; tt;tt）bB（美国） ！U：B; tt; tt） （B！“; tt;tt）ce（U！“; tt; m）（X！“; m; tt）dF（U！“; tt; n）（X！“; n; tt）上述fcBPA与3.2中描述的PDA系统是双相似的，PDA系统与任何PAN系统都不是双相似的，因此所考虑的fcBPA过程也与任何PAN系统都不是双相似的。因此我们得到一个推论，其中X（ Y）表示X是Y的严格子类，而X6Y表示X不是Y的子类.推论5.3 BPA（ fcBPA，PA（ fcPA，PAN（ fcPAN和fcBPA6 PA，fcBPA 6 PAN，fcPA 6 PAN。证据直接从BPA和PAN类的定义，并由此得出BPA类是PAN类的子类引理4.4暗示BPA类是fcBPA类的子类我们知道，存在一个fcBPA系统，它与任何PAN系统都不双相似，因此也与任何BPA系统都不双相似。因此，我们知道BPA是fcBPA的严格子类。其他关系的证明也是类似的。2例5.4让我们考虑一个具有约束系统的斯特雷日切克13一BeCXXX（分别） 在1和以下平行组合物的一部分之间）。 因此下面描述的和初始状态（X; tt）。ff（X！XkA; tt; tt）（X！XkB; tt; tt）O（X！“; tt; o）tt（A！“;o;tt）d（B！“; o; tt）引理5.5如果有一个PAD系统与例5.4中的fcBPP系统双相似，那么也有一个PDA系统与这个fcBPP双相似证据设是具有初始状态Q（w.l.o.g.）使得Q与所考虑的fcBPP系统的初始状态（X; tt）双相似。由于重写规则的左侧只能发生顺序组合，因此只有当存在形式为（t1 kt2）：t3的可达状态时，并行组合t1kt2的某个部分才能影响这样的系统的行为，其中t3可以是“。如果不存在这样的状态，我们可以从规则中删除所有的并行组合，我们得到一个PDA系统，因此也与所考虑的fcBPP过程双相似。另一种情况出现，如果存在形式为（t1 kt2）：t3的可达状态，其中t3可以是“。让我们假设，在推导state（t1kt2）：t3从Q中没有其他形式的状态（t0kt0）：t0（t3可以是1 2 3“）. 由于Q是单一过程常数，且任何平行组合物在项p：（s1ks2）：p0不能通过重写来改变，直到p是“，必须有一些重写规则（t！L：（T1 KT 2）：R）2（L; R可以是“，x2fa; b; c; d; eg），使得T1 KT 2是所提到的平行组合物。有两种情况。(i) 状态（t1 kt 2）：t3是在一个字w2 fa; bg下从Q导出的.我们证明了t1或t2是死锁的。关于PAD的定义，它不提供并行组合中进程之间的任何形式的通信或同步，只有t1 kt2的一个组件可以启用动作e，让我们假设它是t2。然后t1被死锁{它既不能执行动作a或b（因为这些动作在动作e之后被禁用），也不能执行动作c或d（因为这些动作在动作e之前被禁用）。然而，t1 ： t0项 对于某项t0不 一 定 是 死 锁 的 . 因此，规则（t！l：（t 1 kt 2）：r）2可以改变为顺序组合t 2：t 1。我们应该在t2和t1之间插入一些分隔符（分别为l和t2）保持并行组成部分之间的不可能通信X x我们替换规则（t！l：（t 1 kt 2）：r）2由规则t！l：X：t2：X：t 1：r（分别） 不 ！t2：X：t1：r if l=“），其中X2=Const（）是一个新的const。stant，我们添加新的重写规则X：sx的！每一次重写，斯特雷日切克14规则s02（如果我们已经有了X形式的规则：ss0斯特雷日切克15XXX1 2 3 33在修改后，我们不需要在未来再次添加它们这些变化并不影响的行为。(ii) 动作e发生在从Q导出状态（t1kt2）：t3的过程中。状态（t1 kt2）：t3则与所考虑的fcBPP的状态（An kBm; o）5双相似，因此进程（t1 kt2）：t3执行的每个可能的动作序列是nite，以及项t1 kt2执行的每个可能的序列。我们构造了一个nite标记的（无环）转移图，其中顶点是从并行组合t1kt2（这是图的根）可到达的过程，边自然对应于动作（分别为）。重写规则）。现在我们给图的每个顶点分配一个新的过程常数，该图具有一些并行组成内部（没有任何平行组合的顶点 保持不变）。我们替换规则（t！l：（t 1 kt 2）：r）2根据规则T！l：Z：r，其中Z2=Const（）是分配给t1kt2的过程常数。对图中从顶点A（A是一个新的常数）到顶点v的每一条边，我们添加一个规则A！v（其中x是边的标号）if（tkt）：tt0：t则项t可以通过以下方式进行更改只有当t0中没有平行合成时，才发生转移，并且没有任何平行合成的顶点不变。在这两种情况下，重写规则中的并行组合的数量都减少了折痕（有一个例外{当我们添加X：s形式的规则s0，则平行合成的数量可以加倍，但这并不重要，因为我们只做一次）。如果modi ed中仍然存在形式为（t1 kt2）：t3的可达状态，我们可以再次使用相同的方法。由于重写规则中的并行组合数是nite，经过nite步，我们得到一个没有任何可达状态的PAD系统，其形式为（t1kt2）：t3，这就是本文开头讨论的情况2上下文无关语言（context-free languages）由PDA过程生成的语言类）在与常规语言的交集下是封闭的 由来自示例5.4的fcBPP系统生成的语言L不是上下文无关的，因为L\abecd=fanbmecndmj m;n0g不是上下文无关的。 因此，不存在PDA过程双相似于来自实例5.4的fcBPP，并且从引理5.5得出不存在PAD过程双相似于以上呈现的fcBPP。因此我们得到：推 论 5.6 BPP （ fcBPP ， PAD （ fcPAD 和 fcBPP 6 PA ， fcPA 6PAD，fcBPP 6 PAD。fcBPP类甚至不同于PN。语言对等由例5.7中的y PN生成的语言L=fanbcndenfj n0 g是一个5 表达式An 是并行组成的过程常数A的n个副本的缩写。缩写Bm 有类似的意思。到 . 的行为仍然没有改变，斯特雷日切克16BXzXz由PN生成的语言的实例，由于下面的Pumping引理，它不能被任何fcBPP描述。例5.7假设=（R; W）是具有如下重写规则的Petri网。a eW ！W kAkBY kB！ YW ！ XYCF！ZzX kA！ XZKA！ ZKAD zX！ YZkB ！ ZKB引理5.8（fcBPP的泵引理）设L是fcBPP系统的语言。存在一个常数h使得如果u 2 L且juj > h则存在x; y; z; w 2 Act使得u = xz，jyj > 1，且δi 0成立xyi zwi 2 L.6证据证据可以在附录A中找到。2为了证明严格的fcPRS-层次结构完全，我们引入了一个PDA过程，这是不是bisimilized任何fcPAN过程和PAN过程，这是不是bisimilized任何fcPAD过程。例5.9让我们考虑例3.2中描述的PDA系统，其初始状态为U：X：Y，并具有以下附加重写规则。V：YV：Y！U：X：YW：Y！ ZW：Y！U：X：Y！Z这个系统的行为与例3.2中定义的一样，但是当原始系统终止时，增强的系统可以选择在操作z下终止或在操作x下重新启动。引理5.10不存在与例5.9中给出的PDA过程双相似的fcPAN系统。证据我们假设相反的情况，并得出一个矛盾。 假设fcPAN双相似于实施例5.9中定义的PDA过程。从中使用的约束系统的有效性如下：存在一个非终结可达状态（t;o），使得从（t; o）可达的每个非终结状态约束系统）。由于（t; o）是非终结符，w2fa;b;c;d;e;fg suchthat（t;o）w！：x（s; o），其中（s; o）与来自实施例5.9的PDA方法的状态U：X：Y。如果从中移除由动作x; z标斯特雷日切克17记的规则，并将（s; o）作为初始状态，则我们得到其可达状态都以o作为其存储的系统，这与例3.2中6 表示字u的长度。斯特雷日切克18vv现在让0是具有初始状态s和重写由规则l！r，其中（l！r; m; n）2，o`m，o^n = o和v2fa; b; c; d; e;fg.很明显，该PAN系统0与实施例3.2中定义的PDA系统是双相似的。 这是一个矛盾。2推论5.11 fcBPA（ PDA，fcPA（ fcPAD和fcPAD 6 fcPAN。例5.12设一个PAN进程，初始状态为（XkAkB）：W，重写规则如下。gayxX！ XkAkBY KA！ YX！ “ W！（XkAkB）：WcbyzX！ YY kB！ YY！ “ 魏 ！D每日XKA！ ZY KA！ ZZ ！“的每日XKB！ ZY kB！个zla ！“的yB ！“的重写规则的前两列包括与例3.3给出的Petri网相同的规则。这个PAN系统可以表现为上述Petri网（它可以偏离PN的行为，只有在行动y）。与所考虑的PN的终端状态相对应的PAN的状态可以执行一系列动作y以到达状态W，然后在动作z下终止或在动作x下重新启动系统。引理5.13不存在与来自实例5.12的PAN过程双相似的fcPAD系统。证据这个证明类似于前面引理的证明，它使用了例3.3中的Petri网，而不是例3.2中的PDA2推论5.14 fcPA（ fcPAN和fcPAN 6 fcPAD。fcPAD和fcPAN的不可比性意味着这些类是fcPRS的严格子类。在fcPRS层次结构中PRS和fcPRS类之间的边缘是点的，因为我们没有证据证明fcPRS类严格来说更具有表达性（w.r.t.比PRS类更相似。从PRS fcPRS的定义中可以明显看出，但我们只能为PRS（ fcPRS）提供直观。不平等的证据可以在下面的fcPA中找到。例5.15令是具有初始过程项XkY的fcPA系统斯特雷日切克19X以及下面的约束系统和重写规则。a a0ff（X ！X：A; tt; tt）（A！“; o;tt）b b0o（X ！X：B; tt; tt）（B！“; o;tt）pc c0（Y ！YkC; tt; tt）（C ！“; o;tt）tt（X！“;tt; p）y（Y ！“; p; o）我们可以证明这个fcPA系统不是任何PAD过程和任何Petri网的双相似。现在，我们试图解释为什么我们推测没有PRS过程双相似所考虑的fcPA。PRS（或一般的重写系统）的弱点是重写的“局部势”。如果一个并行组合中至少有一个顺序组件大于任何重写规则的左侧，则该规则不能同时影响该大组件和并行组合的其余部分。粗略地说，大型组件和并行组合的其他组件之间的通信与所考虑的fcPA系统双相似的任何PRS过程都应该具有这样的并行组合，其中一个组件具有顺序字符（因为有必要保持关于动作a和b执行顺序的信息），并且它可以是任意大的。我们需要向项声明，行动y已经完成了.6结论我们已经丰富了进程重写系统的机制与计算部分信息的形式，广泛研究的并发约束编程。在过程重写系统中，这种机制可以有效地为过程项的每个部分提供某些信息，因此它可以被看作是一个保存特殊类型的全局信息的单元。它已被证明，丰富的类nite系统，下推过程，和Petri网与nite约束系统不会改变他们的表达，甚至w.r.t.所生成的标记转移系统的同构。相反，随着这些系统的表达能力的增加，利用nite约束系统扩展的过程重写系统类BPA 、BPP 、PA 、PAD 和PAN 建立相应的新类fcBPA 、fcBPP 、fcPA、fcPAD和fcPAN。在PAD和PAN类的情况下，这可能看起来相当令人惊讶，因为这些类的形式主义分别包含PDA或PN的形式主义。然而，PDA和PN并没有增加他们的表达能力，如果丰富了nite约束系统。已经引入了fcPRS类的层次结构，w.r.t.互模拟等价（除了斯特雷日切克20PRS和fcPRS类）已经过验证。过程重写系统领域，夜间约束系统仍然为进一步的研究提供了一些有趣的话题。一个有趣的挑战是指定fcBPP类区域中的nite-state过程的互模拟等价和弱互模拟等价的可判定性边界（因为这两个问题对于BPP是可判定的，而在MSA7的情况下是不可判定的）。进一步研究的另一个可能的主题是用（nite）状态单元代替约束系统，其中实际状态的演化由给定的排序决定。一个完全不同的任务是采用一个在夜间约束系统。一个ckno wl edegements：我想感谢M ojmrKretnsky宝贵的 讨论，阅读草案，并不断支持。我还要感谢Anton n Ku cera的鼓励和鼓舞人心的评论。我感谢三位匿名推荐人的有益评论。引用[1] Bergstra，J. A.，和J. W. Klop，代数与抽象通信过程，理论计算机科学37（1985），77{121。[2] Burkart，O.，D. Caucal和B.张文，“基于互模拟的过程分类方法”，计算机科学学报，第1119卷，1996年，第247{262}页。[3] Burkart，O.，和J. Esparza，More in nite results，Bulletin of the EuropeanAssociation for Theoretical Computer Science62（1997），138{159.[4] Caucal ， D. ， 关 于 前 X 重 写 的 规 则 结 构 ， 理 论 计 算 机 科 学 106（1992），61{86.[5] 克里斯滕森，S.，进程代数中的可判定性与分解毕业论文，爱丁堡大学计算机科学系，1993年。[6] Groote，J.F.，和F.范德拉格，结构化操作语义和互模拟作为一个同余，信息与计算100（2）（1992），202{260。[7] 迈尔河，巴西-地结合Petri网和PA过程，TACS '97会议录，计算机科学讲义，第1281卷，Springer-Verlag，1997，547{561.[8] 迈尔河，巴西-地Process rewrite systems，Electronic Notes in TheoreticalComputer Science7（1997）。7[11]《易经》云：“君子之道，焉可诬也？有始有终。在[12]中，还证明了MSA类是Petri网的严格子类。在[15]中证明了fcBPP是MSA的严格子类，并且MSA系统的可表达性不会通过用nite约束系统来丰富它们而改变。
我的内容管理
展开
