高维自动机软件工程规范研究

1《理论计算机科学电子札记》68卷第1期（2002）网址：http://www.elsevier.nl/locate/entcs/volume68.html11页关于高维自动机的特殊化？理查德·巴克兰新南威尔士大学澳大利亚悉尼迈克尔·约翰逊麦考瑞大学澳大利亚悉尼多米尼克·维里蒂麦考瑞大学澳大利亚悉尼摘要高维自动机（HDA）作为并发过程的模型已得到广泛的研究目前的工作主要集中在发展所需的有向代数拓扑概念分析HDA，以确定其计算机科学性质（死锁，安全，不可达状态等）。相反，本文关注的是HDA的软件工程，并详细介绍了HDA的进程代数操作的规范。这些规范适用于三次HDA，但也适用于最初由Buckland提出的显式选择高维自动机（ECHDA）。我们开始吧！-多重图，一个比粘贴方案更容易使用但比立方复形更一般的图形概念！- 多重图中，讨论了并发、协商和冲突选择的三种情况，指出了“死锁选择”可能产生于冲突选择的交叉，并指出了常见的软件工程关系与选择关系相对应.？ 研究部分由澳大利亚研究委员会支持在CC BY-NC-ND许可下开放访问。Buckland，Johnson & Verity21引言高维自动机（HDA）是非确定自动机的自然推广HDA由Pratt [14]引入，作为基于非确定性自动机的并发系统模型的扩展，以便也对真正的并发进行建模。特别是，普拉特需要具有更高维度结构的自动机，以在真正并发的情况下获得调度和自动机之间的Birkho对偶。自从Goubault [8]的开创性工作以来，HDA已经被广泛研究。最近的工作主要集中在有向代数拓扑学的发展，用于分析HDA，以确定重要的属性，如安全，死锁，和不可达的状态。例子包括Goubault的进一步工作，例如[11]和[10]，Gaucher的一系列论文[3]，[4]，[5]，[6]，[7]以及Grandis [12]和Raussen [16]的工作参见《计算机科学中的数学结构》特刊[9]。本文研究了基于进程代数运算的HDA规范，据作者所知，这是第一篇详细研究这一问题的论文。HDA已经被各种各样地定义为n-范畴[14]、立方复形[15]和粘贴图式[4]。 在大多数情况下，所有的细胞都是立方体。因此HDA的规范必须能够处理在某些适当的三次高维图概念上的运算。然而，我们设计的操作工作在更一般的高维图，原因如下。在[1]中，第一作者认为，显式选择应该被纳入过程模型，他提出了一个概念，我们现在称之为显式选择高维自动机（ECHDA）1基于粘贴计划[13]。 虽然本文没有特别讨论ECHDA的情况，但值得注意的是，额外的一般性几乎没有增加过程代数运算的复杂性，只要使用适当的高维图的概念。在本文的其余部分，我们将集中讨论ECHDA，但要提醒读者，HDA是ECHDA的一个简单特例，因此我们所说的也适用于HDA。非确定性自动机可以简单地表示为有向图，其中节点被解释为状态，边被解释为事件。由于ECHDA（和HDA）重要地利用了高维结构，它们不能用普通的有向图来表示这 篇文章的主要目的之一是介绍！- 多重图是高维图的一个相对简单的概念。 了！多重图用于表示ECHDA，其方式与图用作非确定性自动机的表示相同。此外，我们还精确地展示了如何构建！多重图对应于过程代数的基本术语。就像非确定性自动机，n odesof！-多重图被解释为1ECHDA是复数缩写。 相当独特的是，当我们需要引用一个明确的选择高维自动机时，我们将其称为ECHDon。Buckland，Johnson & Verity3状态和边缘被解释为事件。 更高维度的面孔！多重图用来表示显式选择和真并发. 有趣的是，[14]的早期草稿已经注意到了过去的局限性提出了\n-图的新概念。 在某种意义上！-多图提供了一个答案|！多重图为ECHDA提供了一个替代基础（因此也为HDA提供了一个替代基础，但也请参见本文的最后一段，其中指出了使用的主要限制！- 多重图作为HDA的定义）。其中一个广告的一个阶段！-多重图表示是1-这是一个伟大的人 ！多重图（只取节点和一维边得到的有向图）正是与系统相关的非确定性自动机的通常表示。 我们！多图很容易被已经有使用非确定性自动机经验的软件工程师使用。|额外的结构在一个！Multicraph用于工程师可以选择的额外规范（选择和并发）。你好！表示ECH DA的多重图 可以是相当高的维数，因此难以可视化和操作。可以说，当高维性来自于许多并发执行的进程时，它是系统性质的准确反映。相反，当高维是嵌套选择的结果时，有一个简单的解决方案称为at- tening，它可以降低- 多重图。[1]第6节中提出了展平，但本文首次完整地描述了展平操作。同样在[1]中，有人认为注意实际上是指定过程的一部分。我们现在有了更多的ECHDA和原型ECHDACASE工具的经验[2]，很明显，对于软件工程应用程序，必须经常使用注意力来降低复杂性。我们在第5节中展示了即使在没有选择规范的情况下如何atten。总之，ECHDA提供了一个很有前途的软件工程工具。本文为ECHDA提供了一个严格的数学基础（这是继续开发CASE工具所必需的），说明了基本的进程代数运算是如何在ECHDA上进行的，并对重要的注意运算提供了第一次形式化2！-多重图粘贴方案为ECHDA提供了基础，但它们有几个缺点。首先，它们要么难以定义，要么必须通过归纳构造而不是公理化来定义。在这两种情况下，他们都需要相当长的时间来详细介绍。此外，证明一个建议的方案确实是一个粘贴方案是相当困难的，这使得很难对粘贴方案进行新的操作。在本节中，我们！-多重图是一类相对简单的公理化描述的Buckland，Johnson & Verity4-+的高维图在下面的部分中，我们将定义上的操作！- 对应于顺序合成、选择、并发和关注的多重图。了！- 多重图本身并不容易定义，因为它们捕捉了高维图的一个非常微妙的概念。了！表明重图可以是任意高维的（n重图是n维的）。定义2.1 An！- 重图是一个集合X，X的幂集的一个子集U，它包含所有的单点子集，对于每个自然数i，有两个函数si;ti：U！U这样，si sj= si tj= si i j tisj= ti tj= ti i jsi sj= ti sj= sjji sitj= ti tj= tjji：注意，每对方程中的一个与另一个是对偶的，这里对偶意味着它可以通过选择一个下标，比如i，并将所有出现的si改为ti，反之亦然，从另一个得到。我们经常只陈述一半的结果，而把对偶结果隐式地留下。定义2.2如果sifxg=fxg，则称x为i-单元格.引理2.3元素x是i胞腔当且仅当tifxg = fxg。引理2.4对任意x，sifxg是i-胞腔.定义2.5对于最小的i，写出dimx，使得x是i-胞腔，并说x是dimx-维的。定义2.6对于最大的i，写出dimX，使得存在一个x2X，它是i维的，并且说X是dimX维的.上述四个方程是理论的基础，我们称之为st方程。 它们最初被用于定义！- [17]中的类别。选择字母s和t作为源和目标的助记符。每个元素x的一个！- 多重图对于每个i将具有i维源sifxg和i维目标tifxg。如果x是n维的，我们将把它画成从它的（n 1）维源到它的（n 1）维目标的方向.例2.7这里有两个二维的！-多重图：QaQ buqrv3QwQp-sQrX和pQ-sQsC+的Buckland，Johnson & Verity5两个人的距离！- 多重图（X;U;s;t）和（Y;V;s0;t0）被定义，当s（X）=t0（Y）=z，则X和Y在z上不相交. 它有c或re-我我我我为了满足条件s（X）=t0（Y），或者为了在第一种情况下，具有作为0维源（0-源）fpg和作为1-源fa; bg，以及作为0-目标frg和作为1-目标fxg。 同样，在第二种情况下，具有作为1-源fu;v; wg和fu;v; wg具有作为0-源p和作为0-目标s等。注意，st方程是满足的，只要单元z被绘制为n维we要求它是n-单元（即sifzg=fzg，对于所有in和对偶）。例2.8多重图是一个！- 多重图，其中每个元素都是1-胞元：节点是0-胞元，并且多重图是图当且仅当s0fxg和t0fxg对所有x都是单例。3进程代数运算下面的小节将详细介绍基本进程代数操作和上的构造之间的对应关系。- 多重图。顺序组合结构3.1两种ECHDA的顺序组成，我我我00回应！- 由（X[Y;U [V））给出的具有继承的源和目标的函数（注意sfzg =tfzg =z=s0fzg =t0fzg）。在制定详细工艺规范的过程中阳离子时，X或Y之一将需要被替换为y同构！-00确保X和Y不相交。通常我们会忽略这些没有评论的修改。如果我们确实需要评论，我们将称之为连贯性重新标记。选择（Choice）在非确定性自动机中，表示为有向图，在状态s的两个进程X和Y之间的选择由s处的传出分支表示，X是分支的一条路径，Y是另一条路径。在ECHDA中，路径之间的空间用二维单元格标记，该单元格表示用于确定X或Y是否出现的选择条件。选择条件可以是普通的if。. . 别的. . 语句、概率性指定的选择、显式非确定性内部或外部选择、始终 选 择 （ if X else Y |always choose Y ） ， never choice （ 如 果TRUEX，则Y|永远不要选择Y）等。例如，RST！例2.7所示的多重图将表示在进程a然后b和进程x之间的选择，选择条件由单元指定（其细节未显示，就像事件a的细节未显示一样）。Buckland，Johnson & Verity6当X和Y不相交时，定义了多重图（X;U;s;t）和（Y;V;s0;t0治疗选择的三个方面尤其值得注意。首先，选择条件由有向胞元表示在大多数情况下，但不是所有情况下，选择是不对称的|if B then X else Y通常不同于if B then Y elseX，并且在ECHDA中表示为！- 多重图一个可以从另一个通过反转选择条件的方向获得其次，ECHDA是强对偶的。 很少有人会争辩说，为了在X和Y之间 做 出 选 择 ，必须有一个X和Y都能发生的状态s。通常在规范中，X被构建，Y被构建，然后尽管它们似乎开始于不同的状态，但使用相干重新标记（通常是隐含地）来给它们一个共同的开始状态。或者，引入一个新的起始状态s，并引入两个空转换以分别将s与X和Y的起始状态连接。在ECHDA中，我们双重地要求X和Y具有共同的nal状态，或者通过相干重标记，或者通过引入新的状态t和分别从X和Y的nal状态到t的两个空跃迁。因此，选择条件总是由例2.7所示的过程所限定的单元格。它们从来都不像非确定性自动机中经常出现的那样只是开分支注意，这并没有在ECHDA中的选择和非确定性自动机中的选择之间引入语义上的区别|它没有区别，并且更好地对应于基本编程实践，具有状态t，其表示（比方说）语句ifBthenXelseY的完成，并且其发生在X的最终状态和Y的最终状态之后。第三，从我们已经说过的话来看，因为ECHDon可能是二维的，与非确定性自动机中的过程相反。如果我们希望能够在任意过程之间引入选择单元，我们将需要做出一个定义，该定义允许例如在两个二维ECHDA之间进行选择，从而产生三维ECHDon，或者在一维ECHDon和三维ECHDon之间进行选择，从而产生四维ECHDon，等等。构造3.2两个ECHDA之间的选择P由！-我我我以及当最高维数之一是n维时。相应的！ -multigraph 的 构 造 如 下 。 它 具 有 作 为 元 素 X [Y] 以 及 一 个 新 的（n+1）维元素p，对于0in，具有不同的新元素sifpg和tifpg<，并且对于每个i，具有0 2时，n维的注意力集中！- 重图是（n 1）维的！- 多重图，其（n1）维元素由图的（n1）维元素组成！- 重图的n维元素，以及与之对应的新的（n 1）维元素. - 多重图。 对于n维的q，将sn1fqg中的（n1）维元素重新解释为它们的选择条件与q的选择条件的析取，将tn1fqg中的（n1）维元素重新解释为它们的选择条件与q的选择条件的合取.对应于q的新的（n1）维元素具有+Buckland，Johnson & Verity10as（n2）-源tn2fqg和as（n2）-目标sn2fqg。值得注意的是，虽然这个过程似乎会引入循环，但我们在一篇准备中的论文中表明，在所有实际情况下，这些循环都将被消除，因为它们涉及不可执行的跟踪。6今后工作现在我们有了过程代数运算的完整形式定义！- 多重图，我们可以进一步发展文[2]中所描述的CASE. 与此同时，还有其他重要的理论问题：(i) ECHDA被设计为在软件工程师选择使用的任何选择条件下工作。然而，为了实现atening，我们需要指定在合取和析取下的选择的相互作用，并且对于某些选择条件，这种相互作用是相当微妙的。例如，当上面的q具有非确定性的选择条件时，重要的是我们只评估这些条件一次，并在需要它们的地方替换它们。我们已经对选择的代数和逻辑进行了编目，但是我们需要对其进行扩展，以包括尽可能广泛的选择条件类型。(ii) 注意力在不同阶段的使用在一个规范和重新定义，neme ntcyclegeneratesanequi v alence on！- 多重图的互模拟等价。我们才刚刚开始探索这种等价的详细性质最后，我们应该注意到这一点！- 多重图不是n-图的完美概念，因为它允许“病态”行为，而这种行为在我们的过程代数中没有标准的解释。相反，！多重图提供了一个框架，我们可以很容易地表示ECHDA及其操作。 如果我们对已经捕获了ECH D A上的所有适当操作感到满意，那么收集！用这些运算可以从基本胞元构造出的n-多重图大概是n -图的一个热门类别。检验这一点的标准是某种游离性，这一点将在其他地方加以说明。引用[1] R. Buckland，Choice as a rst class citizen，inIntensional Programming I，eds Orgun and Ashcroft，（1996）249{259，World Scienti c.[2] R. Buckland和M. Johnson，ECHIDNA：一个操作显式选择高维自动机的系统，AMAST'96，计算机科学讲义1101（1996）587{591.[3] P. Gaucher ， >From concurrency to algebraic topology ， ENTCS ， 39（2000）。Buckland，Johnson & Verity11[4] P. Gaucher ， Homotopy invariants of higher dimensional categories andconcurrency in computer science ， Mathematical Structures in ComputerScience，10（2000）481{524.[5] P.Gaucher ， Combinatoricsofbranchingsinhigherdimensionalautomata，Theory and Applications of Categories，8（2001）324{376.[6] P. Gaucher，Investigating the algebraic structure of dihomotopy types，ENTCS，第52话出现[7] P. Gaucher， 关 于高 维自 动 机的 球形 同源 性 ， 拓扑 学与 几何 分类，（2002），即将出版。[8] E. Goubault，The Geometry of Concurrency，PhD thesis，ENS，1995。[9] E. Goubault（ed），几何和并发性，计算机科学中的数学结构特刊10（2000）409{573。[10] E. 古博湖Fajstrup和M.陈文，“并发系统中的死锁检测”，计算机科学学报，1998年，第332卷，第347页。[11] E. Goubault和M. Raussen，Dihomotopy as a tool in state space analysis，拉丁文'02，计算机科学讲义2286（2002）16{37。[12] M. Grandis，定向同伦理论I：基本范畴，预印本，2001年。[13] M. Johnson ， n- 范 畴 粘 贴 的 组 合 ， JournalofPureand Applied Algebra62（1989）211{225.[14] 诉王志华，“几何并行建模”，北京大学出版社，（1991）311{322。[15] V. Pratt，Transition and Cancellation in Concurrency and Branch Time，Mathematical Structures in Computer Science（2002）。[16] M. Raussen，关于并发几何模型中的路的分类，计算机科学中的数学结构10（2000）427{457。[17] R.H. Street ， 定 向 单 形 的 代 数 ， 纯 粹 与 应 用 代 数 杂 志 49 （ 1987 ）283{335。