偏序约简与建设的几何方法：并发程序验证方法比较

可在www.sciencedirect.com在线获取理论计算机科学电子笔记298（2013）179-195www.elsevier.com/locate/entcs偏序约简Eric Goubault Tobias Heindel Samuel MimramCEA，列表法国伊夫河畔吉夫摘要并发程序满足给定的属性，如无死锁，在计算上是困难的。朴素探索技术正面临着状态空间爆炸问题：它们考虑并行线程交错的指数数量（相对于程序大小）。偏序约简是解决这一问题的标准方法。它基于这样的观察：某些指令集（称为持久集）不受其他并发指令的约束，因此在搜索死锁时总是首先进行探索。最近的并发进程模型使用有向拓扑空间：状态是点，计算是路径，等价的交织是同伦的。这种几何方法应用代数拓扑的理论结果来改进验证。尽管非常不同的起源的方法，本文比较了偏序约简与建设的几何方法，未来组件的类别。主要的结果，这表明，这两种技术本质上是相同的使用持久转换，是基本的兴趣和目标的交叉施肥的两种方法，以改善并发程序的验证方法并行程序是一个计算上困难的任务，因为人们必须检查所需的安全属性是有效的任何可能的调度程序，通常，并行的数量是指数的大小的程序。例如，考虑下面的并发程序，由两个并行进程组成，每个进程修改两个存储单元的内容x：=1;y：=2 |y：=3;z：=4（1）在下文中，我们假设执行模型是顺序一致的，使得程序（1）的执行将交错两个进程的指令，并且因此对应于以下六个顺序程序之一。（二）为了验证程序（1）是正确的，因此可以对六个程序（2）使用传统的验证技术，这也可以被描绘为1作者感谢PANDA ANR-09-BLAN-0169项目的支持。1571-0661 © 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。http://dx.doi.org/10.1016/j.entcs.2013.09.013x：=1;y：=2;y：=3;z：=4x：=1;y：=3;y：=2;z：=4x：=1;y：=3;z：=4;y：=2y：=3;x：=1;y：=2;z：=4y：=3;x：=1;z：=4;y：=2y：=3;z：=4;x：=1;y：=2180E. Goubault等人理论计算机科学电子笔记298（2013）179x：=1x02x：=1X12y：=2X22z：=4x01y：=3x00x：=1z：=4X11y：=3X10y：=2y：=2z：=4X21y：=3X20z：=4y：=3x：=1y：=2图1.一、的异步变迁语义和几何模型（1）.图1左侧的从x00到x22的路径。然而，这种方法不会扩大规模，因为对应于并发程序的顺序程序的数量增长非常快：这种现象被称为状态空间爆炸。为了避免它，已经发明了利用指令之间的固有依赖性的状态空间缩减技术。例如，x：=1和y：=3的执行顺序与大多数程序属性无关：这两种可能的执行最终会导致相同的内存状态。 我们使用瓷砖（标记为），以指示何时可以以这种方式切换指令，并表示指令可交换。形式上，图与瓦片形成一个异步转换系统或简称为ATS[19]。注意，在这个程序中，指令x：=1是持久的，因为它与所有可能的并行指令交换（形成第二个进程）。在不失一般性的情况下，我们可以假设它首先被执行，并且我们被留下来验证程序x：=1;（y：=2| y：=3;z：=4）是有效的。这个程序只产生了三种可能的执行，而（2）中有六种：我们可以避免检查通过状态x01和x02的路径。当然，我们可以迭代地使用这个过程来进一步减少程序，这导致删除通过状态x12的路径。这个过程由Valmari引入并由Godefroid [7]开发，称为偏序约简（POR），并导致了各种成功的工具，如SPIN [14]（其中上述持久集与其他技术互补，如睡眠集）。这些工具最初是为了优化死锁检测而设计的（后来以各种方式进行了扩展因此，我们将专注于死锁检测，尽管预期的应用范围更广（完全可达性将在未来的工作中详细介绍）;此外，我们将主要关注非循环系统，这也是偏序约简技术中的常见限制（例如，参见[6]）。独立于POR的进步，并发程序的拓扑语义的工作已经导致了基于类似观察的新技术，但在不同的上下文中制定[8，9]。在这条研究路线中，并发程序被建模为有向拓扑空间[4]。例如，在图1的右边，我们看到与程序（1）相关联的空间：忽略此时的弯曲路径，空间本质上是一个填充的正方形，带有一个方孔（以灰色呈现）。注意空间和左边的异步转移系统之间的强烈相似性：在某种精确的意义上，拓扑模型实际上是ATS的几何对应物（即，它的几何实现）：一种设置中的构造可以在另一种设置中重新表述;避免关于拓扑的形式细节，我们诉诸几何直觉来说明主要思想。E. Goubault等人理论计算机科学电子笔记298（2013）179181在几何方法中，程序执行被建模为空间中的路径，如图1所示。例如，通过洞下面的路径对应于（2）中的第一种可能的调度。请注意，当投影到坐标时，路径应该始终是单调的;这捕获了程序每个线程的时间进度。这就是为什么模型的拓扑空间需要赋予方向的概念[13]。在这些拓扑模型中，通过反复切换交换指令可以从彼此获得的两个交织被表示为双同伦路径，即可以连续变形为彼此的路径。 例如，在图1的右侧，在洞的顶部是异同伦的，但没有一个是异同伦的下面通过的一个;原因是，洞是一个障碍，连续变形的路径下方和上方的洞。根据拓扑空间定义程序语义的兴趣在于，它允许重用来自代数拓扑的概念和工具。这使得状态空间缩减方法的公式化成为可能，如下所示。从并发的角度来看，如果路径不改变可能的未来路径，直到同伦，则路径是不必要的：这样的路径对应于程序没有做出重要选择（例如选择条件选择的分支）或调度器（例如命令两个不交换的并发动作）的执行使用适当的形式化，人们自然会考虑程序的拓扑语义中的路径范畴，这些路径被非本质路径所取代，以便只保留与研究程序直到指令交换相关的结构在[11]中引入的这个类别被称为未来组件类别，并在工具ALCOOL [4，9]中使用，该工具已成功用于工业环境[2]中的死锁检测。尽管持久集和非本质路径的概念之间有惊人的相似之处，但两者之间的关系从未被正式研究过，本文的目的就是填补这一空白，以使偏序约简和几何技术相互改进，并结合它们的潜力来缓解状态空间爆炸问题。因此，我们能够证明，在相当合理的假设下，持久转换是非本质路径的代数对应物。尽管这种类比是直观的，但事实证明，理论上的比较有时涉及技术问题。在更实际的方面，在[4]中开始了基于实验的初步比较。在第一节中，我们首先回顾了这里用来形式化持久集的计算模型：具有独立性的标记变迁系统（LTSI），它被推广到异步变迁系统（ATS）。在第2节中，我们保守地将持久集的原始定义从LTSI扩展到ATS，这更接近于几何模型，并表明它们保留了其基本的约简潜力，以修剪死锁检测的搜索空间。 最后，我们开发在第3节中，我们给出了偏序约化和有向代数拓扑之间的第一个概念性联系;在定理3.10中，我们精确地给出了在什么意义上持久的问题。182E. Goubault等人理论计算机科学电子笔记298（2013）179单例本质上与非本质态射相同，因此确定了几何和偏序约简方法的共同概念（在两种方法中使用的大量技术和几何学中）。我们将在第4节的总结中进一步讨论这一点，以及未来研究的地点。1并发计算我们将使用两种模型进行并发计算：具有独立性的标记变迁系统（LTSI），如传统上在POR技术中使用的，以及异步变迁系统（ATS），它可以被看作是几何观点的有向拓扑空间的代数对应物这两种方法都形式化了程序的状态空间，如图1所示。1.1具有独立性的一个标记的转移系统（LTS）是一个三元组（S，Λ，→），其中S是一组状态，Λ是一个变换标号集，并且→ ΛS×Λ×S是一个变换标号。Wewrites−→tsJ当ver（s，t，SJ）∈ →和s−→t当t∈Λi时s使d在s中成立，即当存在一个状态sJsu ch，即s−→tsJ。这里我们只考虑确定性跃迁系统即 s−→tsJ和s−→tsJJ意味着sJ=sJ J。如果相对顺序为他们在哪里执行并不重要，在这个意义上说，这两个祝福基本上是相同的计算，特别是产生相同的结果。这种独立性的概念激发了以下定义[7]。定义1.1（独立性）具有独立性的标记转移系统（LTSI）由具有独立关系的LTS（S，Λ，→）组成，独立关系是对称的、不相关的关系<$$> Λ× Λ，使得对于每个对（t1，t2）∈ <$，每个可达状态s，(i) 如果s-t→1 sJ，则sJ−t→2is−t→2;and(ii) 如果boths−t→1s→t→2hold，re存在唯一的sJ J，使得（对于唯一的pairofstates1，s2∈S）boths−t→1s1−t→2sJJ和s−t→2s2−t→1SJJ保持。1.2异步转移系统并发的几何模型已经被引入，其思想是将代数拓扑中开发的工具应用于并发程序的分析[8];这些程序被认为是有向拓扑空间，其中（有向）路径对应于程序的特定执行，并且路径之间的双同伦是执行的等价物（导致相同结果的并发程序的相关双同伦）。对于并发系统的分析，拓扑形式化可以用它的代数对应物，即异步转移系统（或更一般的预三次集）来代替，这使我们更接近LTSI的形式化，正如我们在这里回忆的那样，参见[12]以获得它们之间的详细比较E. Goubault等人理论计算机科学电子笔记298（2013）179183模型回想一下，图G=（V，E，src， tgt）由顶点集V、边集E和两个函数src， tgt：E→V组成，这两个函数分别将每条边与其源和目标相关联从顶点x到顶点y的路径u，记为u：x→y，是一个连续边的序列;顶点x上的空路径记为εx：x→x。两条路径u：x→y和v：y→z的连接表示为u·v：x→z。定义1.2（异步变迁系统）异步变迁系统，或简称ATS，是一个对（G，n），其中G是一个图（其顶点称为位置，边称为变迁），n是具有相同源和目标的长度为2的路径集合上的关系，即（u，v）∈ n，仅当u，v：x→y。 图中的元素称为瓦片。 两个跃迁m：x→y和n：x→z是独立的，记为m<$n，如果存在跃迁m J和n J使得（m·n J）<$（n·m J），即 我们在右下方有如 （3）中的瓦片。为了形式化我们可以在并发系统的运行中重新调度独立事件而不改变实际执行的计算，我们使用以下迹的定义，它细化了Mazurkiewiczm·n′··n·m′（三）定义1.3（迹）两条路u，v：x→y是同伦的，记为u∈v，如果u可以从v中通过用mj · n来重新置换路径fm ·nJ得到e d，只要存在一个瓦片（3），即关系f是w. r. t的最小同余。路径组合，扩展了路径。迹是一个等价类w.r.t. 我们把它写成[u]，作为路径u的等价类。定义1.4（迹范畴）与一个ATS（G，n）相关联的迹范畴具有G的顶点作为对象和迹[u]，其中u：x→y作为来自x到y复合是路径连接在迹上引起的运算，恒等式是空迹[ε x]。为了将这个模型与上一节介绍的模型联系起来，我们应该注意到，每个LTSI（定义1.1）都自然地诱导出一个ATS，如下所示。定义1.5（诱导ATS）设（S，S）为LTSI其中S=（S，Λ，→）。其诱导的ATS，表示为ATS∈S=（G，G），以顶点为位置，以边缘为过渡，即V=S和E=→;此外，对于每个（s，t1，s1）S（s，t，s）s1（s1，t′2，s′）SJ（s，t′，s′）e=（s，t，sJ）∈E，我们有src（e）=s， tgt（e）=sJ，并且当t1>t2时，2 2s221s→t→1 则s-t→2。例1.6考虑下图左边的LTSI，其中，k={（a，c），（c，a）};其关联的ATS显示在中间。注意，没有一个LTSI可以生成右边的ATS，因为要生成它的转换，我们必须生成引理2.11中所述的从这个意义上说，ATS比LTSI更通用。184E. Goubault等人理论计算机科学电子笔记298（2013）179C⬦t1t2−−−→tn3a BC caB可以很容易地定义ATS的标记变体，并且本文中在ATS上执行的所有构造都可以推广到标记情况（参见[12]这些模型之间的精确关系）。然而，转换的标签并不是真正需要的，因为转换标签的合适概念可以抽象地恢复为其相关联的事件：定义1.7（事件）设（G，）是一个ATS。 两个变迁m和m J是平行的，记为m Q m J，如果它们形成某个瓦片（3）的相对侧，即如果对于某些变迁n和n j存在瓦片（m·nJ，n·m J）∈ n。事件是一个等价类。包含Q的变迁上的最小等价关系。例如，在例1.6的中间ATS中，左边的两个垂直转换是同一事件的元素，而最右边的不是：考虑左边的LTSI，因为b和c不是独立的，在b之前或之后执行c并不对应于同一事件备注1.8在后续的文章中，我们将限制那些有独特的方式来“关闭”方块的AT形式上，前者意味着（m·p）<$（n·q）和（m·pJ）<$（n·qJ）意味着p=pJ和q=qJ，而后者意味着u<$v和u<$w意味着v=w。所有由LTSI引起的AT都满足这个性质。2异步迁移系统持久集是最著名的减少的执行，以检查并发程序不会导致死锁状态。在这里，我们将它们的定义推广到ATS，以将其与第3节中的几何约简技术进行比较。我们首先回顾Godefroid定义2.1（持久集）给定一个LTSI（S，Λ，→，λ）和一个状态s∈S，在一个状态s ∈ S中使能的转移标签的集合R <$Λ在s中是持久的，如果 对于所有非空转移序列s=s1−→ s2−→ S...tn−1n−→sn+1对于满足ti∈/R（1 ≤i≤n）的条件，对每一个变换t∈R成立。只要可以将单个转换拉回，就可以将其视为持久转换通过用独立的（不一定是持久的）转换来排列它，将其转换到它首次启用时的状态。更一般地说，持久集通常包括某个并发组件的条件选择的操作，如以下示例所示。E. Goubault等人理论计算机科学电子笔记298（2013）179185的t00tn1n1n−→例2.2考虑下面的程序及其各自的 LTSI语义。y：=2·x：=1if（z 0）x：=1|y：=2y：=2·x：=1x：=1|y：=2··其他··（4）x：=1·y：=2y：=3x：=1y：=2y：=3·在左边的LTSI中，x：=1和y：=2完全并行运行;因此，{x：=1}和{y：=2}在初始状态下都是持久集。相比之下，在右边的系统中，转换x：=1和y：=2与y：=3是一致的;唯一的持久集由一个没有线程并发运行的“单片”组件组成{x：=1，y：=2，y：=3}是初始状态下唯一的持久集作为最后一个例子，在图1中，{x：=1}和{x：=1，y：=3}在初始状态下是持久的，而集合{y：=3}不是。回想一下，死锁是一种不启用转换的状态。如前所述，持久集的主要目的是缩小并发程序中死锁的搜索范围：给定每个状态的持久集选择，可达死锁总是可以通过仅包含所选持久集中的转换的路径到达;因此，探索系统“沿着”持久集是足够的命题2.3（持久死锁可达性[7，定理4.3]）给定一个非空持久集Rs在每个状态s上的选择，该状态s不是死锁，对于每个路径s−→是.. . S−→ % d到死锁% d，则存在路径% st′0 sJ...SJ屯德使得t Ji∈R si 对于所有i∈ {0，.， n}。上述命题的证明基于以下观察：对于每个导致死锁d和在s处的持久集R的路径u：s→d，存在路径v∈[u]（即v<$u），其初始转移在R中。这促使我们基于以下定义来推广持久集的定义定义2.4设（G，G）是一个ATS。给定一条路径u：x→z，一个变迁m：x→y是初始模同伦，如果存在一条路径v：y→z，使得u∈m·v;u中的初始模同伦的所有变迁的集合记为m（u）. 具有公共源x的两条路径u：x→y和v：x→z是相容的，记为u↑v，如果存在具有共同目标x j的路径w y：y→x J和w z：z→x J，使得u·wyv·w z.因此，特别地，在某些路径中是初始模同伦的所有转换是成对相容的。这些概念使我们能够将持久性推广到ATS，如下所示：定义2.5（同伦持久集）设R是一个ATS（G，G）中的一组变迁，它们共享一个状态x作为公共源。 集合R是同伦持久的，如果每个路径u：x→z与R中的所有变迁相容，前提是R中没有变迁是它的同伦初始变迁，即。当x→z时，R<$u（u）=<$m∈R。 u↑m。0−→·186E. Goubault等人理论计算机科学电子笔记298（2013）179Y'Jz<$注释2.6持久的单例（具有单个元素的持久集合）对应于与具有相同源的所有路径兼容的转换例2.7单例{o→y}是下面（5）中的ats中的同伦持久集。注意，转换o→y与转换o→x兼容，即使这两个转换不是这种情况通常出现在消费者保护中-zyJ在使用n元信号量的情况下，确保耗尽的资源不被使用，例如如当实现具有有限大小的队列时。对于xJoJ例如，假设我们有一个队列，最多可以放入两个元素（如果已经有两个x元素时，放置操作会阻塞，直到元素从队列中取出o'Jx'x′J（五）下面的程序生成了上面的ATS（箭头下标表示相应转换的方向）。放↑|如果（.）（tak e）|put t→}else{takes|Putt←}现在还需要证明同伦持续集的概念实际上是原概念的保守扩展（定义2.1）。该证明基于以下观察：在由LTSI引起的每个AT中，转变m：x→y在兼容路径u：x→z之后具有唯一的剩余路径u/m：y→z;我们说这种ATS有兼容的残差。一旦执行了m，则u之后m的残差u/m直观地具有备注1.8中的假设对于以下定义的合理性是必要的。定义2.8（残差）设m：x → y是一个过渡，u：x → z是一条路径，m之后的u的残差，记为u/m，以及m之后的m的残差，记为m/u，通过对u的长度的归纳定义如下。• εx/m=εy和m/εx=m• （m·uJ）/m=uJ和m/（m·uJ）=ε• 如果nj=m，（n·u）/m=nJ·（u/mJ），其中mJ和nJ是跃迁，使得m·n J<$n·m J如（3）所示（其中m J由备注1.8唯一确定）。一年二年u/my3 · · ·yk−1ykε ykyk+1· · ·yl−1v/mylm m/uε m/vx1x 2x3· ··xk−1uxkykM/uyk+1· · ·yl−1ylv注2.9路径u之后的变迁m的残差m/u（当它存在时）要么是变迁要么是空的（如上所述）。将定义扩展到路径u：x→y之后路径v：x→z的残差v/u是很简单的。OyE. Goubault等人理论计算机科学电子笔记298（2013）179187/由LTSI引起的每个AT具有相容残差的事实可以从它们满足特定DI的事实推导出来。n′XJqoJXRzJm′n′yJxJp 布吕普yxzJm′yJzqy[2017 - 10 - 17][2017 - 10 -17][2017- 10][2017 - 10][2017 - 10- 17]莫恩莫恩（六）定义2.10（Forward Cube Property）如果对于（6）中左侧所示的每三个图块，存在（6）中右侧所示的三个匹配图块，则ATS具有前向立方体属性（或fcp）。引理2.11LTSI的诱导ATS具有FCP性质。我们对该物业的主要兴趣是以下物业[16]：命题2.12（残差）具有FCP的ATS具有相容残差。这个命题是主要的工具来表明，实际上我们对持久集的定义是对原来定义的保守扩展：命题2.13（同伦持久是持久的）设（S，Λ，→，λ）是一个LTSI，设x是位置，并且设R是全部被启用的转变的集合在X。 集合R在x处不变当且仅当集合RJ={（x，t，y）|t∈R，x−→ty}在TS空间中同伦在x处不变。证据 如果R是持久的，很容易证明RJ是同伦持久的，因为如果R中的一个变迁标签独立于路径上的所有变迁标签，特别是与相应的跃迁（定义2.8）相容相反，存在RJ是同态py的条件。因为根据引理2.11，一个TS∈S具有FCP，对于每条路径u：x → z，我们可以使用命题2.12来证明，要么R中的一个跃迁的某些残差在u中发生（如果f∈（u））， RJ=），或wehav eRJ中u之后的所有跃迁的残差（如果u与RJ中的所有跃迁相容）。可以很容易地检查到，RJ中的任何跃迁的残差总是带有与R j中的“原始”相同的标签Q有了这个结果，我们从现在开始就把ATS引理2.14设G =（G，G）是一个ATS，u：x→d是一条路，使得d是一个死锁，R是x上的非空持久集。然后R包含u的一些初始转换（即， u <$m·v（对于 某个m∈ R和一条合适的路v）.证据假设路径u：x→d导致死锁d。假设u与R中的所有变迁相容。因为R是非空的，所以在R中存在一些变迁m：x→y和路径uJ：d→z和v：y→z，使得u·uJ<$m·v。由于d被假定为死锁，我们必然有uJ=εd和z=d。188E. Goubault等人理论计算机科学电子笔记298（2013）179[v′]y[u]因此，um·v，即 m∈φ（u），并得出结论. 否则，u与R的某个跃迁m：x→y不相容。 如果R是同素的，则R≠0（u）/=0。Q推论2.15（持久死锁可达性）设（G，G）是一个以V和E分别为顶点和边集的ats，设R：V→G（E）是一个函数，使得对于所有非死锁状态x∈ V，集合Rx在x处是一个非空持久集。给定一个死锁d∈V可由路径u：x0→d到达，存在一条路径v：x0→d使得u≠v，并且在v中发生的每个变迁m：x→y在x处是持久的，即m∈ Rx。请注意，对于任意的安全属性，持久集本身并不存在，必须使用类似于[7]的睡眠集的额外技术最后，以下技术引理将在以下方面有用引理2.16在与满足fcp的ats相关联的迹范畴中，每个态射都是epi，也就是说，对于每个路径u：x→y和v，w：y→z，[u·v] = [u·w]蕴涵[v] =[w]。3比较POR和未来组件在本节中，我们将持久集的概念与未来组件的类别[10]，它通过消除只允许“不必要的”转换的状态，给出了并发程序（的几何模型）的压缩表示。我们首先在ATS的背景下重新表述这个构造以及相关的性质：我们引入未来相关迹的概念，然后将未来分量的范畴定义为迹的范畴与一组一致的未来相关迹的商。 在那之后，是精确地确定哪些过渡被认为是不必要的。直觉上，人们可能认为所有持久转换都是不必要的。然而，ATS的一般定义允许在通常程序生成的ATS然而，我们将证明，对于适当的对非本质转换的第一个要求是，它们不影响任何可能导致死锁的选择直觉上，在执行一个不重要的过渡之前和之后，未来可用的选择应该是相同的：它们应该在以下意义上反映未来。定义3.1（未来相关迹）迹[u]：x → y是未来相关的，如果对于从y可到达的每个位置z（即存在路径y→z），与[ u ]的预合成导致从y到z的 迹 和从x到z的迹之间的双射。zXy[u]x[u]yz z[v]~xE. Goubault等人理论计算机科学电子笔记298（2013）179189例3.2（反映未来的过渡）重新考虑图1中的ATS。调度转换的唯一重要选择涉及指令y：=3和y：=2的相对顺序。也就是说，x00→x10（标签x：=1）的转换并不影响选择，因此直观上是事实上，它根据定义反映了所有的未来。例如，从x10到x22的两条迹通过x00→x10唯一地因子化。相比之下，转换x10→x20（带有标签y：=2）不反映未来，因为从x20到x22只有一条迹线，而从x10到x22有两条迹线。换句话说，如果一个轨迹是面向未来的，那么未来的所有选择都已经在它们的源头出现了。面向未来的过渡概念与持久过渡概念接近;然而，这两者通常并不一致，如以下示例所示例3.3考虑右边的立方体。所有的跃迁对都是独立的，除了o→oJ和o → y（立方体的正面不是瓷砖）。现在两转换O→Y和O→OJ是持久的，因为它们与从O开始的所有其它转换兼容。然而它们都不是未来可追溯的痕迹。看到o →y不是一个未来相关的迹线，考虑迹线zJxJyJoJzXyO[y→yJ]。从y到YJ只有一条迹线，但从o到yj有两条迹线。o→oJ的论证是对称的。在这个例子中需要注意的重要一点是，关联的迹类别不是偏序集（它可能有多个态射两个物体之间事实上，可以证明，当迹范畴是偏序集时（这是事件结构的情况），所有持久转换都是面向未来的。在右边的ATS中，o→y的转变是持续的。奥伊然而，它不是一个未来的反思轨迹，因为轨迹[o→x]不通过[o→y]分解。 还请注意，ATS实际上是由LTSI引起的。xJx z在未来组件范畴中使用的状态空间缩减的基本思想因此不需要显式地表示。因此，从一个ATS开始，人们可能会考虑相关的迹类别（定义1.4），并将其与所有未来相关的迹进行商，这相当于将它们形式转化为身份 事实证明，这压碎了太多关于迹的信息（参见[5]，特别是商和分数范畴之间没有等价性，并且通过Van Kampen定理没有组合性结果）。一个合适的解决方案是对所有未来反射迹的子集进行商，即那些在合成和“残差”下闭合的迹定义3.4（非本质系统）设（G，G）是一个ATS，设G是一组迹。集 合 f是一个无 要 素 系统（System of Inessentials），如果(i) 每个元素都是一个未来反射迹;(ii) Bclf包含所有空迹，并且在复合下是封闭的;190E. Goubault等人理论计算机科学电子笔记298（2013）179L(iii) 在推出条件下，BMF是稳定的，即 对于任何迹σ：x → z ∈ f，trace[u]：x→y，re存在推出z[u′]xJσ′y/z←−σ[u]Xy使得σ J∈ ψf。−→←−−→我们记得范畴C中的两个态射f：A→B和g：A→C的推出是一对态射GJ：B→D和FJ：C→D，满足FJ<$g=gj<$f，更进一步，对于任何其他态射对h：B→DJ和k：C→DJ，满足k<$g=h<$f，存在唯一态射fBg′Af′GCHDDJKl：D→DJ满足bothk=lf J和h=lgJ（如图ht所示）。定义3.5（非本质迹）一个迹是非本质的，如果它属于一个ats的所有非本质系统的并集（这是一个非空的ATS，它是最大wrt包含）。事实上，在下面的大多数例子中，沿着另一条不重要的迹线推出的只是它的残差。下面的例子表明，未来反射转换的集合不需要在残差下闭合，因此最大残差不包含所有未来反射迹。例3.6考虑右侧的ATS，其中所有面zJ但背面是瓷砖 o → o J的 跃 迁 是未来-xJy J的反射。它在o → x之后的残差，即x→x J，不是future-o Jz反射的（甚至不是持久的）。实际上，最大的Nxy是{oJ→xJ，oJ→yJ，y→z，y→yJ}通过残差、o复合和恒等式的闭包。请注意，此示例的ATS然而，未来组成部分的类别已明确界定。定义3.7（未来成分的一个ATS的未来成分的范畴是它的迹范畴，由不重要的迹来表示这种构造等于把不重要的过渡当作同一性而忘记了它们。另一种观点，由下面的命题形式化，是这种构造去除了使不必要的转换的状态：非正式地，通过它们不会带来任何关于可能的未来跟踪的新信息（因为程序或调度程序不能做出重要的选择）。这与图1中介绍性示例的非正式解释一致;状态空间缩减删除了状态x01、x02和x12。命题3.8设（G，G）是一个ATS，令G是最大的K。如果不可能，那么未来成分的范畴就是迹的范畴的全部子范畴，它是由不允许不可能中的任何跃迁的所有状态所诱导的。最后，我们给出了未来成分范畴产生期望状态空间的充分条件。最后一个条件是没有d'eja`vu s（参见）。实施例3.3）。定义3.9（D′ej`avu）d′e j`avu是一个变换m：x→y，使得re存在一条路径u：yJ→x和u中的一个变换mJ：xJ→yJ，它是与E. Goubault等人理论计算机科学电子笔记298（2013）179191M. 如果它的转换都不是d'ej` a v u s，则它是d'ej`avur ee。在其他的词中，一个ATS是d'eja`vufree的，如果它的路径中没有一个包含两个是同一事件的实例的转换。例 如，在例3.3的第二个AT中，跃迁x→z是一个d'eja`vu，因为路径o→xJ→x→z包含了同一事件的两个同时发生：（x→z）Q（o→y）Q（x→x J）。类似地，任何循环的ATS都有d'ej`avus，尽管d'ej`avus不一定是e循环。 有了这个最终 的过程，我们得到了非本质和持久转移之间的形式对应（即转移m：x→y，使得{m}是x处的持久集）。定理3.10（不存在性vs. 在任何具有前向立方体性质的d'eja`vufreATS中，转移是持久的，只要它属于某个立方体（特别是最大的一个）。如果ATS的跟踪类别是有限的，则未来组件的类别是包含所有不启用持久转换的对象的完整子类别。证据 假设n∈f是一个N，m∈ n∈f是一个跃迁。我们想展示{m}是一个持久集。对于任何与m共初始的路径，我们有m沿u的推出，因为n ∈f在推出下是封闭的。因此，m↑u和m根据注2.6是持久的。相反，设fj是仅由持久转换组成的迹的集合。它表面上表明，阿吉是一个阿吉。 为了证明在推出时，m1···mk∈φJ，设u是与m1共初始的路.我们使用FCP、注释2.6和命题2.12连续地取mi沿u的残差，并验证残差的合成是推出的。接下来，我们证明了持续的过渡是未来的。设m：x→y是一个持续的转换，z是从y可到达的状态。因为假设ATS具有FCP，所以根据引理2.16，变迁m是满态迹，即对于每个路径u和v，使得[m·u] = [m·v]，我们有[u] = [v]。也就是说，在这种情况下，我们有u=（m·u）/m<$（m·v）/m=v，中间同伦被证明为m·u<$m·v和剩余与同伦相容。因此，带有从y到z的迹的m的预合成是单射的，它仍然要表明它是满射的。给定一条路径u：x→z，我们必须证明u通过m因式分解。 根据注释2.6，变迁m与u相容，因此我们可以沿着[u]推出[m]，这只是m在u之后的残差;它必须是我们可以以其他方式获得ad'eja`vu的恒等式，事实上，[u]因子为[m]·[uJ]，其中[uJ]是[u]沿着[m]的推出。Q因此，在一个大类的公共系统中，包括那些由事件结构或具有非循环因果关系的Petri网生成的系统，持久单例实际上与非本质态射相同。 因此，尽管几何方法和POR技术的起源之间存在巨大差距，但在一大类系统中，我们确实不仅有192E. Goubault等人理论计算机科学电子笔记298（2013）1794结论我们已经开发了一个持续集到异步转移系统的保守扩展（定义2.5），它与LTSI的原始概念（命题2.13）相一致。这种扩展形式的基础上，我们的比较的部分订单减少技术和几何方法的状态空间减少，因为ATS是几何模型的代数对应。特别地，我们已经证明，我们的定义保留了持久集的主要应用，包括修剪对死锁的搜索（推论2.15）。这些概念对于我们的主要贡献至关重要，它证明了未来分量范畴的理论构造的实际相关性，并进一步证明了[10]中的结果，其中对一般有向拓扑空间进行了状态空间约简定理3.10掩盖了细节，它说不必要的转换与持久单例是一样的作为一个直接的结果，当我们只使用持久单例时，未来组件类别的构造大致相当于POR技术的应用。因此，我们发现了几何方法和POR技术的共同核心，而这两种方法都有额外的算法和方法来提高性能。几何方法[4]有很好的例子，这激发了未来的研究。在理论上，持久单例和非本质跃迁之间的完全一般对应是不可能的（如例3.3所示），考虑到起源的不同，这并不奇怪。为了衡量每种方法在实践中的优势，需要对POR我们进一步计划使用Petri网[3，15]中的方法和工具这是因为Petri网更接近于几何方法和por技术，正如Petri网中所谓的顽固集[ 18 ]的研究所证明的那样，这是持久集的一个Petri网启发技术的添加是基于以下观察：未来组件的类别与发生网的刻面抽象具有相似性[1]，并且[4]中几何方法的最新进展使用了“弱因果关系”的概念最后，我们期望得到具有代表性的实验结果，这将补充本文的理论结果。引用[1] S. Balaguer，T. Chatain和S.哈尔从揭示关系中构建紧密的发生网。《儿童生存与发展加速方案》，第44-53页。IEEE，2011年。[2] R. Bonichon和Al。工业控制软件中并发故障自由的严格证据计算机安全性、可靠性和安全性，第85-98页[3] J. - M. Couvreur，D. Poitrenaud，and P. Weil.一般petri网的分支过程。在应用和理论的Petri网，卷6709的LNCS，第129施普林格，2011年。[4] L. Fajstrup，E. Goubault，E.奥库尔，S. Mimram和M.劳森迹空间：一种有效的状态空间约简新技术。见ESOP，第274E. Goubault等人理论计算机科学电子笔记298（2013）179193- 是的 此外，我们有箭头σ→Q（B）=Q（B）[5] L. Fajstrup，E.Goubault，E.Haucourt和M.劳森基本范畴的组成部分Applied Categorical Structures，12（1）：81[6] C. Flanagan和P.Godefroid。模型检测软件的动态偏序约简在POPL[7] P. Godefroid。Partial-Order Methods for the Verification of Concurrent Systems：An Approach to theState-Explosion Problem，计算机科学第1032卷。Springer，1996年。[8] E.古博几何与并发：用户指南。Mathematical Structures in Computer Science，10（4）：411[9] E. Goubault和E.奥库尔几何语义在并发程序静态分析中的实际应用。 在proc 的CONCUR'05，LNCS的第3653卷，第503-517页。Springer，2005.[10] E. Goubault和E.奥库尔第二类基本要素。Applied Categorical Structures，15（4）：387[11] E. Goubault，E. Haucourt和S.克里希南有向拓扑中的未来路径成分。在MFPS，ENTCS的第265卷，第325[12] E. Goubault和S.米姆拉姆并发的几何模型和经典模型之间的正式关系。ENTCS，2012年。[13] M.葛兰迪斯有向代数拓扑：不可逆世界的模型，新数学专著第13卷。剑桥大学出版社，2009年。[14] G. 霍尔茨曼模型旋转。 IEEE Trans. 软. Eng. ，23（5）：279[15] Khomenko和A.莫霍夫一种直接构造完全合并过程的算法。在应用和理论的Petri网，卷6709的LNCS，第89Springer Berlin，2011.[16] S. 米姆拉姆 S'emantiquedesjeuxdichr oneset r'e'ecritu re2-dimensionne lle. 博士论文，巴黎狄德罗大学，UFR d ' I n f o r m a t i q u e ， 2 0 0 8 年 。[17] R.桑色素并发自动机与异步系统。在MFCS，LNCS的第3618卷，第686-698页中。Springer，2005.[18] A.瓦尔马里简化状态空间生成的顽固集。 在应用和Petri网理论，第491-515页[19] G.温斯克Handbook of Logic in Computer Science，Volume 4：Semantic Modeling，chapter 1：Models for concurrency.牛津大学出版社，1995年。A.未来组成部分类别的特征证据 设D <$C是极大满子范畴，使得对所有σ：A → B ∈ C，若A∈D则σ =idA.现在我们定义一个“商”函子Q的候选： 为每个对象A∈ C，考虑定义域为A的所有箭头。由于图是有限的，我们可以取相应图的上极限（使用连续的推出）来获得上极限对象Q（A）;此外，我们有一个