抽象的分类方法：图变换系统的模块化

网址：http://www.elsevier.nl/locate/entcs/volume51.html14页图变换系统的抽象模概念（Marta Simeoni2Dipartimento di Informatica，Universita `Ca Foscari' di Venezia摘要图变换系统是一种著名的形式化规范技术，它支持基于规则的系统动态行为规范。近年来，许多图变换系统的规范语言被开发出来，为了处理大型复杂的图变换规范，提高规范的重用性，隐藏实现细节，需要采用模块化技术。在本文中，我们提出了一个抽象的分类方法，图转换系统的模块化。模被称为cat{模，并定义在图变换规范和态射的一般范畴cat上。本文描述了cat{-模的主要特征和性质，它们的互连运算，即模的并、合成和还原，以及这些运算之间的相容性。1引言图形文法和图形转换系统是用于图形和图形结构的操作的公知的基于规则的图语法通常指定图语言，而图转换系统通常描述动态演化系统，其中图是状态，图转换是状态转换。近年来，人们开发了许多用于图文法和图变换系统的规范语言。例如，使用 图重 写系 统的 编程 （PROGRES ） （ 参见 [17] ） 和代 数图 语法（AGG）系统（参见[7]）。因此，需要模块化技术来处理大型和复杂的图形转换规范，以提高规范的重用性和隐藏实现细节。1 这项工作得到了EEC TMR网络GETGRATS（图形转换系统的一般理论）的支持。关于该主题的完整调查是与Martin Gro e（Rhode，Dirk Janssens和Francesco ParisiPresicce）合作的结果2 电子邮件：simeoni@dsi. uni ve. Itc2002年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2关于这一主题，已经有各种各样的建议。第一种方法已在[3]中介绍，但较成熟的方法是PROGRES包（见[16]）、GRACE图变换单元和模块（见[10，11]）以及DIEGO模块（见[18]）。所有这三种图转换系统的模块化方法都满足了对模块的基本要求，这意味着它们支持实现隐藏和使用模块的关系（即指定模块如何使用另一个模块导出的功能的可能性）。在PROGRES、GRACE和DIEGO方法中缺少的是关于模块化的正式抽象理论，以及关于模块互连操作之间的兼容性属性和模块组件的行为保持的具体结果。后者是图变换规范满足的主要要求，因为它们描述了系统的动态行为。对于模块，这意味着导出中指定的语义需求（分别为导入）接口，必须保留在主体组件中。在本文中，我们提出了一个抽象的分类方法，图转换系统的模块化，它已在[15]中介绍，并实例化的局部动作系统（见[9]）和类型化图转换系统的双推出方法（见[2]）。抽象模的概念是受[6]中引入的代数规范模的启发。在图变换规范和态射的类属范畴cat上定义了模，称之为cat{模。cat{模块有三个组件：导入接口、导出接口和主体。接口描述了与其他cat{模块的关系。更准确地说，导出接口指定模块向其他模块或环境提供的功能，导入接口指定其他模块所需的部分，并且可以在主体中使用以实现要导出的功能。每个组件都是一个图形转换系统规范，它由一组定义其基本步骤的图形转换规则组成。模块组件之间的互连建模的态射的图形转换speci阳离子。在代数规范模的类似互连运算的指导下，我们定义了模的并、组合实现了模块之间的使用关系，而组件实现了一种继承关系。我们证明所提出的操作之间的兼容性：一个重要的是兼容性的组成方面的模块。本文独立于任何特定的图变换方法，通过指出cat {模块在一个具体的3框架.这种抽象形式化的优点是，我们得到给出了一种通用的模块化方法，并给出了具体但仍然通用的结果，如cat{模块的互连操作的定义和相容性。 此外，cat{modules over一种具体的方法自动地通过提供形式证明来说明CAT{模块}本文的结构如下。第2节描述了cat{模块的主要特征和性质，并在第3节中给出了cat{模块的互连操作及其兼容性。第4节提出了一些结论性意见。2cat{模块在本节中，我们引入了图变换系统的抽象模概念，其灵感来自代数规范模（见[6]）。图转换系统由一组规则名称和与每个名称相关联的底层图转换规则的映射指定。更确切地说，我们考虑具有在特定类型系统上类型化的规则的规范，例如，通过节点和/或边标签的字母表或[1]意义上的类型图来建模。由于我们对范畴设置中的模的定义很感兴趣，我们假设图变换规范和态射的类属范畴猫是可以定义的。因此，我们定义了cat上的抽象模块，并称它们为cat{模块。在下文中，我们描述了它们的主要特征和属性，并指出了在具体框架上的cat{模块的任何实例化所要满足的具体要求。cat{模块有三个组件：导入接口、导出接口和主体。这三个组件中的每一个都是一个图形转换Speci。阳离子。因此，规则不仅存在于主体组件中，而且存在于接口中，这意味着与编程语言模块不同，除了导入和导出特征的名称之外，还可以指定它们的行为。我们现在继续逐步描述cat{模块组件及其互连的作用和意义。导入接口导入接口指定由其他模块提供的功能，并在主体组件中使用以实现新功能。导入接口为空的模块是自底向上开发模块化系统的基本构建块。然而，除了自底向上的技术之外，cat{modules还允许自顶向下的模块化系统开发。事实上，从其他模块导入的特性不仅由它们的名称指定，还由描述它们行为的规则指定这4允许其他模块推迟它们的具体实现，并实现了支持泛型导入的机制。此外，由于没有明确引用提供导入特性的具体模块，因此可以使用实现相同行为的任何模块。这种导入机制的一个优点是，它可以有选择地导入特征。一般来说，这在编程语言模块的情况下是不允许的，其中必须导入导入接口中导出接口导出接口指定模块实现的功能，并向外部环境输出。同样，导出的特性不仅由它们的名称指定，而且还由描述它们的行为的规则指定：在这种情况下，规则指定了它们实现的前置条件和后置条件导出接口是模块从外部环境中唯一可见的组件，即通过导出类型系统键入的导出规则是唯一可访问的资源。这意味着导出规则的实现细节隐藏在模块内部身体cat{模块的主体包含所需的所有本地和导入规则 以实现导出的功能。支持实现的想法是，每个导出的功能都是通过身体规则的适当组合来实现的。导出接口的类型系统旨在成为主体类型系统的子类型：这样主体可以使用从外部环境不可见的私有类型，即支持数据隐藏。此外，导入接口的类型系统通常是主体类型系统的子类型：这样，本地规则可以使用导入类型之外的其他类型cat{模块的三个组件必须以这样一种方式相关联，即导入的特征嵌入到主体中（以便主体可以使用它们），导出的特征使用主体的规则（即本地规则和导入的规则）实现。这意味着，必须建立两种关系：一种是导出接口和主体之间的关系，另一种是导入接口和主体之间的关系。他们两个都必须联系起来首先是两个组件的类型系统，然后是它们的规则。导入{主体关系cat{模块中的import{body关系的任务是将导入的规则包含到body中，以便body可以使用它们来实现导出的规则：我们通过单射纯态射对其进行建模5普通态射将源类型系统与目标类型系统相关联，并在规则之间建立一对一的对应关系：它将源规范的每个规则与目标规范的单个规则相关联，以这种方式，源规则在目标类型系统上的转换恰好产生相关联的目标规则。我们要求纯态射具有以下性质要求：规范和普通态射定义了一个在推出下闭的范畴。导出{主体关系导出{body}关系的形式化非常复杂，因为导出接口的每个规则都必须通过body的规则与其实现相关联：它由元素态射建模我们使用资源来支持执行任务。要素是复杂系统规范开发的基本步骤。从系统行为的抽象描述开始，逐步修正产生越来越多的具体规范，这些规范最终应该可以在机器上直接实现。一个更具体的规范对一个更抽象的规范的回复是通过将更抽象的规范的每个规则与更具体的规范的规则的组合相关联来给出的，以这样一种方式，组合规则（即由组合产生的规则）与抽象规则在ner类型系统上的转换相一致。如前所述，导出类型系统旨在成为主体类型系统的子类型：通过通过元素对导出{主体关系进行建模，我们实现了数据和实现隐藏，因为主体的内部类型和内部步骤都对模块用户不可见（他们只能通过导出接口访问模块任何普通态射都可以嵌入到一个元素态射中，将每个抽象规则与一个具体规则相关联。对Speci阳离子和元素态射的第一个要求是以下之一：要求：Speci cations和renement morphisms定义了一个范畴，这个范畴有speci cations和plain morphisms范畴作为此外，我们还需要以下具有包含性质的推出，以重新元素态射，需要在下一节中定义cat{模块之间的组合操作要求：如果一个态射是单射纯态射，则特殊和元素态射范畴在推出下是闭的。诱导态射又是一个元素和一个单射纯态射（即单射纯态射被保持）。已经描述了cat模块的组件及其互连，6EXPRImpM BJODBODKRSWQIMP tEXEp u我们可以具体地形式化一个cat{模块如下。M R定义2.1[cat{Module] A cat{module MOD =（IMP！BODEXP）由IMP，BOD和EXP给出，一个单射纯态射m：IMP！BOD，和一个元素r：EXP！ 身体它可以通过以下方式可视化：图1示出了导出两个规则p和u的模块的示例，这两个规则p和u分别通过规则w; q;s和s; k; r的适当组合在主体组件中实现（重新定义）。其思想是，元素态射指定了如何组合主体规则，以实现导出接口的相应规则。该模块导入一个规则t，该规则通过一个从t到q的纯态射映射被包含到body组件中。Fig. 1. 的模块由于纯态射只是元素态射的特殊情况，猫模的分支和态射都可以在规范和元素态射的范畴中建模。因此，一般范畴猫就是特殊态射和元素态射的范畴语义猫模的语义是由它的三个组成部分的语义给出的，这三个组成部分由特定态射诱导的映射联系起来。然而，这种诱导映射的存在性必须是明确要求的。要求：规范态射诱导语义上的映射。由于导出接口是cat{模块中唯一可以从外部环境看到的组件，因此只有导出接口语义是可见的。7E，，IBr10的米0我们已经指出cat{模块允许其他模块实现的功能的通用导入，并用于实现导出的功能。泛型导入使得将每个模块视为具有完全定义的语义的自包含实体成为可能。因此，模块系统的语义可以从其模块组件的语义中定义。这种组合语义在编程语言模块中是不允许的，其中模块的语义仅在导入接口处所需的所有模块实际上都被导入的情况下才被定义。行为财产保全为了适当地对系统的动态行为建模，我们需要对变换规范和形态进行图形化的主要属性是以下行为属性的保持：要求：图变换规范的动力学行为必须沿着普通态射和元素态射保持。此属性对于cat{模块的导出{体态射}特别重要：由于导出接口是从外部环境中可见的模块的唯一组件，因此保留导出语义以及元素定义是所实现功能的正确性标准。我们通过描述关联cat{模块的基本方法来结束本节，这是下一节中定义互连操作的基础。cat{模可以通过cat{模态射来关联，由一个三元组的普通态射组成，与它们的内部模连接相容M R定义2.2[cat{模态射]设MOD =（IMP！ BODEXP）m0r0MOD0=（IMP0！ BO D0EXP0）beca t{模块。Acat{monumerous-phismm o d：February2009付款日期0 是一个三元组（m o d：IMP！ IMP0; 每 日 一 次：BOD！ BOD0;mod经 验！EXP0）的纯态射，如Ch，以下是交换图猫。ImpmBODBODEXPmodI=JmodBJmodB=J思维方式JIMP0BOD0BOD0EXP0在定义了cat{模和cat{模态射之后，我们可以证明以下命题：命题2.3 [15]cat{模和cat{模态射形成一个叫做MOD的范畴.cat{模块之间的另一个有用的关系是子模块关系：如果存在一个，r8MRca t{单态射mo d =（mo d I;mo d B;mo d E ）：MOD！付款日 期0 因此，body组件之间的普通态射mod B保持导入规则和本地规则分离：该条件确保两个组件中的规则具有相同的角色。定义2.4[子模块]设MOD =（IMP！BODEXP）和m0r0MOD0=（IMP0！ BO D0EXP0）btoca t{modules. MOD是一个子模块的 MOD0 ， 如 果 存 在 一 个 ca t{m o d = （ m o d I;m o d B;m o d E ） ：MOD！付款日期0你好，我是说你好！BOD0将导入的规则映射到导入的规则，并将本地规则映射到本地规则。模态射称为子模态射。在下一节中，我们使用子模关系来定义cat{模的并集。然而，为了能够进行这种操作，必须要求具有以下性质：要求：规范和纯态范畴中的推出在规范和保留态范畴中被保留。有了这个性质，我们可以证明范畴MOD关于子模关系（这是定义并运算的基础）有推出。命题2.5 [15] MOD有关于t子模的推出。在本节中，我们描述了cat{模块的组件和互连，它们的语义以及它们的基本属性。此外，我们还介绍了cat{模之间的基本关系。在此基础上，我们在下一节中定义了cat{模块的一些可能的互连操作。3cat{模的一个代数模块已被引入作为复杂规格开发的结构化手段。因此，除了定义图变换系统的模块概念之外，定义模块的互连操作也很重要。在代数规范模运算的指导下（见[6]），我们引入了cat{模的类似运算，即并、复合和模的消去.由于范畴方法，模块之间的连接是由态射建模的，操作的结果是由它们的通用属性抽象指定的。3.1cat{modules两个模块MO D 1和MO D 2的并集由以下定义： 显式定义的公共子模块，其中子模块关系已经在定义2.4中引入。这允许显式控制哪些项9....MR！国防部，0MOD 1和MOD 2中的每一个都被认为是共享的，而哪个被认为是本地的，而不是所选择的名称。 在这种方法中，来自MOD 1和MOD 2的项目在并集中被识别，当且仅当它们是MOD 0中的一个对应项目的图像，其元素与MOD 1和MOD 2的结合使识别显式。更具体地说，联盟国防部1 国 防 部 0 首先取MOD 1和MOD 2的相应分量的不交并，然后识别MOD 0中包含的公共部分，可以获得MOD 2。定义3.1假设MOD 1 关于MOD2 betwoca t{m odules}并让MOD0beb第二天 ， 通过子模态射m o d 1：MOD 0！ MOD 1和MOD 2：MOD 0！第二章. 联盟MOD 3=MOD 1MOD0 MOD 1和MOD2的MOD 2w.r.t. MOD 0、mod 1和mod 2是通过MOD中的MOD 0、mod 1和mod 2的推出而给出的。. ... .，c.国防部，1 、、、、、、p：o、、，zMOD2. .. .z，. CMOD3在命题2.5中陈述了MOD关于t子模的推出的存在性。当联合操作与下面描述的组合操作结合使用时，它特别有用：在这种情况下，它允许导入由不同模块实现的功能。最后，下列事实可以只用所涉及范畴的标准性质来证明。对于它们的完整证明，我们参考[12]，其中它们是针对代数speci cation模证明的。命题3.2（i）并集和子模关系的相容性：MOD1和MOD 2是MOD1MOD0的子模块 MOD2(it由命题2.5和推出的标准性质得出）;（ii）工会的集体性：如果MOD 0 是MOD1的子模块 和MOD 2，并且MOD 3是MOD 2和MOD 4的子模型，则（周一 至周五） 2）MOD3 MO D 4 =周一至周五 1MOD0 （MO D 2MOD3MOD 4）.3.2cat{模块的组成组合操作实现cat{modules：a module}MOD=（IMP！BODEXP）可以使用另一个MOMOD0=（IMP0 MBOD0REXP0）如果第一个的导入接口可以与第二个接口的导出接口通过一个纯态射，称为接口10、、、勒布尔，h，0r10的IMPm BOD.H1H2H1H2态射，MOD的导入接口和MOD 0的导出接口之间，h：IMP！经验0：由MOD和MOD0组合而成的新模型具有MOD0的接 口、MOD的扩展接口以及BothMOD和MOD0的特性。定义这个操作的基本范畴要求是范畴cat的包含推出属性，它允许构造组合体。mrm0定义3.3设MOD=（IMP！ BODEXP）和MOD0=（IMP0！BOD0 EXP0）btwca t{modulesandleth：IMP！经验0 be平原态射，称为界面态射。该组合物MOD00=MOD 0MOD由MOD00定义 =（IMP00mmBO D00EXP00）其中：IMP00=IMP0，EXP00=EXP，BO D00是cat中下图的推出对象（m和r是诱导态射）。EXPRJHJp：o：M...R...J__BOD00注意，接口态射h可以仅仅是单位态射h= id，即总是定义合成操作事实上，我们可以恢复h6=idcasebyy ， 使 用 中 间 值 {m0} （ EXP0IDEXP0IMP），并将其与给定的模块组合.为了实现不同模块的特征导入，可以组合使用组合和合并操作：如果一个模块MOD需要导入由不同模块MOD 1和MOD 2实现的特征，则应首先执行MOD 1的合并 和MOD2，然后将所得模块与MOD组合。关于并运算，下面的合成的基本性质可以直接从它们的泛性质中推导出来，如[6]中关于代数规范模的显式所示。建议3.4（i）组合物的分配比：（MOD00）由于标准部件的性能，MOD=MOD00（MOD0MOD）HIm0米0经验0r10的11IMPm BOD我0BEr10的R0000pushouts的位置EXPRJ.H1 J经验0r10 的m0Jm00IMP 0H2JEXP00r00 JBOD 0 _____________________________________________________________________________________________________J。..... .JJIMP00BOD00_J_BOD000(ii) 组件和子组件的兼容性：如果MOD 1是MOD 3的子组件第二 天 ， 是MOD 4 的子模块 然后（MOD 1h1 MOD 2）是（MOD 3）的子项 MOD4），其中h1和h3互射分别从MOD 1到MOD 2和从MOD 3到MOD 4。(iii) 并、合的对称分配性：设MOD 0 bea sub-MOD模块，MOD和MOD0 按付款日期0付款，付款日期0。Let1 20 1 20h i：MOD i！MOD，i= 0;1;2是界面态射，使得h 是H1和H2的限制。然后0 0（周一 至周五） MO D 2）1小时1小时 H2 （MO D 1MODMO D 2）=00 0（每月1日） MOD 1）MOD0小时M OD0（每月2日）MOD 2）的情况。3.3cat{modules}的关系单种之间的关系可以推广到cat{模。我们说一个猫模被另一个猫模环化，如果在它们对应的组件之间存在三个与内部模连接相容的定义这个操作没有特殊的要求：它实现了cat{模块的一种继承关系。mrm0定义3.5设MOD=（IMP！ BODEXP）和MOD0=（IMP0！生化需氧量EXP0）btwca t{模块。Acat{m one n ementrMOD=（r; r; r）：MOD！付款日期0 是环ntsr的三元组：IMP！IMP0，I B E Ir：BOD！ BO D0和r：IMP！实验0表明，在猫里通勤。IM PmBOD，，EXPrI=rB=rEJm0Jr0JIM P0BOD0，，经验0021201010111注意，在2.2节中定义的cat{模态射是cat{模元素的特殊情况。此外，请注意，环化模块的每个组件都可以包含“本地规则”，这些规则不依赖于更抽象的模块的规则，即环化模块可以专用于抽象模块不可见的功能。我们通过展示cat{模块元素关于cat {模块的并集和合成的两个兼容性性质来结束本节。为此，类似于范畴MOD，我们定义了cat{模和cat{模元素的范畴MOD-Ref，并证明了它在推出下是闭的，如果其中一个涉及的态射只是内射cat{模态射（直接从具有包含性质的推出中得出建议3.6[15]任何空气（rMOD：MD 0 ！付款日期 1;付款日期：付款日期 0 ！ MOD 2）由一个猫{模元素rMODD和一个内射猫{模态射mod}组成，在MOD-Ref中有推出。本文讨论了cat{模元素w.r.t. cat{模块的联合或组合基于以下兼容性条件：定义3.7令m：MOD 0 ！ Mod1 是一个亚同态，rmod0 ：MOD0！MOD0 做一只猫。 猫{模块re ne-门Mod1：MOD1！MOD0 与m和r相容Mod1若有存在子模态射 ：MOD0 ！MOD0 这样，下图通勤：MODmMODr模式Jr模式J00米0MOD0有了这个定义，我们可以证明以下性质：命题3.8[15]cat{模元素的并集是该并集的cat{模元素。cat{模块元素的组合是组合的cat{模块元素。4结束语本文提出了图变换系统的模化的抽象范畴方法.在[15]中研究了这种方法的两个具体实例：第一个是基于双推出方法的类型化图变换系统，第二个是局部作用系统。cat{模的灵感来自代数speci cation模。然而，这两种规范形式主义之间有一个主要的概念差异0MOD13图变换系统规范用于形式化地规范动态演化系统。因此，保持系统的动力学行为很重要。这种动态方面在代数规范中不存在，因为它们中的每一个都指定了一个代数（初始语义）或一类代数（松散语义），这些代数仅对组件的静态功能视图进行建模。猫{模块和其他模块化的方法图转换之间的关系和区别也需要讨论。然而， 由 于篇幅 限制 ，我 们参考[15] ， 详细 介绍了 主要 方法及 其与r.t.cat{modules.未来工作的想法都与猫{模块的其他实例化的发展，以及关系的扩展。在第一种情况下，我们感兴趣的是intantiating猫{模块的任何形式主义满足所需的属性（例如图变换的单推出方法，代数重写，Petri网）。在第二种情况下，我们感兴趣的是扩展用于建模case distinctions的关系，如if{then{else和case构造以及迭代。 在这个方向上的第一次尝试可以在[8]中找到，其中讨论了在双推出方法上类型化图转换系统的模块的元素的一些扩展。引用[1] A. 科 拉 迪 尼 Montanari 和 F. Rossi“Graph processes”Special issue ofFundamenta Informaticae，Vol. 26（3，4）pp. 241{266（1996）[2] A. 科拉迪尼 Mo n tanari，F. Rossi，H. 埃里格河 他很好，M。Lo we“代数方法图变换第一部分：基本概念和双推出方法”在[14]，pp. 163{246[3] H. Ehrig，G.Engels“Pragmatic and Semantic Aspects of a Module Conceptfor Graph Transformation Systems”Proc. 5th International Workshop onGraphGrammarsandTheirApplicationtoComputerScience，Williamsburg'94，LNCS 1073，pp.137{154（1996）[4] H. Ehrig ，G.恩格斯J. Kreowski， G. Rozenberg 编，“Handbook of GraphGrammarsandComputingbyGraphTransformation ， Volume2 ：Applications，Languages and Tools”World Scienti c（1999）[5] H. Ehrig，H.J. Kreowsky，U.蒙塔纳里湾Rozenberg编，“Handbook of GraphGrammarsandComputingbyGraphTransformations ， Volume3 ：Concurrency，Decomelism，and Distribution”World Scienti c（1999）[6] H. 埃 里 希 湾 Mahr“Fundamentals of Algebras Speci cations 2 ： ModuleSpeci cations and Constraints”EATCS Monographs on Theoretical ComputerScienceVol. 21 Springer Verlag，Berlin（1990）14[7] C. Ermel，M. Rudolf，G. Taentzer的“AGG方法：语言和环境”[4]，第10页。487{546（1999）[8] M. Gro e{Rhode ， F.Parisi Presicce ， M.Simeoni“Formal Software SpecicationwithRementsandModulesofTypedGraphTransformationSystems”Journal of Computer and System Sciences，待发表。[9] D. Janssens“Actor Grammars and Local Actions”，[5]，pp.57{106（1999）[10] H-J. Kreowski ， S. Kuske“On the Interleaving Semantics of TransformationUnits { A Step into GRACE}”，LNCS 1073，pp. 89{106（1996）[11] H-J. Kreowski，S. Kuske“Graph Transformation Units and Modules”In[4]，pp. 607{638[12] F. Parisi Presicce“模块规格操作的内部和相互兼容性”技术报告86-06 TUBerlin（1986）[13] F. Parisi Presicce，“Transformation of Graph Grammars”，LNCS 1073，pp.428{ 442（1996）[14] G. Rozenberg编，“Handbook of Graph Grammars and Computing by GraphTransformations，Volume 1：Foundations”World Scienti c（1998）[15] M.Simeoni“ACategoricalApproachtoModularizationofGraphTransformation Systems using Re nements”PhD Thesis，Universita La Sapienzadi Roma（2000）[16] A.史昌湖rr，A.Winter“UMLPackagesforPROgrammedGraphRewritingSystems”Proc.6thInternationalWorkshoponTheory and Application of Graph Transformation（TAGT'98），Paderborn，LNCS 1764，pp. 396{409（1999）[17] A. 史 昌 湖rr ， A.Wi nter ， A. Zundorf“ThePROGRESapproa ch ：LanguageandEnvironment”in [4]，pp. 547{668（1999）[18] G.泰恩泽，A.史昌湖RR “迪戈，另一 步骤 去沃兹一 图变换系 统 的 概 念 ” ， Proc.GraphRewritingandCommunication ，SEGRAGRA'95ElectronicNotesofTCS，Vol.2，（1995）http://www.elsevier.nl/locate/entcs/volume2.html