理论计算机科学电子笔记128（2005）53-68www.elsevier.com/locate/entcs匿名环Wan Fokkink1荷兰阿姆斯特丹自由大学计算机科学系庞军2荷兰阿姆斯特丹CWI软件工程系摘要基于Itai和Rodeh [14]的算法，我们提出了两个具有FIFO通道的匿名单向环的概率领导选举算法。与Itai-Rodeh算法相比，我们的算法是有限状态的。因此，可以使用显式状态空间探索来分析它们;我们使用概率模型检查器PRISM来验证，对于大小为4的环，最终以概率1选出唯一的领导者。关键词：分布式计算，领袖选举，匿名网络，概率算法，模型检测。1介绍领导者选举是在网络中选举一个唯一的领导者的问题，在这个意义上，领导者（进程）知道它已经当选，而其他进程知道它们没有当选。Leader选举算法要求所有进程具有相同的本地算法，并且每个计算终止，其中一个进程被选为Leader。这是一个根本性1电子邮件：wan@cwi.nl;wanf@cs.vu.nl2 电子邮件地址：pangjun@cwi.nl1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.04.00454W. Fokkink，J.Pang/Electronic Notes in Theoretical Computer Science 128（2005）53分布式计算中的问题，并有许多应用程序。例如，它是在分布式系统中打破对称性的重要工具。通过选择一个进程作为领导者，可以在分散的环境中执行集中式协议。领导者选举还可以用于从基于令牌的协议的令牌丢失中恢复，通过使领导者负责在当前令牌丢失时生成新令牌。存在广泛的领导者选举算法。这些算法在最坏和/或平均情况下具有不同的消息复杂度此外，它们在通信机制（异步与同步）、进程名称（唯一标识与匿名）和网络拓扑（例如，环、树、完全图）方面也有所不同。单向环的第一个领导选举算法由Le Lann [17]给出。 它要求每个进程都有一个唯一的标识，并具有一个-在恒等式上的tal排序;具有最大恒等式的进程成为领导者。Le Lann算法的基本思想是每个进程在环上发送一条带有其标识的消息。 因此它总共需要n2消息，其中n是环中的进程数。 张和罗伯茨[7] 改进了Le Lann算法，只让具有最大身份的消息完成往返行程;他们的算法仍然要求按顺序 在最坏的情况下有n2个消息，但平均只有nlogn富兰克林[10]开发了一个双向环的领导选举算法，其最坏情况的消息复杂度为O（nlogn）。彼得森[18]和Dolev，Klawe和Rodeh[8] 独立适应富兰克林方向环所有上述算法都适用于异步和同步通信，并且不需要关于进程数量的先验知识。有时网络中的进程不能通过唯一标识来区分。首先，随着网络中进程数量的增加，保持所有进程的身份不同可能变得困难;或者网络可能会意外地将相同的身份分配给不同的进程。其次，身份不能总是在网络上发送，例如出于效率的原因。后者的一个例子是火线，IEEE 1394高性能串行总线。从容错的角度来看，在没有唯一进程标识的情况下工作的领导者选举算法也是期望的。在匿名网络中，进程不携带身份。安格卢因[2]证明了在异步匿名网络中不存在用于选举领导者的终止算法。根据这个结果，拉斯维加斯算法（意味着算法终止的概率大于零，并且所有终端配置都是正确的）是最好的可能选择。W. Fokkink，J.Pang/Electronic Notes in Theoretical Computer Science 128（2005）5355Itai和Rodeh [14，15]基于Chang-Roberts算法提出了一种匿名单向环的概率领导选举算法。每个进程从有限域中随机选择一个标识，如果检测到名称冲突，则具有最大标识的进程开始新的选举回合。假设所有进程都知道环的大小，因此每个进程都可以识别自己的消息（通过作为消息一部分的跳数计数器）。Itai-Rodeh算法是一种Las Vegas算法，以概率1终止;它平均需要nlogn条消息Itai-Rodeh算法除了公平调度之外，不对信道行为做任何假设。一个旧的消息，已经被环中的其他消息所取代，原则上可能导致没有领导者被选举的情况（见图1）。第2.2节）。为了避免这个问题，算法在连续的轮中进行，并且每个进程和消息都被提供一个轮数。因此，可以识别和忽略旧消息。 由于使用了整数，Itai-Rodeh算法具有无限状态空间。在本文中，我们假设通道是FIFO的。我们声称，在这种情况下，轮数可以省略Itai-Rodeh算法。我们提出了两个适应的Itai-Rodeh算法，这是正确的FIFO通道的存在。在第一种算法中，进程只能在其消息完成往返行程时才能选择新的标识，如在Itai-Rodeh算法中是这样的。在第二种算法中，一个进程一旦检测到环中的另一个进程携带相同的标识（即使这个标识可能不是环中最大的标识），就选择一个新的标识。由于这两种算法都不使用整数，因此它们是有限状态的。这意味着我们可以应用模型检查来自动验证算法的属性，在某些时态逻辑中指定。对于特定的环大小，这些属性可以针对算法的显式（有限）状态空间进行检查。我们使用PRISM [16]，一种概率模型检查器，可用于建模和分析包含概率方面的系统。我们在PRISM语言中指定了这两种算法，并且对于大小为4的环，我们验证了该属性：PRISM提供了计算算法在若干消息之后终止的概率的可能性。这些统计数据表明，平均而言，第一种算法比第二种算法需要更多的消息来终止。在PRISM的网页（http://www.cs.bham.ac.uk/~dxp/prism）上，异步环的Itai-Rodeh算法被修改为同步环。在PRISM中，进程在操作标签上同步，因此同步56W. Fokkink，J.Pang/Electronic Notes in Theoretical Computer Science 128（2005）53环可以简单地通过从规范中排除通道来建模。进程在同一轮中同步，因此不需要轮数（类似于我们的算法A）。因此，状态空间变为有限，和PRISM可以用来验证属性最终选出一个独特的领导人”，对于8号以下的戒指。此外，还计算了在一轮选举中选出领导人的概率。关于领导者选举算法的形式验证的更多相关工作可以在本文的完整版本中找到[9]。第2节包含原始Itai-Rodeh算法。在第3节和第4节中，我们提出了两个具有FIFO通道的匿名环的概率领导选举算法。我们用PRISM解释我们的验证结果。第5节揭示了一些实验结果，使用PRISM的消息数需要终止。我们在第6节总结本文并讨论未来的工作。2伊泰-罗德领导人选举考虑一个由n ≥ 2个进程p0，.组成的异步匿名单向环. ，pn−1. 进程通过在通道上发送和接收消息进行异步通信，这些通道被认为是可靠的。通道是单向的：由pi发送的消息被添加到p（i+1）modn的消息队列中。消息队列由公平调度器引导，这意味着在每个无限执行序列中，每个发送的消息最终都会到达其目的地。进程是匿名的，因此它们没有唯一的标识。面临的挑战是提出一个统一的本地算法为每个进程，这样一个领导者被选为进程之间2.1Itai-Rodeh算法Itai和Rodeh [14，15]研究了如何使用概率算法打破匿名网络中的对称性。他们提出了一种概率算法，在上述网络模型中选出领导者，假设进程知道环的大小为n。这是一个拉斯维加斯算法，以概率1终止。Itai-Rodeh算法基于Chang-Roberts算法[7]，其中假设进程具有唯一标识，并且每个进程发送携带其标识的消息。只有具有最大标识的消息才能完成往返行程并返回到其发起者，该发起者成为领导者。在Itai-Rodeh算法中，每个进程从 一个有限的集合因此，不同的进程可能具有相同的特性。每个进程再次发出一条携带其标识的消息。消息提供有W. Fokkink，J.Pang/Electronic Notes in Theoretical Computer Science 128（2005）5357跳计数器，以便进程可以识别其自身的消息（通过检查跳计数器是否等于环大小n）。此外，环中具有最大标识的进程必须能够检测环中是否存在具有相同标识的其他进程。 因此，每个消息都提供了一个位，当它通过一个不被污染的进程时， 其发起人，但共享相同的身份。当一个进程收到自己的消息时，它要么成为领导者（如果该位是干净的），要么选择一个新的标识并开始下一轮选举（如果该位是脏的）。在下一轮选举中，只有共享环中最大标识的进程才是活动的。所有其他进程由于接收到标识大于它们自己的标识的消息而变得被动。活动进程保持一个整数，最初从零开始，并在每一轮新的选举中增加。因此，前几轮选举的信息可以被识别和忽略。我们继续提出一个详细的描述Itai-Rodeh算法。每个进程pi都有三个参数：- idi∈ {1，...，k}，其中k≥ 2，是它的恒等式;- 状态i的范围在{主动，被动，领导者}上;- roundi∈N表示当前选举回合的数量。只有主动进程可以成为领导者，被动进程只是传递消息。 在新一轮选举开始时，每个活动进程发送一条形式为（id，round，hop，bit）的消息，其中：- id和round的值取自发送消息的进程- hop是一个计数器，初始值为1，每次被进程传递- bit是一个初始为true的位，当它访问一个具有相同标识但不是其发起者的进程时，它被设置为false如果每个进程都是被动的或被选为领导者，并且通道中没有剩余的消息，则我们说Itai-Rodeh算法的执行序列已经终止58W. Fokkink，J.Pang/Electronic Notes in Theoretical Computer Science 128（2005）53Itai-Rodeh算法• 最初，所有进程都是活动的，每个进程pi随机选择其标识idi∈{1，.，k}并发送消息（id i，1，1，true）。• 在接收到消息（id，round，hop，bit）时，被动进程pi（状态i=被动）传递消息，将计数器跳数增加1;主动进程pi（状态i=主动）根据以下步骤之一进行操作：J·如果hop=n且bit=真，则pi成为领导者（状态i=领导者）;·如果hop = n并且bit = false，则p选择新的随机身份id∈ {1，.，k}，移动J我我进入下一轮（roundJ=roundi+1），并发送消息（idJ，roundJ，1，true）;我我我· 如果（round，id）=（roundi，idi）且跳数为n，则pi传递消息（id，round，hop+1，false）;· 如果（round，id）>（roundi，idi），a，则pi变为被动（状态J=被动）并传递我消息（id，round，hop+1，bit）;· 如果（round，id）（roundi，idi），则pi清除消息。
v（v，1，true）v（x，1，true）v >w，x（v，3，true）vv > w，x图1.一、如果通道不是FIFO，则必须使用舍入数W. Fokkink，J.Pang/Electronic Notes in Theoretical Computer Science 128（2005）5359算法A.• 最初，所有进程都是活动的，每个进程pi随机选择其标识idi∈{1，.，k}并发送消息（id i，1，true）。• 在接收到消息（id，hop，bit）时，被动进程pi（状态i=被动）传递消息，将计数器跳数增加1;主动进程pi（状态i=主动）根据以下步骤之一进行操作：·如果hop=n且bit=真，则p1成为领导者（状态J=领导者）;我·如果hop = n并且bit = false，则p选择新的随机身份id ∈ {1，. ......、k}并发送J我我message（id，1，true）;J我·如果id > id，则p变为被动（state=passive）并且传递消息（id，hop+·如果id=idi和hop n，则pi传递消息（id，hop+ 1，假）;J我我我1，bit）;·如果id idi，则pi清除消息。3无轮数的我们观察到，如果通道是FIFO，则舍入数是冗余的。因此，我们得到了Itai-Rodeh算法的简化。算法A是通过仅考虑Itai-Rodeh算法中的那些情况而获得的，其中，进程P1和传入消息具有相同的轮数。由于消除了舍入数，算法A是有限状态的，与Itai-Rodeh算法相反。因此，我们可以应用显式状态空间生成和模型检查来确定算法A对于固定环大小的正确性PRISM [16]是一个概率模型检查器。它允许人们对包含概率方面的系统和算法进行建模和分析。PRISM支持三种概率模型：离散时间马尔可夫链（DTMC）、马尔可夫决策过程（MDP）和连续时间马尔可夫链（CTMC）。如果模型是DTMC或MDP，或者是CTMC情况下的CSL [3]，则通过针对概率时序逻辑PCTL [12，4]为了模型检查算法A的概率性质，我们首先使用PRISM语言将算法编码为DTMC模型，PRISM语言是一种简单的基于状态的语言，基于Reactive Modules formalism of Alzheimer和Henzinger [1]。一个系统是由许多模块组成的，这些模块包含局部变量，并且可以相互交互。DTMC的行为由以下形式的一组命令描述：[a]g→λ1：u1+. +λl：ulA是进程代数风格的动作标签，其将同步引入模型。它只能由所有在其规范中出现动作标签a的模块同时执行。如果一个转换不需要与其他转换同步，60W. Fokkink，J.Pang/Electronic Notes in Theoretical Computer Science 128（2005）53需要为这种过渡提供标签。符号g是系统中所有变量每个ui描述了一个转换，如果g为真，模块可以进行转换转换通过相对于变量的未初始化值给出它们的新初始化值来更新变量的值λi用于为转换分配概率信息要求λ1+···+λ1= 1。 如果l = 1（因此λ1= 1），则可以省略该概率信息。PRISM将没有传出转换的状态视为错误状态;终止状态可以通过添加自循环来建模。我们使用PRISM来验证算法A满足概率属性我们在PRISM中将每个FIFO通道和每个进程建模为单独的模块。以下是PRISM语言中的简化代码给出了大小为2的通道的规格通道channel1从进程p1接收消息（mes1 id，mes1 counter，mes1 bit）（在来自p1的动作标签rec上同步）并将其发送到pro。cessp2（在动作标签上同步发送到p2）。每个位置i∈ {1， 2}在信道由三个自然数表示：一个用于包含在消息中的进程标识（B12I1），一个用于跳计数器（B12I2），一个用于比特（B12I3）。如果通道中某个位置的自然数大于零，则意味着该位置被消息占用。否则，该位置为空。我们提出了进程p1和p2之间的通道。进程的数量和标识集的大小都是2（N=2; K=2）。模块通道1b 1 2 11：[0..K]; b 1 2 12：[0..N]; b 1 2 13：[0..1];b 1 2 21：[0..K]; b 1 2 22：[0..N]; b 1 2 13：[0..1];[rec from p1] b 1 2 11=0→（b 1 2&11 '= mes1 id）（b 1 2 12'= mes1 counter）（b 1 2[从p1接收]（b 1 2 11>0）（b 1 2 21=0）-（b 1 2&21 '= mes1 id）（b 1 2 22'= mes1 counter）（b 1 2[发送到p2] b 1 2 11>0→（b 1 2&（b 1 2&（b 1 2端模mes1 id、mes1 counter和mes1 bit是共享变量。它们在下面的模块process1中用于接收和发送消息。只有在该模块中，才能为这些变量赋值。 消息的标识是mes1 id，mes1 counter它的跳计数器，mes1位表示干净（1）或脏W. Fokkink，J.Pang/Electronic Notes in Theoretical Computer Science 128（2005）5361（0）位。如果不存在消息，则所有三个变量的值都为零。(Somes1 bit=0有两种含义：要么没有消息，要么该位是脏的。每个进程pi通过变量processi id指定：[0. K]表示其身份（其中0表示该过程是被动的或选择新身份），变量si：[0. 5]对于其本地状态（这在下面解释），以及变量leaderi：[0.. 1]（在状态中，0表示进程是被动的，1表示进程是被动的。是领导者）。下面的PRISM代码是进程p1的规范。模块进程1进程1 id：[0.. K]; s1：[0.. 5]; leader1：[0..1];mes1 id：[0..K]; mes 1计数器：[0..N]; mes 1位：[0..1];当一个进程处于状态0时，它是活动的，可以随机地（通过概率R=1/K建模）选择它的标识，用这个标识构建一个新的消息，并将其状态设置为1。[ ] s1=0-R：（s1 '= 1）（process1 id'=1）（mes1 id'=1）（mes1 counter'= 1）（mes1 bit '= 1）+ R：（当s1=1时，进程将新消息发送到通道1（通过在来自p1的动作rec上与通道1的同步来建模），并移动到状态2。[从p1接收] s1=1在状态2中，该过程可以从信道2接收消息（通过在动作send到pl时与模块信道2的同步来3 .第三章。注意，b 2 1 11、b 2 1 12和b 2 1 31是共享变量，表示模块通道2中的第一个位置。[发送到p1] s1=2→（&s1 '= 3）（mes1 id'= b 2 1 11）（mes1当一个进程处于状态3时，它收到了一条消息并做出了决定。如果进程得到了自己的消息（mes1计数器=N）并且消息的位是干净的（mes1位=1），则进程被选为领导者（[]（s1=3）（mes1计数器=N）（mes1位=1）→（&&如果mes1计数器=N且mes1位=0，则进程将其状态更改为0，并将62W. Fokkink，J.Pang/Electronic Notes in Theoretical Computer Science 128（2005）53选择一个新的随机身份。[]（s1=3）（mes1计数器=N）（mes1位=0）→（s1 '= 0）（process1 id'=0）（mes1 id'= 0）（mes1 counter'= 0）（mes1 bit '= 0）;如果mes1 id=process1 id和mes1 counterN，则进程已收到具有相同标识的消息，但该消息并非源自自身。 它将消息中的跳数计数器增加1，使位变脏，并移动到状态5以传递消息。[]（s1=3）（mes1 id=process1 id）（mes1计数器N）→（[]（s1=3）（mes1 idprocess1 id）→（ 1，并进入状态4，在状态4中它变为被动的（即，leader1的值保持为零）。[]（s1=3）（mes1 id>process1 id）→（在状态5中，进程传递消息，并移动到状态2。[来自p1的rec]（s1=5）→（s1 ′ = 2）（mes1 id ′ = 0）（mes1 counter ′ = 0）（mes1 bit ′= 0）;在状态4中，被动进程（leader1=0）只能传递跳计数器加1的消息。[发送到p1]（s1=4）（leader1=0）（mes1 id=0）→（mes1&id '= b 2 1 11）（mes1 counter'= b 2 1 12+1）（mes1[rec from p1]（s1=4）（leader1=0）（mes1 id>0）→（mes1id '= 0）（mes1 counter'= 0）（mes1 bit '= 0）;我们将合取leader1=0添加到谓词中，以强调leader不必处理传入的消息。也就是说，当一个进程被选为领导者时，由于通道是FIFO，因此没有剩余的消息。在状态4中的过程中添加了一个自循环，其中同步操作标签为done，以避免死锁状态。[done]（s1=4）→（W. Fokkink，J.Pang/Electronic Notes in Theoretical Computer Science 128（2005）5363过程身份通道尺寸FIFO国过渡Ex.1222是的127216实施例2333是的5,46712,360实施例3434是的99,329283,872表1具有FIFO通道的算法A端模其他通道和进程可以通过仔细地对模块channel1和process1进行模块重命名来构造。每个变量的初始值是其范围内的最小值。下面，我们将具有两个过程的环的属性属性：P>=1 [ true U（s1=4 s2=4 leader1+leader2=1 b 1 211+b 2 1 11=0）]它指出，最终p1和p2都处于状态4的概率（s1=4 s2=4），恰好有一个进程被选为领导者（leader1+leader2=1），至少是一个。此外，我们检查算法终止时环中没有消息（b 1 2 11+b 2 111=0）。为了模型检查此属性，算法描述（基于模块的语言）被解析并转换为MTBDD [11]。在PRISM中，执行可达性以识别不可达状态，并相应地过滤MTBDD。表1显示了我们构建的每个模型的统计数据。第一部分给出了每个模型的参数：环的大小n，单位集的大小和通道的大小。不难看出，在任何时候，环中最多有n个消息，因此信道大小为n;并且具有n个不同的可能身份意味着在每个“回合”中，所有活动进程都可以选择不同的身份。第二部分给出了表示模型的MTBDD中的状态和转换的在表1中的所有环形网络上都成功检查了属性（我们使用模型检查器PRISM2.0及其默认选项）。 注意对于n= 4时，我们只能检查大小为3的恒等式集的属性为n= 4和大小为4的恒等式集，并且通常对于n≥5，PRISM失败建立一个模型，因为缺乏记忆。64W. Fokkink，J.Pang/Electronic Notes in Theoretical Computer Science 128（2005）53算法B• 最初，所有进程都是活动的，每个进程pi随机选择其标识idi∈{1，.，k}并发送消息（idi，1）。• 在接收到消息（id，hop）时，被动进程pi（状态i=被动）传递消息，将计数器跳数增加1;主动进程pi（状态i=主动）根据以下步骤之一进行操作：J·如果hop=n，则pi成为leader（状态i=leader）;·如果id = id且跳数为 idi，则pi变为被动（状态J=被动），并传递消息（id，hop+我1）;· 如果ID为i，则pi清除消息。4没有比特的在本节中，我们将介绍另一个领导者选举算法，它是算法A的一个变体。再次假设通道为FIFO。我们观察到，当活动进程pi检测到名称冲突时，这意味着它接收到具有自己的标识和小于n的跳计数器的消息，pi没有必要等待自己的消息返回。相反，pi可以立即选择新的随机身份并发送新消息。 算法B是ob-通过根据该观察调整算法A来获得 特别是所有出现的位都被省略。通道的建模方式与第3节相同。我们为每个进程pi提供一个变量process iid：[0. K]对于其身份，变量si：[0. 4]对于其局部状态，以及变量leader i：[0..1]。我们只给出了过程p1的PRISM规范的一部分。当进程处于状态0时，1、2或4被省略，因为该行为与算法A非常相似（参见第3节）。状态5在这里是多余的，因为一个进程选择了一个新的标识一旦发现名字冲突模块进程1进程1 id：[0.. K]; s1：[0.. 4]; leader1：[0.. 1]; mes1 id：[0..K];mes 1计数器：[0.. N];当进程处于状态3时，它已经从通道接收到消息并做出决定。如果mes1计数器=N，则进程被选为领导者（[]（s1=3）（mes1计数器=N）→（s1 '= 4）（进程1 id'= 0）（mes 1 id '= 0）（mes 1计数器'= 0）（领导者1 '= 1）;如果mes1 id=process1 id且mes1计数器为N，则进程返回到状态0并将选择新的身份。W. Fokkink，J.Pang/Electronic Notes in Theoretical Computer Science 128（2005）5365n−1过程身份通道尺寸FIFO国过渡Ex.1222是的97168实施例2333是的6,01914,115实施例3434是的176,068521,452实施例4444是的537,4671,615,408实施例5525是的752,0472,626,405表2具有FIFO通道的算法B[]（s1=3）（mes1 id=process1 id）（mes1计数器N）→（[]（s1=3）（mes1 idprocess1 id）→（s1 ′ = 2）（mes1 id ′ = 0）（mes1 counter ′ = 0）;如果mes1 id>process1 id，则进程变为被动，将消息的跳数增加1，并进入状态4。[]（s1=3）（mes1 id>process1 id）→（s1 '= 4）（process1 id'= 0）（mes1 counter '= mes1counter+1）;...端模其他通道和进程可以通过模块重命名来构造。针对算法B，在FIFO通道设置中，针对大小为5的环，成功对属性进行了模型检查。对于任何较大的戒指尺寸，在环大小为5且单位域包含3个元素的情况下，PRISM无法产生MTBDD。表2总结了采用PRISM的算法B5性能分析[ 14 ]中的概率分析表明，如果k = n，Itai-Rodeh算法在大小为n的环中选出一个领导者所需的期望轮数是bounderdbye·n。预期将为一个小时提供更多的服务时间复杂度O（n） 因此，Itai-Rodeh算法的平均消息复杂度是时间复杂度O（n）同样，算法A和B的平均消息复杂度为O（nlogn）。概率时序逻辑PCTL [12，4]可以用来表示软66W. Fokkink，J.Pang/Electronic Notes in Theoretical Computer Science 128（2005）53过程身份通道尺寸步骤㈧步骤（B）Ex.122225.019.0实施例233333.629.3实施例343452.546.0表3在为每个算法选出唯一领导者之前的预期步骤数最后期限，例如3.计算具有两个过程的环在t个离散时间步内选出领导者的概率的PCTL公式为：P=？[ true U =t（s1=4 s2=4 leader1+leader2=1）]我们使用PRISM来计算算法A和B在给定数量的转换内终止的概率，对于大小为2和3的环。图2和图3中给出的实验结果表明，算法B似乎比算法A具有更好的性能。注意，当t移动到无穷大时，两种算法都以概率1选出领导者2个过程，2个身份10.90.80.70.60.50.40.30.20.1010 20 30 40 50 60 70 80 90 100离散时间步数图二. 选举一个有截止日期的领导人的概率。我们还使用PRISM的开发版本来计算在为每个具有固定配置的算法选出唯一领导者之前的预期步骤数。(This新功能将包含在下一版本的PRISM.）一些实验结果（见表3）表明，算法B平均比算法A快。3每个离散时间步长对应于算法中的一个转换算法A算法B选出领袖W. Fokkink，J.Pang/Electronic Notes in Theoretical Computer Science 128（2005）53673个过程，3个身份10.90.80.70.60.50.40.30.20.1010 20 30 40 50 60 70 80 90 100离散时间步数图三. 选举一个有截止日期的领导人的概率。6结论与未来工作本文提出了两个具有FIFO通道的匿名单向环的概率性领导选举算法这两种算法都经过了指定，并成功地使用PRISM进行了模型检查他们满足“概率为1 ， 最 终 只 有 一 个 领 导 人 当 选 ” 的 假 设 PRISM 中 的 完 整 规 范 可 在www.example.com上www.cwi.nl/~pangjun/leader。状态空间的生成和验证在具有512 Mb存储器的1.4 GHz AMD AlthlonTM处理器上执行此外，我们为每个算法提供了手动正确性证明（参见[9]）。未来的工作是形式化和检查这些证明通过一个定理证明，如PVS。Itai和Rodeh [14]指出：“We could have used any of the improved algorithms [沿着这个方向，我们开发了两个概率领导选举算法，基于Dolev-Klawe-Rodeh算法[8，10]。它们都是有限状态的，我们在µCRL [5]中成功地对它们进行了模型检查，六号的戒指。Dolev-Klawe-Rodeh算法的调整与我们的Chang-Roberts算法的调整（算法A和B）非常相似;即，进程再次选择随机标识，以完全相同的方式解决。因此，我们的Dolev-Klawe-Rodeh算法的适应性在这里不介绍。感兴趣的读者可以在www.example.com上找到我们所有算法的规范www.cwi.nl/~pangjun/leader。这些规范采用的是语言µCRL，该语言用于初始非概率模型检查练习。算法A算法B选出领袖68W. Fokkink，J.Pang/Electronic Notes in Theoretical Computer Science 128（2005）53确认该研究由荷兰技术基金会STW在项目CES 5008下支持。我们感谢GethinNorman帮助我们进行PRISM。引用[1] R. Alzheimer和T. A.亨辛格Reactive模块。系统设计中的形式化方法，15（1）：7-48，1999。[2] D. 安格鲁 处理器网络中的局部和全局性质（扩展摘要）。 在Proc. STOC82-93，ACM，1980年。[3] C.拜尔湾Haverkort，H. Hermanns和J. - P·加藤通过瞬态分析对连续时间马尔可夫链进行模型检验。在Proc. CAV 358-372. 斯普林格，2000年。[4] C. Baier和M.奎亚特科夫斯卡具有公平性的概率分支时间逻辑的模型检验。分布式计算，11（3）：125-155，1998年。[5] S. C. C.布洛姆，W. J. Fokkink，J. F.格鲁特岛A. van Langevelde，B. Lisser和J.C. van dePol.µ CRL：一个分析代数规范的工具集。在Proc. CAV250-254. Springer，2001年。[6] J. E.伯恩斯消息传递系统的形式化模型。技术报告TR-91，印第安纳大学，1980年。[7] E. J. H. Chang和R.罗伯茨一种改进的循环过程分散求极值算法。Communication of the ACM，22（5）：281-283，1979.[8] D. Dolev，M. Klawe和M.罗德一个O（nlogn）时间复杂度的算法。Journal of Algorithms，3：245-260，1982.[9] W. J. Fokkink和J. Pang。简化匿名戒指的Itai-Rodeh领导人选举。技术报告SEN-R 0405，CWI阿姆斯特丹，2004年。[10] R.富兰克林关于处理机循环配置中分散极值搜索的一种改进算法。Communication of the ACM，25（5）：336-337，1982.[11] M. 藤 田 市 McGeer 和 J.C. - Y. 杨 Multi-terminal binary decision diagrams ： An efficient datastructure for matrix representation. 系统设计中的形式化方法，10（2/3）：149-169，1997。[12] H. Hansson和B.琼森关于时间和可靠性的推理逻辑。Formal Aspects of Computing6（5）：512-535，1994.[13] D. S. Hirschberg和J. B. 辛克莱尔 循环过程配置中的分散极值发现。Communication of theACM，23（11）：627-628，1980.[14] A. Itai和M.罗德分布式网络中的对称破缺。在Proc.FOCS150-158. IEEE计算机学会，1981年。[15] A. Itai和M.罗德分布式网络中的对称破缺。信息与计算，88（1）：60-87，1990。[16] M. Z. 夸特科夫斯卡湾Norman和D.帕克PRISM：概率符号模型检查器。在Proc.TOOLS200-204.施普林格，2002年。[17] G.勒兰分布式系统：走向正式的方法。信息处理77，IFIP大会，pp。155-160，1977年。[18] G. L.彼得森一个O（nlogn）的循环极值问题的单向算法。IEEE Transactions on ProgrammingLanguages and Systems，4：758-762，1982。
我的内容管理
展开
