分布式µ-演算：UPP DMC模型检测工具的算法实现及性能研究

µ理论计算机科学电子笔记128（2005）91-105www.elsevier.com/locate/entcsUppDMC：一个分布式的μ-演算FrdrikHolm'en1Marti nLeucker2MarcusLindstro？m3乌普萨拉大学IT系瑞典乌普萨拉摘要我们提出了UPP DMC，一个分布式模型检测工具。它是为检查有限状态系统和µ-calculus规范而定制的，最多有一个最小和最大固定点算子的交替 这个片段也被称为L2. 最近，有效的基于游戏的算法，这一逻辑已被概述。我们描述了这些算法在UPP DMC内的实现，并研究了它们在实际例子中的性能。在一个简单的工作站集群上运行UPP DMC，我们能够检查VLTS Benchmark Suite中给出的最大示例的活性属性，之前没有答案。关键词：模型检测，µ-演算，基于博弈的模型检测1介绍模型检测[5]是一种用于验证复杂硬件和软件系统的强大技术。然而，所谓的状态空间爆炸仍然限制了它的应用。虽然偏序约简或符号模型检查将状态空间减少了几个数量级，但典型的验证任务仍然需要现代时序计算机达到其内存限制。增强当今模型检查器适用性的一个方向1电子邮件地址：frho6915@student.uu.se2电子邮件：Martin. it.uu.se本文作者由欧洲研究培训网络“游戏”提供支持3电子邮件地址：mali1741@student.uu.se1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.10.02192F. Holmén等人/理论计算机科学电子笔记128（2005）91µµµ并行计算机的内存（和计算能力）这一观察结果导致了近年来并行模型检测算法的发展。一个著名的表达规范的逻辑是Kozen一种时序逻辑，用于计算公式的布尔组合，特别是标记的下一状态、最小和最大固定点量化器。最小和最大固定点运算符的（依赖的）嵌套形成了μ-演算的交替深度层次。另一方面，模型检查的复杂性随着交替深度呈指数增长， 所有已知的算法 因此，将公式的交替深度限制在实用的重要程度上，并为这类问题开发有效的算法是合理的。特别是，我们只需要交替深度2，捕捉LTL和CTL的表达能力[6]。在[3]和[12]中，针对μ-演算公式的并行模型检测算法的交替深度分别为1和2。这些片段分别被称为L1和L2。该算法是基于一个特征-µ µ模型检验问题在两个玩家游戏方面的作用[8，14]。更具体来说，这些算法描述了如何并行地为游戏图着色，以回答底层的模型检查问题。对于L2的算法，它表明，游戏图可以分解成组件，可以（经过一些简单的修改）容易地使用着色算法的游戏获得的公式L1着色。为此，文[3]提出了一种并行着色算法，并将其作为L2图着色的子程序。在本文中，我们描述了实际执行的算法的工作站集群和超级计算机，在一个系统中称为U PP DMC。该系统是用C++开发的，使用消息传递标准MPI [9]进行不同计算机之间的当前版本主要是该系统可在www.example.com上获得http://www.it.uu.se/research/project/parallelMC。此外，我们研究了系统的性能在几个工业示例，特别是在VLTS基准套件上。4VLTS代表VLTS基准测试是从通信协议和并发系统建模的各种案例研究中获得的。这些案例研究中有许多与现实生活中的工业系统相对应我们在Linux集群中不同数量的机器上检查了VLTS中所有40个转换系统的两个公式该集群由25台机器组成4http://www.inr ial pe s. 我的意思是，我的意思是，HT MLF. Holmén等人/理论计算机科学电子笔记128（2005）9193µµ一∈ A每一个都配备了两个500 MHz的Intel Pentium III处理器和512 MB的主内存机器与标准的100 MB交换以太网网络互连 检查的公式没有死锁，活锁，因为这些是VLTS中考虑的属性，可以检查所有这些，独立于所使用的操作。我们表明，几乎所有的过渡系统的所有属性都可以在50秒至10分钟内检查。只在最大的系统上检查活锁需要的内存超过机器的总可用内存，并且需要将运行时间降低到大约2.5小时的交换。请注意，许多系统以前无法检查活锁。并行模型检测领域近年来引起了人们的兴趣。 在[13]中，进行了并行可达性分析。底层结构的分布与这里提出的相似，但它们的算法不适合于模型检查时序逻辑公式。 在[10]中完成了一个值得注意的步骤，其中完全μ-演算的符号并行算法本文介绍[4]提出了一种使用昂贵的并行循环检测的LTL模型检查算法。LTL的另一种模型检查算法在[1]中介绍，基于嵌套的深度优先搜索。然而，我们的明确地使用了L2的博弈图的结构。在第2节中，我们回顾了实现的模型检查算法的主要思想。我们在第3节中描述了实现。第四节研究了系统的运行时间和内存性能2并行模型检测算法为了使即将到来的实现部分更容易理解，我们回顾了实现的并行算法的主要思想。然而，我们把我们的论述限制在L1的算法[3]上.我们不给出正式的定义，而只是举例说明。见[3]和[12]的详细信息。设Var是一组定点变量，A是一组动作。在[11]中引入的Var上的模态微演算的正形式公式定义如下：：：=假|真正|X |ϕ1∧ ϕ2|ϕ1∨ ϕ2|[K] |K|νX. |µX.其中XVar和K. [5]对于μ-演算的公式，我们像往常一样引入子公式、自由变量和约束变量以及句子的概念每一个公式都可以用它的图形来表示。这可以根据定点公式划分为组件。图1（a）显示了图表及其5 −94F. Holmén等人/理论计算机科学电子笔记128（2005）91µX。（（v Y. b（（v Y. bµX。（（v Y. b（（v Y J. b（νY. bB是的。B.B.B.⟨a⟩XB.B.B.X是的。BBAXJYYJV X.µY.（YX）µY。（YX）YXV X. （µY.Y）X（µY.Y）XµY.YXY X Y（一）(b) 交替(c) 无交替Fig. 1. 公式图公式Φ = µX的分解。（（v Y. b（（v YJ. ba交替 描述 了最 小和最 大定 点公 式的（ 依赖 ）嵌套 （见 图1 （b ）和 1（c））。为了使程序产生正确的结果，我们必须限制交替。然而，对于算法的大纲来说，这现在并不重要在基于博弈的模型检验中，给定的迁移系统与公式的图根据博弈规则组合成一个所谓的博弈图。图2显示了一个转移系统的博弈图，该系统有两个状态s1和s2，一个从s1到自身的a-循环，一个从s1到s2的b-边，以及公式Φ。公式的图的分解导致了由虚线和点线示出的博弈图的划分。请注意，博弈图可以比转移系统的大小和公式的大小的乘积小得多。可以证明，博弈图的节点（s，n）可以在满足条件时标记为绿色，否则标记为红色。因此，并行模型检测算法的基本内容是构造、分布和着色年q3图二. 一个分区博弈图。s 1，µX。（（v Y. b（（v Y. bs 1，µX。（（v Y. b（（v YJ. bs1，（νY. bBs 1，νY.b第1条，s1，Xs2，Ys 1，νY J.Bs1，bYJs 1，XJs 2，YJs 2，νY.B.B.B.s 2，νY J. Bs2，b，Qs2，b，YJ年q4F. Holmén等人/理论计算机科学电子笔记128（2005）9195µ这个博弈图一般的想法如下：给定一个转移系统和一个L1-公式，我们的方法是同时构造博弈图以及确定其节点的颜色并行。我们的并行算法的思想是，所有的处理器都在一个组件上并行工作，而组件被一个接一个地处理。分配博弈图我们采用某种标准的方法并行分布和构建游戏图（的组件）[13，2]。 作为一种数据结构， 我们使用邻接列表。 我们还需要链接到前任以及关于用于标记算法的节点的后继者。组件是通过典型的广度优先策略并行构建的。给定一个节点q，我们确定它的后继者q1，.，qn.为了获得工作站集群上的配置的确定性分布，人们采用散列函数的精神，为每个配置分配一个整数，然后将其值取处理器数量的模。这个函数f确定了网络中每个节点的唯一位置，而不需要全局知识。因此，我们可以发送每个q∈ {q1，...，qn}到其处理器f（q）。如果q已经在f（q）的局部存储中，则第二次到达q，因此过程停止。如果q的前导与q一起发送，则前导列表相应地增加。如果q不在f（q）的局部存储器中，则它与给定的前趋者以及其所有后继者一起存储在那里。这些都是以同样的方式发送到他们的（wrt。f）处理器，连同q是前驱的信息。相应的进程以类似的方式更新其本地内存。请参考[2]以获得对这种方法和其他可能的存储分布式转换系统的方法的详细讨论。标签游戏图如前一段所述，采用广度优先搜索并行构建博弈图（的一个组成部分）是很容易的。 当达到终端配置时，可以启动向后着色过程。这可以以显而易见的方式并行地进行。在[3]中建立的主要观察结果是，在所有颜色信息传播之后，所有剩余的未着色节点可以在每台计算机上并行着色，而无需任何进一步的通信。为了检查所有的颜色信息都已传播，采用了分布式终止检查算法。96F. Holmén等人/理论计算机科学电子笔记128（2005）91处理器i游戏记录器Comm微演算高消息队列单独世界处理器过渡系统模型检查器级接口通信线程图三. UPP DMC的简化结构。3执行我们已经实现了前面提到的算法在一个系统中称为U PP DMC。 该系统是用C++开发的，使用消息传递标准MPI [9]进行不同计算机之间的通信。它不依赖于Haskell或C++[2]中以前的实现，更注重性能。 当前版本主要是为了展示并行模型检查在实践中的有效性和好处。虽然[3]和[12]中的一些算法可以在计算机上执行，但当前版本的UPP DMC仅部分使用了它。特别是在下一节中显示的测量中，我们对先前生成的过渡系统进行了研究这仅仅是由于实际的原因：为了能够将我们的系统与现有的模型检查器进行比较，我们使用了作为VLTS基准套件提供的预先计算的[6]我们的系统很容易适应一个行为方式不稳定图3给出了UPP DMC的一般结构的概述。那个...为了便于设计和测试，以及为了在更大的模型检查平台中重用，将每个模块都实现一个类或一个模板作为程序其余部分的接口微演算模块µ-calculus模块基本上包含解析和分析读入模型检查器的公式的功能。我们预先计算公式的图形版本及其划分为组件。公式的图只是公式的解析树，扩展了从所有定点变量到定义它们的节点的边。它在构建游戏图表时使用。在这里，我们还可以找出哪些定点变量是交替的。图形的每个子公式都分配了一个数字，用于表示模型检查器其他部分中的子公式6http://www.inr。我的意思是，我的意思是，HT MLF. Holmén等人/理论计算机科学电子笔记128（2005）9197过渡系统模块转换系统模块读取转换并提供用于访问给定状态和动作的后继集合的搜索函数。目前，在模型检查开始之前，完整的转换系统被读入内存这是因为我们检查存储在磁盘上的先前计算的转换系统。当需要在线行为时，这可以很容易地改变。为了节省内存，我们只存储每个处理器上可能需要的转换。如果转换看起来像s1→s2并且f（s1）=j，则可以在编号为j的处理器上使用转换，其中f是状态分布散列函数。转换存储排序的前身和标签，使转换为一个标签标签对被发现在O（log 2kj）的时间，其中kj是唯一的标签标签对transi- tions存储在处理器j的集合中的数量。如果只有一个这样的转换，则用于存储前驱/标签对的转换的存储器使用是12字节，并且如果有t >1个这样的转换，则是12+ 4个t字节博弈图模块游戏图模块定义了模型检查器的主要数据结构。游戏图节点在子公式上进行散列存储，以避免在每个节点中存储子公式。 存储按子公式分组的节点可以很容易地找到组件的初始节点，因为组件中的所有初始节点都具有相同的子公式。回想一下，并行算法一个接一个地作用于博弈图的组件。因此，需要组件的初始节点。该算法总是以向后的方式向图的根传播颜色。因此，存储对后继者的引用是不必要的，而必须建立前导者前趋节点的子公式是已知的，除了变量的前趋节点和μ-或ν-节点。在这里，我们显式存储每个前驱节点的子公式。这是因为它们在图的表示中可能有多个前驱。因此，在可能的情况下，前趋变量只存储为状态，否则我们将同时存储公式和状态（参见图1（a））。着色算法中节点的标记大致如下。如果它是一种或节点，当一个后继节点是绿色时，它变成绿色;如果所有后继节点都是红色，它变成红色。当后继节点和父节点被放置在不同的计算机上时，检查后者的成本可能很高。一般来说，这建议将子节点的颜色信息也保存在父节点中以避免这种情况。然而，对于我们的算法，我们可以做得更好：该算法意味着后继者只改变一次颜色。因此，如果我们知道总数，只计算红色和绿色继任者的数量就足够了98F. Holmén等人/理论计算机科学电子笔记128（2005）91状态颜色前置项∗成功次数颜色关于Succs左子树右子树见图4。 博弈图数据结构。继任者的数量。这极大地改进了边缘交叉处理器的处理，因为不必存储节点的副本以用于颜色管理。图4描述了一个游戏图的典型结构。它包括以下内容：• 对于每个子公式，我们存储包含子公式的博弈图节点的二叉搜索树。• 对于每个博弈图节点，我们在搜索树中存储以下内容：· 一个国家，· 一种颜色，前趋信息（当我们知道前趋子公式时的状态，当我们不知道前趋子公式时的子公式状态对）· 继任者的总数· 红色和绿色继任者的数量，· 对右子树的引用，以及· 左子树的引用。对前几节中概述的算法的一个重要修改是删除不必要的节点。这是通过从不存储只有一个后继节点的节点来实现的，除了初始节点和从不删除的交替变量。每个游戏图节点占用大约36字节的内存加上存储节点的前身所需的数据。为了获得内存使用情况的图片，让我们假设总的主内存容量为1 TB，这对于相当现代的集群来说并不现实。7假设平均分支因子为10，考虑到VLTS中的分支因子，这不是不合理的，如果我们假设我们只在内存中存储转换系统和博弈图，这样的系统可以处理大约2 109个这些数字假定了下面的livelock公式。7例如，安装在亚琛工业大学的Sun Fire SMP集群总共有1 TBhttp://www.rz.rwth-aachen.de/computing/hpc/sun/每个子公式...·F. Holmén等人/理论计算机科学电子笔记128（2005）9199过渡系统和游戏图形数据结构的设计，以提供一个合理的时间以及内存效率。从内存使用的角度来看，它们并没有得到优化然而，我们的重点是检查算法的实用性，而不是将其与更有效的数据结构（如BDD）集成。这可能是今后工作的一个方向通信通信模块提供了一个大类。它提供了一个高级接口，用于发送和接收算法和终止检测中使用的不同类型的消息。当这个类的对象被创建时，一个单独的线程被创建用于网络通信。该类包含一个受保护的数据结构，该结构存储所有入站和出站消息。数据结构由网络线程以及模型检查器模块访问。这使得算法的实现与通信方法我们已经实现了使用MPI和TCP/IP的通信类。MPI版本缓冲消息以更好地利用网络带宽。如果缓冲器已满或超时使缓冲器溢出，则在一个数据包由于到大部分的通信是瓶颈，因此缓冲器的大小和超时间隔对整体性能有很大的影响。如果数据包发送得太频繁，而消息太少，网络就会拥塞。另一方面，如果数据包以太大的间隔发送，接收方可能会无事可做地等待，浪费宝贵的处理器时间。终止检测模块终止检测模块用于确定算法的一个步骤（例如组件的扩展）何时结束，以及下一个步骤（例如封装）何时开始。我们使用Dijkstra的终止检测算法[7]。该算法是基于一个虚拟令牌环形成的所有 处理器。其中一个处理器是终止检测服务器。该处理器启动终止检测，并负责在终止发生时通知其他处理器。简而言之，该算法让令牌围绕令牌环，根据每个处理器上的计算状态改变颜色。然后，终止检测服务器可以在令牌返回时判断计算是否已经终止实现的算法模型检查器模块实现了一个模板，该模板以公式对象、转换系统对象和通信对象作为参数。该实现与上一节中概述的算法非常100F. Holmén等人/理论计算机科学电子笔记128（2005）91财产式没有死锁V X. （[−]X−true）活锁µX。（− XνY. （Y））图五. 测试过程中使用的两个公式名称国家数量转换次数nodeladlock（s）活锁维西2581 114422,581,37411,442,38244 S47突击步枪vasy 4220 139444,220,79013,944,37256 S67分zidanevasy 4338 156664,338,67215,666,58864 s64 svasy 6020 193536,020,55019,353,47459 S125 Svasy 6120 110316,120,71811,031,29295后108秒CWI 7838 591017,838,60859,101,007149秒314 S电话：8082429338,082,90542,933,110162秒134秒vasy 11026 2466011,026,93224,660,513150 S160年代维西12323 2766712,323,70327,667,803160年代177秒CWI 33949 16531833,949,609165,318,222560年代8715S见图6。VLTS中10个最大转换系统在25台机器上运行时的运行时间。在[3]和[12]中详细描述。主要的分歧是在上面的游戏图表中4实践经验我们在Linux集群中的3、6、12、18和25台机器上对VLTS中的所有40个迁移系统检查了两个公式。每台机器都有两个500 MHz的Intel Pentium III处理器和512 MB的主内存。机器与标准的100 MB交换以太网网络互连。图5中的公式是nodlocked和livelock，因为这些是VLTS中考虑的属性。我们在每台机器上运行两个线程，一个是通信线程，另一个运行算法。由于我们的机器有两个处理器，并且线程可以并行运行，因此与在单处理器机器上运行相比，我们可能会获得轻微的性能改进我们的测试表明，[12]中提出的算法可用于大型模型的实际验证。在图6中，我们看到了VLTS中一些最大的转换系统在25台机器上的运行时间（以秒为单位）。时间仅为算法运行时间，不包括公式读取和过渡系统。在几乎所有的例子中，答案都在几秒钟或几分钟内给出。cwi 33949 165318上的livelock运行时间过长是由于内存已满时进行交换。游戏图的内存使用是真正的瓶颈。 了理论F. Holmén等人/理论计算机科学电子笔记128（2005）91101∗∗ ∗ ∗ ∗ ∗−∗∗名称金#game graph节点前置（字节）估计（字节）实数（字节）维西2581 1144215,488,24410,113,18497,007,420923,733,008461,082,044vasy 4220 1394425,324,74016,259,519141,316,7601,357,910,544726,659,444vasy 4338 1566626,032,03216,427,458153,659,9481,438,483,968745,048,436vasy 6020 1935336,123,30024,082,199218,734,8721,919,749,9681,085,694,036vasy 6120 1103136,724,30822,087,877152,118,9761,675,076,432947,282,548CWI 7838 5910147,031,64831,354,431402,914,5123,584,371,5521,531,674,028电话：80824293348,497,43027,081,699399,108,8283,119,767,0001,374,049,992vasy 11026 2466066,161,59243,652,440327,786,1403,170,953,7281,899,273,980维西12323 2766773,942,21848,788,082367,199,9443,547,289,5442,123,570,896CWI 33949 165318203,697,654134,404,2631,724,364,39612,623,298,6486,562,917,864图7.第一次会议。 与最坏情况下估计的无死锁运行上限相比的内存使用情况博弈图中节点数的上限是k n，其中k是公式中子公式的数目，n是转移系统中状态的数目。这对应于所有可能的子公式和状态对都是可达的场景。由于每个博弈图节点占用36个字节，因此它们总共占用36个kn字节。 由于前置公式所需的内存取决于公式，因此我们必须分别以4个字节和8个字节计算导致前置公式我们称子公式的数量为4字节存储r。最后我们得到最坏情况下的公式36k n +4Rm +8 （千美元）r）的M用于近似总博弈图的大小，其中m是转换的数量。在这个公式中，我们假设所有子公式在博弈图中结束的概率相同。在图7中，我们将这个最坏情况的估计与VLTS中十个转换系统的内存使用这个简单的近似值对实际内存使用情况的估计有多好，在很大程度上取决于我们正在检查的公式。由于nodlockup公式在模态运算符中只有−作为标签，因此游戏图的大小将比我们使用特定标签的情况更接近k n。 在图7中，我们可以看到近似值大约是实际值的两倍。对于其他公式，这种差异可能更大。换句话说，公式越具体，博弈图的某些部分就越有可能没有被构造出来。102F. Holmén等人/理论计算机科学电子笔记128（2005）91见图8。更改通信参数（但不包括内存大小和超时）对运行时间的影响。在图8中，我们看到了不同缓冲器大小和通信超时的影响。我们看到运行时间随缓冲器大小的变化而变化。对于这些特定的系统，10到20条消息的缓冲器大小似乎是最有效的。超时的变化对于运行时间来说似乎并不像缓冲器大小那样重要。与没有缓冲的运行时间相比，所有这些变化都很小。这些系统的无缓冲运行时间为：cwi-7838-59101为21769 s，vasy-8082-42933为83008 s，vasy-11026-24660为26174 s，vasy-12323- 27667为29917 s关键点是缓冲器大大降低了运行时间，而缓冲器大小和超时的确切值似乎并不那么重要。在图9中，我们可以看到增加机器数量对运行时间的影响。过渡制度的结构可以限制F. Holmén等人/理论计算机科学电子笔记128（2005）91103100090080070060050040030020010000 5 10 15 20 25 30见图9。两个过渡系统vasy-4220-13944和vasy-6120-11031在3，6，12，18和25处理器上的运行时间。水平刻度是处理器数量，垂直刻度是时间（秒）。过渡系统活锁电话：808242933不满意vasy 11026 24660不满意维西12323 27667不满意CWI 33949165318满意见图10。 活锁是由VLTS产生的，以前不适用。增加机器数量的后果。如果系统的分支因子非常低，那么计算注定在很大程度上是顺序的，因为游戏图的分支使得并行化成为可能。此外，我们看到，并行电源主要是在使用累积的内存时受益。这些例子太小了，不能从超过12台计算机中获利。虽然我们的测量结果表明该算法在实践中表现良好，但我们想提到一个更重要的点。VLTS基准测试套件中的大多数大型示例之前都没有检查过活锁。这是因为当前的模型检查器无法做到这一点。然而，UPP DMC设法在短时间内回答了所有问题对于模型检查工具的实用性来说，最重要的特征是得到一个答案。图10显示了我们获得的结果。“瓦西-4220-13944”“vasy-6120-11031”104F. Holmén等人/理论计算机科学电子笔记128（2005）91µ5结论在本文中，我们描述了一个基于并行博弈的模型检查工具的实现，该工具用于μ-演算的一个重要部分。它也可以用来检查LTL和CTL。此外，我们还研究了模型检查器在现实生活中的例子的性能。我们能够为以前无法处理的系统找到答案。作为未来的工作，这将是有趣的，我们的模型检查工具与状态空间生成器，使建模和模型检查工作台可以提供。引用[1] J. 巴纳特湖 布莱恩，还有我。 不知道。 Property 驱动器故障，但不属于必要的故障。IinVCL2002 ： The Third International Workshop on Verification and ComputationalLogic，Pittsburgh PA，2002.[2] B. Bollig，M.Leucker和M.韦伯无交替的局部并行模型检测µ 技术报告AIB-04-2001，亚琛工业大学。[3] B. Bollig，M. Leucker和M.韦伯无交替μ演算的局部并行模型检验。在Proceedings of the 9thInternational SPIN Workshop on Model checking of Software（SPIN施普林格出版社，2002.[4] L. 布林岛 Cern'a，P. 克雷奇阿尔河。 Pel'an ek. D 是TRIBUTLMD-ChekingaseDonegativecycledetection.在第21届软件技术和理论计算机科学基础会议（FSTTCS'01）的会议记录中施普林格，12月2001年[5] E. M. Clarke，O. Grumberg和D. A.佩尔德。模型检查。麻省理工学院出版社，马萨诸塞州剑桥，1999年。[6] M.大坝CTL* 和ECTL* 是模态微演算的片段。理论计算机科学，126（1）：77-96，4月。一九九四年[7] E. W. Dijkstra 和C. S. 斯科尔滕使用计算进行冲突的终止检测。信息处理快报，11（1）：1-4，8月。1980年[8] E. A. 爱 默 生 角 S. Jutla 和 A. P. Sistla.μ 演 算 片 段 的 模 型 检 验 。 在 Proc.5th InternationalComputer-Aided Verification Conference，卷697的Lecture Notes in Computer Science，Springer，1993中。[9] MPI论坛。标准消息传递接口的文档。 CS-93-214，田纳西大学，1993年11月。[10] O. Grumberg，T. Heyman和A.舒斯特分布式符号模型检验的µ演算。在Proceedings of the 13thConference on Computer-Aided Verification（CAVSpringer，2001年7月。[11] D.浩善命题μ演算的结果。理论计算机科学，27：333- 354，12月。一九八三年[12] M. 洛伊克河 Somla和M. 韦伯 平行 LTL、CTL和L2的模型检验。 在洛Brim和O. Grumberg，编者，《理论计算机科学电子笔记》，第89卷。Elsevier Science Publishers，2003.F. Holmén等人/理论计算机科学电子笔记128（2005）91105[13] 联合Stern和D. L.迪尔使穆尔河的水化。号手术Grumberg，编辑，计算机辅助验证，第9届国际会议，计算机科学讲义第1254卷，第256-267页。Springer，1997年6月。[14] C.斯特灵游戏互模拟和模型检查，1996年7月。 有限模型理论的数学拟合研讨会，威尔士大学，斯旺西。