可在www.sciencedirect.com在线获取理论计算机科学电子笔记298(2013)165-178www.elsevier.com/locate/entcs基于开映射的高维自动机的历史保持双相似性乌利·法蒂贝格·阿克塞尔·莱盖INRIA/IRISA,Campus de Beaulieu,35042 Rennes CEDEX,France摘要我们表明,历史保持高维自动机的双相似性有一个简单的表征直接在高维过渡。这意味着它对有限个高维自动机是可判定的。为了达到我们的特征,我们应用开放的映射框架的Joyal,尼尔森和Winskel在类的开折的precubical集。关键词:高维自动机,保历史双相似,同伦,开折,并发1引言过程行为等价的主要概念是Park [31]和Milner [27]引入的互模拟它之所以引人注目,是因为它具有良好的代数性质,允许使用模态逻辑、不动点或博弈论进行几个简单的刻画,并且通常具有较低的计算复杂度。互模拟,或者更确切地说,其底层的转换系统语义模型,适用于动作的并发性与非确定性交织相同的设置;使用CCS符号[27],|b = a.b + b. a。然而,对于某些应用,这两者之间的区别是必要的,这导致了所谓的非交织或真正并发模型的发展,如Petri网[32],事件结构[30],异步转换系统[4,35]等;参见[40]的调查。一个最流行的概念等效的非交错系统是历史保留双相似性(或简称HP-双相似性 它 由 Degano , De Nicola 和 Montanari 在 [ 6 ] 中 独 立 引 入 , Rabinovich 和Trakhtenbrot [34],然后由van Glabbeek和Goltz在[ 39 ]中为事件结构引入,Best等人为Petri网引入。 在[5]中。它受欢迎的一个原因是它是一个1571-0661 © 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。http://dx.doi.org/10.1016/j.entcs.2013.09.012166联合Fauberberg,A.Legay/Electronic Notes in Theoretical Computer Science 298(2013)165在动作精炼下的同余[5,39],另一个是它的良好的可判定性:它已被证明是可判定的安全Petri网由Montanari和Pistore [29]。作为对比,它的表亲遗传hp-双相似性在[ 24 ]中由Jur d zin ′ ski,Nielsen和Srba证明对于1-安全Petrinets是不可判定的。高维自动机(Higher-dimensional automata,HDA)是另一种非交错形式,用于推理并发系统的行为。由Pratt [33]和van Glabbeek [37]在1991年引入,目的是对并发理论进行几何解释,此后van Glabbeek [38]表明HDA提供了对“文献中提出的主要并发模型”[ 38 ]的推广(直到hp-双相似性)因此,HDA是一个有用的工具,比较和相关的不同的模型,也作为一个建模形式主义本身。HDA是几何的,因为它们非常类似于代数拓扑中使用的单纯复形,对HDA的研究已经从几何和代数拓扑中吸取了很多工具和方法,如同伦[11,14],同调[15,20]和模型类别[16,17],也可以参见调查[18]。在本文中,我们使用Joyal,Nielsen和Winskel在[23]中介绍的开放映射方法以及第一作者以前的论文[7]中的结果,对HDA的hp-双相似性给出了几何解释。使用这种解释,我们表明,HP-双相似HDA有一个表征直接在(高维)的HDA过渡,而不是在运行方面,例如。Petri网[13]我们的结果意味着有限HDA的hp-双相似性的可判定性他们还将hp-双相似性牢固地置于[23]的开映射框架中,并加强了双相似性和弱拓扑纤维化之间的联系[3,25]。由于篇幅所限,我们不得不在本文中省略所有的证明。它们可以在长版本中找到[9]。2高维自动机HDA作为并发行为的一种形式化描述,具有能够表示并发系统中事件间所有高阶依赖关系的特性。与转换系统一样,它们由状态和转换组成,这些状态和转换被标记为事件。现在,如果从一个状态的两个跃迁,例如标签为a和b,是独立的,那么这可以用标签为ab的二维跃迁的存在来表示。图1显示了两个例子;在左边,转换a和b是独立的,在右边,它们只能以任何顺序执行。 因此,对于HDA,正如实际上对于任何采用所谓的真正并发范式的形式主义一样,代数定律|b = a.b + b. a不成立;并发与交织不同。上述考虑同样可以应用于多于两个事件的集合:如果三个事件a、b、c是独立的,则这使用标记为abc的三维过渡来表示。因此,这不同于相互成对独立性(由转换ab,ac,bc表示),这是一个无法区分的区别联合Fauberberg,A.Legay/Electronic Notes in Theoretical Computer Science 298(2013)165167|Xδ1xδ2XKKKK11KK一BABB一一BB一Fig. 1.CCS表达式ab(左)和a.b+b. a(右)的HDA。 在左边的HDA中,正方形被填满通过标记为ab的二维过渡,表示事件a和b的独立性。 在右边,a和b不是独立的。在形式主义中,例如异步转换系统[4,35]或具有独立性的转换系统[40],它们只考虑二元独立关系。一个未标记的HDA本质上是一个点预三次集,定义如下。对于标记的HDA,我们可以传递到箭头类别;这是我们将在第6节中做的。在那之前,我们集中精力在未标记的情况下。一个准三次集是一个分次集X={Xn}n∈与映射δ ν一 起 :X n→X n−1,k∈ {1,.,n},ν∈ {0,1},满足准三次恒等式δν δμ=δμ δν(k