跨度（图）中的组合最小化

··理论计算机科学电子笔记104（2004）181-197www.elsevier.com/locate/entcs跨度（图）中的组合最小化：一些例子Piergiulio Katis1，2N.萨巴迪尼，1，3，R.F.C. Walters沃尔特斯1，4文凭Scienze CC. FF.MM.Universit`adel摘要我们研究了一类最小化自动机的例子，就分支互模拟的范围内的跨度（图）模型。 组合最小化对于包含经典餐饮哲学问题及其变体的类特别有效。其有效性的原因是类的有限子集生成互模拟幺半群的有限子幺半群。我们表明这可能是如何用于研究死锁。在用餐哲学家的情况下，关键的事实是，在互模拟幺半群中，（FP）3=（FP）2，其中F是叉子，P是叉子。哲学家关键词：模型检验，最小化，分支互模拟，自动机，幺半群，哲学家用餐1介绍自动机最小化的经典概念在[9]中被推广到Span（Graph）的合成设置，特别是关于分支互模拟。类似的最小化是组合模型检查的基础[2]，[10]，[12]），试图规避问题1该研究得到了意大利科莫因苏布里亚大学化学科学、数学和数学系以及意大利ProgettiCofinanziati MUIR：计算元模型（COMETA）的财政支持2电子邮件：piergiulio katis@hotmail.com3Email：nicoletta.sabad i n i@ un n i nsu br ia. 它4电子邮件：robert. uninsubria.it1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.08.025182P. Katis等/ Electronic Notes in Theoretical Computer Science 104（2004）181-197········· ····在穷举自动状态空间搜索中可能发生的状态指数增长。该方法已在实际的模型检验程序中得到应用。[4]）在各种问题上取得了成功，尽管该方法已被证明有其局限性（[3]）。这似乎是一个非常困难的数学问题，以确定类的问题，其中组合最小化减少状态空间从指数到多项式的大小。本文是对一类例子的研究，在这些例子中，该方法被证明是非常有效的。本文的一般代数情况在[9]中描述，但为了将注意力集中在最小化问题上并避免代数细节的过载，本文中我们只考虑两种类型的跨距：具有两个相等接口的跨距-左接口和右接口;以及没有接口的跨距。我们考虑给定初始状态的跨度，我们只考虑两个操作。如果X和Y有两个接口，我们将span复合的可达部分（通信并行产品）表示为X Y，它也是一个有两个接口的span;这个操作模拟了用Y的左接口识别X的右接口的构造（效果是隐藏它们现在共享的接口）。如果X有两个接口，我们也定义Fb（X），它是一个没有接口的跨度;将X的右接口反馈到其左接口的构造。 这些操作使我们能够对由一条线或一个环组成的问题进行建模，每个并行进程与其两个相邻进程进行通信。请注意，Span（Graph）[8]允许用类似电路的几何结构描述更一般的系统。在第2节中，我们简要回顾了我们对跨度模型的要求，以及我们将使用的双相似性概念-本质上我们引入了双模拟幺半群BisAut的概念，其元素是span模分支双模拟。第3节回顾了组合最小化的跨度方面分支互模拟-我们用min（X）表示X的最小化组合模型检查中的基本复杂性问题如下。 考虑一个无限序列X1，X2，. 的跨度，每个具有最大值的c状态和转换。 然后min（X1X2可以通过一系列初等最小化和合成来计算。min（X1X2Xn）的状态数和跃迁数明显受cn的限制。问题是哪些跨度序列可以用多项式来代替inC.本文的技术内容致力于提供无限多个具有此性质的跨度序列，包括经典的哲学家用餐问题及其变体。我们通过详细分析通过锁定和解锁进行通信的跨度在这些例子中考虑的跨度族实际上生成有限P. Katis等/ Electronic Notes in Theoretical Computer Science 104（2004）181-197183··−−submonoid的BisAut;从这个事实可以立即推断，最小化算法适用于这些家庭是线性的。在用餐哲学家的情况下，关键的事实是，三个叉子和哲学家在一排是双相似的两个哲学家和叉子在一排-根据互模拟幺半群，（FP）3=（FP）2. 这意味着一行（更多）比两个）交替的叉子和哲学家是bisimilar只有两个叉子和哲学家。虽然吃饭的哲学家是并行系统中研究最多的例子之一，但这一事实似乎以前没有被注意到。在最后一节中，我们描述了如何推导出关于死锁存在/不存在的各种结果。Pierantonio Redaelli、Mara Barbera和R.F.C. 沃尔特斯有助于获得论文的具体结果2模型2.1跨越自反图是一个有向图，其中可能存在平行边，并且对于每个顶点，都有一个开始和结束于该顶点的指定边，该顶点处的自反边我们将考虑自反图的特殊跨度，即自反图的边在有限集中有两个标号A.我们假设集合A有一个特殊的元素，我们将其标记为定义2.1具有两个相等界面A的图的跨度，或仅一个跨度，是元组（G，g0，l，r），其中：(i) G是有限自同构图。 它的顶点和边有时被称为作为跨度的状态和转换反对称边也称为空闲转换。(ii) g0是G的一个顶点，使得G的每个顶点都是从g0可达的，span的初始状态。(iii) l和r是函数l，r：Edge（G）→A使得如果α是自反边则l（α）= r（α）= −.对于G的每一个变迁α，我们分别称l（α）和r（α）为变迁的左标号和右标号.如果l（α）=然后我们假设转换e在左界面上是不可见的。如果r（α）=，那么我们说跃迁α在右界面是不可见的。一个没有接口的跨度就是一个对（G，g0），其中G是有限自反图，g0是使得G的每个顶点都是从g0可达的. 如果没有理由在混淆中，我们仅用G表示跨度（G，g0，l，r）或跨度（G，g0）。G的一个行为是图G中的一条路径（有限或无限），它从初始状态开始。184P. Katis等/ Electronic Notes in Theoretical Computer Science 104（2004）181-197-→−→例2.2我们在这里描述两个跨度，它们可以用来模拟用餐哲学家的例子。每个都有两个接口。当我们列出一个跨距的变迁时，我们不必麻烦列出自反边，一个变迁α：v→w记为l（α）/r（α）：v→w。对于本文中的这个例子和其他例子，我们假设A包含符号第一个跨度F模拟了一个叉子。它有三个状态0、1、2和以下转换：：0个1，u/：1个0、/升：02，/u：20的情况。状态0对应于叉未被使用，状态1对应于叉在左侧被使用或锁定，状态2对应于叉在右侧被使用。F的初始状态为0。第二个跨度P模拟了一个右撇子哲学家。它有四个状态0， 1， 2， 3和以下转换：−/l：0→ 1 l/−：1→ 2 −/u：2→ 3u/−：3 → 0。状态0对应于哲学家没有握住任何一个叉子，状态1对应于握住或锁定了右边的叉子，状态2对应于握住两个叉子，状态3对应于只握住左边的叉子。 P的初始状态为0。2.2跨度上的操作定义2.3给定两个跨距（G，g0，l G，r G）和（H，h0，l H，r H），我们如下定义它们的余元（G·H，k0，lG·H，rG·H）。 定义两个有限图G×AH，称G和H的限制积. G×AH的一个顶点是任意一对顶点（g，h）∈G×H.G×AH的一条边是一对边（α，β）∈G×H使得rG（α）=lH（β）.自相关图G·H是图G×AH的一个从顶点（g0，h0）可达的子图，该顶点是复合图的初始状态k0边（α，β）∈ G·H的左标号定义为lG·H（α，β）=lG（α），其右标号为rG·H（α，β）=rH（β）.定义2.4如果G是一个有两个界面的跨度，那么G的反馈，记为Fb（G），是没有界面的跨度，定义如下。定义G<$是与G有相同顶点的自同构图，但只有那些左标号等于右标号的边。 Fb（G）是G的从G的初始状态可达的子图。我 们 定 义 一 个 直 线 系 统 ， 或 者 仅 仅 是一 个 系 统 ， 是 一 个 复 合 的X1·X2·... ·跨度的X n，有时也表示为X1X2. X n. 环系是一种形式为Fb（X1X2.X n）。例2.5系统（FP）nF模拟了n个哲学家坐成一排吃饭的系统。n个哲学家围坐在一张桌子旁用餐的经典问题可以用系统Fb（（FP）n）来模拟。P. Katis等/ Electronic Notes in Theoretical Computer Science 104（2004）181-197185→··∈≤⇒⇒⇒→ → →−注2.6上面考虑的代数结构本质上是一个幺半群加上一个反馈（或迹）函数在这里，有两个接口的跨度集扮演幺半群M的角色，而没有接口的跨度集扮演集合S的角色。2.3互模拟我们在这里定义的互模拟概念是分支互模拟概念的一个微小变化。通过[6]的Stuttering引理，我们的概念给出了与分支互模拟相同的跨度上的双相似等价关系定义2.7假设G和H是具有两个界面的跨距。G和H之间的双模拟是关系R<$Vertex（G）×Vertex（H）使得（g0，h0）∈R，并且如果（g，h）∈R则：(a) 如果有边a/b：g→gJ（其中a和b可以等于-），则有是路径h = h0h1. （一）第一个n，（二）第一个n1的边在两个界面上都是不可见的，（ii）最后一条边标记为a/b，（iii）对于0i n，（g，hi）R和（iv）（gJ，hn）。(b) h关于g的对称性。我们用R：G=H来表示这种互模拟。 我们说两个跨距G和H是互相似的，如果存在互模拟R：G=H，我们写GH。没有接口的跨度之间的互模拟的概念是微不足道的这并不意味着我们对这样的系统不感兴趣--吃饭的哲学家没有接口。然而，通过将系统的部分抽象为更简单的过程，可以通过使用互模拟来促进对系统的内部结构（有或没有接口）的分析-参见第5下面的定理（来自[9]）涉及双模拟的合成性。定理2.8（i）如果R：G=H和S：H=K是互模拟，则复合关系R S Vertex（G）× Vertex（K）定义了一个互模拟RS：G = K。(ii) 顶点（G）上的恒等关系是互模拟1：G =G。(iii) 如果R：G = H是互模拟，则对偶关系R：H =G是互模拟。(iv) 如果R：F=G和S：H=K是互模拟，则关系式R×S<$（顶点（F）×顶点（H））×（顶点（G）×顶点（K））186P. Katis等/ Electronic Notes in Theoretical Computer Science 104（2004）181-197∈ −∈→−当被限制在顶点（F·H）×顶点（G·K）<$（顶点（F）×顶点（H））×（顶点（G）×顶点（K））定义互模拟R·S：F·H= G·K。推论2.9双相似性是跨度上的等价关系。在双相似等价关系下，跨距的合成在跨距等价类的集合BisAut上导出幺半群结构。证据幺半群BisAut的恒等式是跨距（S（A），n，1 A，1 A）的等价类，其中S（A）是具有一个顶点n，一组边A和自反边−的图。对于任何跨度，G，H，K我们有S（A）·G<$G<$G·S（A）和G·（H·K）<$（G·H）·K。Q3成分极小化在本节中，我们将展示互模拟如何给出一个组合商结构的例子我们使用这个结构来定义一个算法来计算系统的最小化。首先给出了任意两个界面的跨度G的最大自互模拟的构造算法该构造遵循构造转移系统的最大互模拟的标准方法（例如，参见[1]）。给定关于G的状态的关系R，定义一个新的关系E（R）如下：（x，y）∈E（R），如果(i) 对于G中的任意跃迁a/b：x→XJ，存在一条路径y=y0→y1→y2→...n与第一个n1在左侧和右侧上不可见的过渡，其中（x，y i）R对于i = 0，1，..，n 1，且其中（xJ，yn）R，且(ii) y关于x的对称性。从全关系T开始-任何x都与任何y相关。则E k（T）（k = 1，2，3，. ）最终稳定为G的状态上的等价关系，这是从G到自身的互模拟。我们称这种等价关系为G的极大自互模拟。对于任何G，我们定义G的最小化min（G）为以下跨度。它的状态集由G在最大自互模拟关系下的状态等价类组成。存在min（G）中的跃迁a/b：[g]→ [h]，如果G中存在这样一个标号跃迁，则对这类的任何代表都有这样的标号跃迁。 min（G）的初始状态为s[g0].注意，G的最小化的构造不仅产生跨度min（G），而且产生互模拟εG：G=ε min（G），其实际上是P. Katis等/ Electronic Notes in Theoretical Computer Science 104（2004）181-197187›→F {}F函数：ε G：g[g]。 函数ε可以用于定位系统中的死锁。我们注意到分支互模拟的最小化可以在O（n（n+m））时间内完成，其中n是状态数，m是转换数（[7]，[5]）。结构min的关键性质是它在下面的命题的意义命题3.1对于任何跨度G和H，(i) min（min（G））= min（G），(ii) min（G·H）= min（min（G）·min（H）），(iii) εG·H=（εG·εH）<$εmin（G）·min（H）。互模拟的其他概念（例如米尔纳组合最小化算法应用于系统X1. X n是简单地计算系统的值的min，通过交替地计算min和从左边评估组成。我们假设Xi（如果没有，先把它们减到最小。）解释：初始设置M1=X1;对于i=2ton{cal culateMi−1·Xi;calculatemin（Mi−1·Xi）anddεMi−1·Xi;setMi等于min（Mi−1·Xi）}。命题3.1保证了这个算法的正确性;即，M n= min（X1. n），并且εX1·. ·Xn=（εM1·X2·1X3·.. . ·1Xn）<$（εM2·X3·1X4·.. . ·1Xn）双.. . εMn−1·Xn3.1多项式问题定义3.2最小化问题是一个无限序列X1，X2，. 存在一个数c的跨度，使得对于所有i，Xi的状态和转换数小于c。如果min（X1·X2· ···Xn）的状态数和转移数小于b（n）（对于所有n），则称该问题由函数b：N→N一个问题被称为多项式问题（分别）线性或常数），如果它由多项式（分别地，线性或常数）函数。每一个问题X1，X2，... 由指数函数b（n）= c n界定，其中c是X i可能具有的状态和转换的最大数量。关于模型检查，我们感兴趣的问题是以多项式函数为界。在大多数情况下，Xi 举一个典型问题的例子，让=P，P，其中P是通过交换P的左和右标记获得的跨度;P可以被认为是哲学家188P. Katis等/ Electronic Notes in Theoretical Computer Science 104（2004）181-197---→−→−→Σ2k=1留言该 它至少∈ F他想先拿起左手叉子我们下面所示的一个结果是，任何形式为F，P1，F，P2，F，P3，.的问题。其中Pi∈ F被一个常数函数有界。(Note在这类问题中没有对称性，因为我们没有对Pi为了得到一个由线性函数约束的例子，考虑跨度B有两个状态0， 1和两个（非重复性）跃迁m/−：0→ 1，/m：10。这模拟了容量为1的缓冲器或消息传递器：状态0对应于缓冲器为空，状态1对应于缓冲器为满。可以证明min（Bn）有n+ 1个状态：直觉上Bn是容量为n的缓冲器的模型。所以问题B，B，B，... 由线性函数n+2限定。为了获得不受多项式函数约束的示例，考虑具有三个状态0、1、2和三个（非响应的）转换m/2的跨度C。：0个 1人，男/女：1个2和每米：20. 可以把它想象成一个等待接收两条消息的设备，然后只输出一条消息，并返回到它的初始状态。状态 问题C，C，C，... 不是多项式。 看到这个通知，span C n可以接受n在输出一个nk=1不是双相似的国家。K下面的简单观察将有助于我们分析锁定和解锁的跨度。命题3.3假设BisAut的子幺半群F是由有限族F的成员的互模拟等价类生成的。那么任何问题X1，X2，.其中，每个Xi都由常数函数限定。证据取常数为在任何等价类中最小跨度的最大状态数。Q下面的命题将多项式和线性问题的概念与最小化算法的时间复杂度联系起来。命题3.4假设X1，X2，.是一个多项式问题。然后存在一个多项式函数t：N →N，使得对于任何n，将最小化算法应用于系统X1所需的时间. X n小于t（n）。证据关于分支互模拟的标记转移系统的最小化可以在O（s（s+t））时间内完成，其中s是状态数，t是转移数（[7]）。由于我们假设字母表A（其中接口被标记）是有限的，所以它可以在多项式时间内完成。假设最小化具有s个状态的跨度所需的时间由多项式f（s）限定。现在假设多项式q限制问题X1，X2，设c为上界，P. Katis等/ Electronic Notes in Theoretical Computer Science 104（2004）181-197189i=1F F-→− →→−→跨度Xi可能具有的状态数 然后，min（X1. Xn）·Xn+1由多项式q（n）×c有界。设g（n）是一个多项式，nomial是计算乘积所需时间的上限最小（X1. X n）和X n+1。 现在函数t（n）=<$n（g（i）+f（q（i）×c））限制了最小化X1所需的时间X n. 结果如下（由于多项式的积分是多项式）。Q命题3.5假设X1，X2，.是一个持续的问题。然后存在线性函数t：N → N，使得对于任何n，将最小化算法应用于系统X1所需的时间... X n小于t（n）。证据 存在常数c，使得对于所有i，计算min（X1. X i）和X i+1，然后最小化结果小于C. 因此，将最小化算法应用于X1所需的时间... X n小于C×N。Q推论3.6假设是有限族的跨距和子么半群由家族F的成员的互模拟等价类生成的BisAut是有限的。然后将最小化算法应用于任何系统所需的时间X1. Xn，其中Xi∈ F，在n中是线性的.4的示例在这一节中，我们考虑BisAut的有限子幺半群的一些例子，因此也考虑由常数限制的问题，并且可以在线性时间内最小化。特别是，我们研究的类，我们称之为“锁定-解锁”跨度。其中一类包括用餐哲学家的例子。1.设Z是具有一个状态的跨度，并且其唯一的过渡是反射边。这个跨度具有ZGZ<$Z的性质，对于任何G。这一点的直接结果是，对于任何G和H，（ZG）（ZH）<$ZH和（GZ）（HZ）<$GZ。因此，任何包含形式ZG和HZ的跨度的有限族生成BisAut的有限子幺半群。 跨度Z可以被认为是因为它阻塞了一个接口，从而禁止了模型检查中状态的指数增长。例如，如果我们想检查一个属性，如系统ZG1ZG2G3ZG4的死锁。ZG n Z，直观上很清楚我们只需要检查跨度ZG1Z，ZG2G3Z，.，ZG n Z分别为这个性质;并且这样的过程所花费的时间将相对于n线性增加。2. 设N是具有两个状态0，1和跃迁m/−：0 → 1，m/−的跨度。：1个1,每分钟：11，m/m：11和每分钟：10. 我们称之跨越不确定缓冲器或不确定容量的缓冲器。它具有N2<$N的性质;也就是说，它的等价类在190P. Katis等/ Electronic Notes in Theoretical Computer Science 104（2004）181-197∼2∈∈BisAut. 问题N，N，… 是由一个常数限定的。3. 实施例1中通过使用跨度Z来“分解”系统，即限制系统中可能发生的通信，可以识别上述恒定问题。在这个例子中，我们将考虑这种现象的一个更有趣的例子。我们将使用例2.2中的分叉跨度F来代替Z。我们称X为锁-解锁跨度，如果它具有以下属性：从FXF的每个状态都有一条到初始状态的路径。这个想法是X是一个想要完成一个“循环”的进程哲学家P是一个简单的锁定-解锁跨度的例子，如例2.2所述。我们将定义四个无限类F1，F2，F3和F4的锁定-解锁跨度（其中一个将包括P），使得对于X在任何这些类（FX）中，（FX）3. 此外，我们将证明，任何有限子集的F（F1<$F2<$F3<$F4）={FX|X ∈ F1<$F2<$F3<$F4}生成BisAut的有限子幺半群。要做到这一点，我们需要以下定义。我们说G中的一条路径是不可见的，如果路径中的每一个过渡在左边和右边都是不可见的。一个状态（2，x， 2）∈FXF被称为有界的，如果不存在y∈X和FX中从（2，x）到（0，y）的不可见路径。换句话说，（2，x， 2）是有界的，如果为了让X解锁它的左分叉，X必须访问它的右分叉。类似地，状态（1，x， 1）∈FXF被称为有界的，如果不存在y∈X和XF中从（x，1）到（y，0）的不可见路径。一个状态（f，x，2）∈FXF被称为自由的，如果有一个y∈X和一条从（f，x）到（0，y）的FX中的不可见路径，并且如果没有从（f，x）到（2，z）的FX中的不可见路径，其中（2，z， 2）是一个束缚态。这意味着f= 1。类似地，我们说一个状态（1，x，f） FXF是免费的，如果有一个yX和XF中从（x，f）到（y，0）的不可见路径，并且如果XF中没有从（x，f）到（z，1）的不可见路径，则（1，z，1）是束缚态。这意味着f=2。一个状态（f，x，2）∈FXF被称为自由束缚的，如果以下两个条件之一成立：（i）（f，x，2）是束缚的;或（ii）有一个y∈X和一条从（f，x）到（0，y）的FX中的不可见路径，并且没有从（f，x）到（g，z）的FX中的不可见路径，其中（g，z，2）是自由状态。所以一个自由束缚的状态是束缚的或者可以变成束缚的。类似地，我们说状态（1，x，f）∈FXF是自由约束的，如果以下之一P. Katis等/ Electronic Notes in Theoretical Computer Science 104（2004）181-197191∈F◦下面两个条件成立：（i）（1，x，f）是有界的;或者（ii）存在一个y X和一条从（x，f）到（y，0）的XF中的不可见路径，并且在XF中没有从（x，f）到（z，g）的不可见路径，其中（1，z，g）是自由状态。我们现在定义四类锁定-解锁跨度。(i) X∈F1当且仅当形式（1，x， 1），（1，x， 0），（0，x， 2），（2，x， 2）∈FXF是免费的所以如果X在左边执行锁定（相应地，右），它能够遵循该行动与解锁的左边（分别。右）。(ii) X∈F2当且仅当形式（1，x， 1），（1，x， 0），（0，x， 2），（2，x， 2）∈FXF是自由的。(iii) X∈F3当且仅当形式为（1，x， 1），（1，x， 0）∈FXF的所有状态是自由的，形式为（0，x， 2），（2，x， 2）∈FXF的所有状态是自由有界的.(iv) X∈F4当且仅当形式为（1，x， 1），（1，x， 0）∈FXF的所有状态是自由有界的，且形式为（0，x， 2），（2，x， 2）∈FXF的所有状态是自由的.F1中的跨度的一个例子是F;Z也是一个例子。在F4中跨度的一个例子是P.F3中跨度的一个例子是P，这是本节前面定义的左撇子哲学家。2中的跨度的一个例子是P+P，这个跨度是通过取P和P的不相交并集，然后将它们的初始状态粉碎在一起而形成的（它有7个状态和8个非重复的边）。以下是锁定-解锁跨度PJ的示例，其不属于上述四个类别之一。PJ有六个状态0，1，2，3，4，5和以下转变：l/−：0→ 1−/l：1→ 2−/u：2→ 3u/−：3→ 4−/l：4→ 5−/u：5→ 0它不适合这些类的原因是状态（1，1，2）∈FPJF是有界的，而状态（0，4，2）∈FPJF是自由的。另外，我们注意到（FPJ）2不是（FPJ）3的双相似，而是（FPJ）3<$（FPJ）4。设F= F1<$F2<$F3<$F4.4.1假设T ∈ F是有限的。 任何形式为F，X1，F，X2，.的问题其中每个Xi∈T，都有一个常数的界。我们证明，如果S<$FF是有限的，那么BisAut的子幺半群S<$是192P. Katis等/ Electronic Notes in Theoretical Computer Science 104（2004）181-197∈∈∈ F ∈ F∈没问题。这意味着FX1，FX2，FX3，…有一个固定的界限，从这个界限开始，这个要求是直接的。引理4.2如果X和Y是锁定-解锁跨度，则XFY是锁定-解锁跨度。证据考虑一个状态（f，x，g，y，h）∈FXFY F. X或Y中的任何一个拥有或有权访问中间分叉。假设X是。 然后有一条从（f，x，g，y，h）到（0， 0，0，y，h）的路径。存在从（0， 0， 0，y，h）到（0， 0， 0， 0， 0）的路径我们在四元素集合{1， 2， 3， 4}上定义一个幺半群结构如下：∗123411111212343133141414Lemma4. 3若X∈Fi，Y∈Fj，则nXF Y∈Fi<$j.证据首先考虑i = 1和任意j = 1，2，3，4。考虑FXFY F中的状态（2，x，f，y，2）。如果f/= 2，则由于X是锁定-解锁跨度，因此FXF中存在从（2，x，f）到（0， 0， 0）的不可见路径，因此FXFY F中存在从（2，x，f，y， 2）到（0， 0， 0，y， 2）的不可见路径。 假设f= 2。 由于（2，x，f）FXF是自由的，因此在FX中存在从（2，x）到（0，x）的不可见路径，并且因此在FXFY F中存在从（2，x，f，y，2）到（0，x，f，y，2）的不可见路径。因为我们没有对（x，f，y）XFY施加任何限制，所以状态（2，x，f，y， 2）是自由的，因为它们永远不会被束缚。考虑形式为（1，x，f，y， 1）的状态。如果f= 1，则FY F中存在从（f，y，1）到（0， 0， 0）的不可见路径，因为Y是锁定-解锁跨度;因此存在从（1，x，f，y， 1）到（1，x， 0， 0， 0）的不可见路径如果 f= 1，则由于（1，x，1）FXF是自由的，因此XF从（x，1）到（xJ，0），因此FXFY F中的不可见路径从（2，x，f，y， 2）到（0，z，0，y，2），这将我们带到前面的情况f = 1。 既然我们没有如果对（x，f，y）∈XFY施加任何限制，则状态（2，x，f，y， 2）是自由的，因为它们永远不会被束缚。这证明了如果X∈F1，Y∈Fj ，则XFY∈F1.一个对称论证表明，如果X∈Fi和Y∈F1，则XFY∈F1。我们现在考虑X2和Y3的情况.类似于上一段给出的参数可以用来证明任何状态（1，x，f，y， 1）是自由的。我们需要证明，从任何状态都有一条看不见的路径P. Katis等/ Electronic Notes in Theoretical Computer Science 104（2004）181-197193Q∈ F∈J（2，x，f，y，2）到束缚态。如果f/= 2，则存在到状态（2，xJ， 2，y，2）的不可见路径，因为X是锁定-解锁跨度。假设f= 2。由于X∈F2，在FX中存在从（2，x）到（2，XJ）的不可见路径，其中（2，XJ， 2）∈FXF是有界的。由于Y∈F3，在FY中存在一条从（2，y）到状态（2，y， 2）FY F的不可见路径，该路径是有界的。因此，在FXFY F中存在从任意（2，x，f，y， 2）到束缚态（2，xJ， 2，yJ， 2）的不可见路径。 XY3其余的案件可以用类似的方式进行辩论。Q引理4.4对于i = 1，2，3，4，如果X，Y∈Fi，则FXF<$FY F。证据 对任意X∈ F，我们将FXF的状态划分为八个集合U1，U2，U3，U4，U5，U6，U7，U8（其中一些可能是空的）。1. 对任意的x，（f，x，g）∈U1，如果f∈ {0， 2}，g∈ {0， 1}.2.对所有的x，（1，x，2）∈ U2.3. （f，x，2）∈U3，如果它是自由的.4. （f，x，2）∈U4，如果它是自由有界的而不是有界的.5. （f，x，2）∈U4，如果它是有界的.6. （1，x，f）∈U5，如果它是自由的.7. （1，x，f）∈U6，如果它是自由有界的而不是有界的.8. （1，x，f）∈U6，如果它是有界的.对于X∈ F，这个划分是有定义的。请注意，根据Fi的 记住最后一个观察，很容易检查由这个划分引起的等价关系是一个自互模拟（实际上是最大的）。此外，可以直接证明，如果X，Y∈Fi，则X和Y的最小跨度相同。我们可以利用前面的结果推出（FX）2<$（FX）3，其中X∈Fi. 引理4.3，连 同 上 面 的 四 元 素 乘 法 表 ， 意 味 着 XFX∈Fi 。 引 理 4.4 现 在 意 味 着FXFXF≠FXF。因此，想要的结果。引理4.5如果S <$F F有s个元素，则BisAut的子幺半群S<$F的元素个数小于或等于4 ×s +1。证据设F1，F2，F3，F4是四个最小跨度，使得对任意X∈Fi，FXF<$Fi.根据前面的两个引理，对于任意的X1，...，X n∈ F，FX1F... F X n F<$F i，对于某些i。因此，对于某些i∈ {1， 2， 3， 4}和X，使得FX∈S，S的任何元素都等于Fi X的等价类.（请参阅和中的额外的1来自计数幺半群的单位元。）这就完成了索赔的证明Q194P. Katis等/ Electronic Notes in Theoretical Computer Science 104（2004）181-197陆F注4.6我们给出了四个极小跨度F1，F2，F3，F4的明确描述.从引理4.4的证明中可以清楚地看出，F1有4个状态（对应于情况4、5、7和8为空），F2有6个状态（情况3和6为空），F3（情况3、7和8为空）和F4（情况4、5和6为空）有5 states. 我们将最小跨度描述为跨度Q的子跨度，其具有8个状态（每个状态对应于引理4.4的证明中描述的划分的情况之一）和以下转变：l/l：1→2，−/l：1→3，−/l：1→4，−/l：1→5，l/−：1→6，l/−：1→7，l/−：1→8，u/u：2→1，u/−：2→3，u/−：2→4，−/u：2→6，−/u：2→7，−/u：3→1，l/−：3→2，l/u：3→6，l/u：3→7，−/u：4→1，l/−：4→2，−/−：4→5，l/u：4→6，l/u：4→7，−/u：5→1，u/−：6→1，−/l：6→2，u/l：6→3，u/l：6→4，u/−：7→1，−/l：7→2，u/l：7→3，u/l：7→4，−/−：7→8，u/−：8→1。F1是具有状态1，2，3和6的QF2是具有状态1，2，4，5，7和8的QF3是具有状态1，2，4，5和6的QF4是具有状态1，2，3，7和8的Q的子跨度注4.7上述计算可解释如下。锁定-解锁跨度形成BisAut的子幺半群，其包括FX形式的跨度的互模拟类，其中X是锁定-解锁跨度。虽然的子幺半群F1F2F3F4是无限的，但它的任何有限子集S都生成一个有限子 幺半群。注4.8用一个实现该算法的程序进行的探索揭示了BisAut的有限子幺半群的其他例子。其中一个特别令人感兴趣。假设分叉F和哲学家P都被修改如下：每个非相关标签被两个标签替换（例如，锁变成了锁锁和结束锁），每个非相关转换被两个转换替换，转换的开始和转换的结束，中间状态是一个新的状态。那么新的跨度FJ和PJ在BisAut中满足（FJ·PJ）3=（FJ·PJ）2。5僵局在本节中，我们描述一个简单的结果，在许多情况下，来推断不存在可达死锁。这种情况相当类似于数论[11]中的一种情况，其中对自然数进行模约简的想法可以得出丢番图方程在整数中没有解的结论。为了更具体地说明这一点，请考虑P. Katis等/ Electronic Notes in Theoretical Computer Science 104（2004）181-197195--Diophantine Equations的定义：5 kx2− 34ky2= 72k+1（k = 1，2，. . ）的。即使检查一对整数值x，y，表面上看，也是k的指数计算。然而，考虑模4并使用模4的合成约简，方程序列变为单同余x2y22 mod 4（k = 1，2，.. . ），只要检查16个案例，就很容易看出没有解决方案。这意味着没有原来的丢番图方程有一个整数解注意，使用组合归约模2不允许相同的推导。对于同余式的效用来说，信息是丢失的，并且它们只产生关于丢番图方程的负信息我们使用精确类似的参数来证明许多系统没有死锁。定义5.1跨度G的死锁（有两个或没有接口）是一种状态G，使得G之外的唯一转变是空转转变。死锁状态的一个例子是Fb（（FP）3）的状态（1，1， 1， 1， 1， 1），它是对应于每个哲学家具有其右分叉的状态。命题5.2如果g是span G的死锁，则εG（g）是min（G）。 如果g是Fb（G）的死锁，则ε G（g）是Fb（min（G））的死锁。证据很简单我们希望用这些结果和前一节的结果一起来研究以下形式的系统中死锁的存在性：Fb（F X1FX2. 其中X1，X2，.，Xn∈ F.根据命题5.2，如果Fb（min（F X1FX2. F X n））没有死锁，那么Fb（FX1FX2. FX n）没有死锁。 但是使用上一节的结果来计算min（F X1FX2. FX n）。最小量程（F X1FX2. Xn−1F）是四个最小跨距之一（注4.6）F1，F2，F3，F4，比方说Fi。 哪一个可以用么半群结构（引理4.3）在类F1，F2，F3，F4上计算。然后Fb（min（F X1FX2. F X n））= Fb（min（F i X n））。如果这个跨度没有死锁，我们就可以推断出进程环Fb（F X1FX2. F X n）也没有死锁。让我们将其应用于X1，X2，.， Xn ∈ {F，P + P <$，P <$，P}.只有当Fb（min（Fi Xn））没有死锁时，我们才能得到一个结果。一196P. Katis等/ Electronic Notes in Theoretical Computer Science 104（2004）181-197F简单的计算表明，这恰好发生在Fi=F或Xn=F或下列情况下：（i）Fb（min（F3P）），（ii）Fb（min（F4P））。我们用两个简单的例子来说明。例5.3考虑一个哲学家环，其中包含四个右撇子和两个左撇子，定义如下：Fb（FPFP<$FPFP<$FPFP）.重 复 应 用 引 理 4.3 ， 我 们 看 到 PFP<$FPFP <$FP 在 1 中 ， 因 此 min（FPFP<$FPFP <$FPF）= F1。最后Fb（min（FPFP<$FPFP<$FPFP））=Fb（min（F1P））最后一个环没有死锁，因此我们推断出哲学家的原始环没有死锁。例5.4考虑由表达式Fb（FPFPFPFP）定义的四个右撇子哲学家的环。重复应用引理4.3，我们看到PFPFPFP在F4中，因此min（FPFPFPF）是F4。最后Fb（min（FPFPFPFP））=Fb（min（F4P）），最后一个确实有死锁.我们不能通过这个参数来推断死锁（尽管在这种情况下更仔细地检查最小化函数ε确实可以检测到单个死锁）。引用[1] A. Arnold，Finite transition systems，Prentice Hall，1994.[2] E. Clarke，D.朗，K.麦克米兰组合模型检查。在第四届IEEE计算机科学逻辑研讨会上，353-362，1989年。[3] J.C. Corbett和 G. S. Avrunin， Towards Scalable Compositional Analysis ，Proceedings of theSecond Symposium on Foundations of Software Engineering，ed.大卫·