分布、近似与概率模型检验

理论计算机科学电子笔记135（2006）19-30www.elsevier.com/locate/entcs分布、近似与概率模型检验纪尧姆·吉拉多EPITA研发实验室（LRDE）托马斯·埃罗LRI，巴黎南十一大学理查德·拉森EquipeLogiqueMath′ematique，UMR7056CNRS，UiverityParisVII西尔万·佩罗内EPITA研发实验室（LRDE）syp@lrde.epita.fr摘要APMC是一个模型检查器，致力于根据LTL公式对全概率系统进行定量验证。使用蒙特卡罗方法来有效地近似概率规范的验证，它可以在分布式框架中自然使用。我们在这里提出的工具和它的分布方案，连同广泛的性能评估，显示的方法的可扩展性，即使在集群包含500+异构工作站。关键词：模型检验，APMC，LTL公式，蒙特卡罗方法，概率规范1引言概率模型检验是一种算法方法，旨在自动验证概率系统中的定量属性。1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.10.01620G. Guirado等人/理论计算机科学电子笔记135（2006）19该方法的主要缺点是所谓的状态空间爆炸现象，即工作站在验证大型概率系统时耗尽内存解决这个问题的一个共同的研究方向是设计分布式模型检测算法，以处理更大的系统。这些方法中的大多数是关于状态空间在几台机器上的分布在过去的几年里，我们证明了可以使用完全不同事实上，我们提出使用近似来消除概率模型检测的空间复杂性。使用近似的想法变得越来越流行，现在被几个研究小组使用[16，4]。我们的方法[5]更精确地基于概率系统的执行路径的采样这种方法在构造上是大规模并行的。实际上，可以通过以下方式将计算分布在大型机器集群上：每台机器生成执行路径并验证每条路径上的指定经过一段时间的计算后，主控器已经收到足够的结果，可以对要检查的定量属性的（近似）有效性做出结论在本文中，我们详细解释了我们开发的方法，我们分析了我们的方法在非常大的集群异构机（高达500台机器）的性能所有的实验都是使用APMC（近似概率模型），这是实现我们的方法的工具本文首先简要回顾了相关的工作。然后，在第三节中，我们给出了APMC的理论基础，并解释了它的体系结构和实现。最后，我们在第4节中介绍了在各种案例研究和机器集上进行这些实验表明了该方法的可扩展性。2相关工作在过去的几年中，分布式模型检测已经获得了更新的兴趣，由于出现了容易获得的现在，在计算机科学的每个领域使用这样的集群是一个为了加快模型检验速度和避免状态空间爆炸现象，已经开发了几种使用并行化的第一个想法是分布式状态空间的构造（例如参见[13，3]）。基本上，这是通过散列函数使用可达状态集合的分区来完成的G. Guirado等人/理论计算机科学电子笔记135（2006）1921这种划分引起自然的并行化。关于状态空间的操作，另一种研究方法是提高模型检查器可以处理的转换系统的大小非核心方法被设计来做到这一点[10，9]，特别是对于概率系统（即马尔可夫模型）。这些技术的主要便利之处在于它们可以集成到经典模型检查器中，例如最先进的概率模型检查器PRISM [11]。已经开发和讨论了许多其他方法[7]，但没有一种方法以大规模分布式方式（例如数百台机器）分布整个验证过程我们为概率系统的分布式和近似验证设计的方法是完全不同的，因为它本质上是一种并行方法（由于使用了蒙特卡洛抽样技术）。已经存在其他用于概率系统验证的采样技术[16，4]。[16]的方法使用假设检验的框架，而[4]也使用蒙特卡罗方法。这两种方法也有被并行化的潜力，但是，据我们所知，它3近似概率模型检验3.1理论基础APMC方法[5]使用有效的Monte-Carlo方法来近似完全概率过渡系统上单调性质的满足概率要检查的属性以线性时序逻辑（LT L）表示。3.1.1APMC方法LTL公式建立在一组标记状态的原子命题定义3.1完全概率转移系统（离散时间马尔可夫链的PTS或DTMC）是一个元组M =（S，s，P），其中S是一组数据，s是初始数据，P是转移概率函数，即。为所有s∈S，t∈SP（s，t）= 1.我们用P ath（s）表示第一状态为s的路径集合。路径的长度π是路径中状态的数量，并表示为|π|这个长度可以是无限的。定义了集合P ath（s）上的概率测度Prob以经典的方式[8]。 我们用Prob[φ]表示路径{π|π（0）= s和M，π| = φ}（参见[15]）。设P路径k（s）是PTS中从s开始的长度k>0LTL公式φ的概率22G. Guirado等人/理论计算机科学电子笔记135（2006）19在P路径 k（s）上，k（s）是P路径 k（s）中满足φ的路的测度，记为Probk[φ]。定义3.2 LT L公式φ是单调的当且仅当对所有k > 0，对所有长度为k的路π，M，π| = φ = φ M，π+|= φ，其中π+是π是前缀的任何路径。单调公式的一个基本性质是：若φ是单调公式，0 b−ε。 我们的决定是正确的，有信心（1-δ），样本数为1和log1的多项式。主要优点是，ε δ为了设计一个路径生成器，我们只需要一个简洁的表示转换图的描述，这是一种输入语言的简洁描述，与PRISM（反应模块[1]）中的描述相同。我们的近似问题定义为输入x是DTMC的一个简洁表示，一个公式和一个正整数k。简洁的表示用于生成长度为k的执行路径的集合。随机近似方案是一种随机算法，它以高置信度计算满足公式φ的执行路径集合的概率度量μ（x）的良好近似。定义3.3概率问题的完全多项式随机近似方案（FPRAS）是一个随机算法A，它以x为输入，G. Guirado等人/理论计算机科学电子笔记135（2006）1923模型上属性的概率近似Fig. 1. APMC组件两个实数0<ε，δ 1，并产生值A（x，ε，δ），使得：ΣΣProb|A（x，ε，δ）−µ（x）|≤ε≥1 − δ。A的运行时间是多项式，|X|，1和log 1。ε δ概率被算法的随机选择所取代我们称ε为近似参数，δ为置信参数。算法的复杂度为O（1）。日志1）路径，验证ε2δ在每条路径上的公式φ和计算满足路径的分数这是Probk[φ]的ε定理3.4APMC逼近算法是一个全随机逼近方案，它对LT L公式φ的概率p= Probk [φ]，如果p∈]0，1[.这一结果是利用Cherno-Hoe-Deding界[6]对独立随机变量和分布的尾部进行估计得到的该算法的时间复杂度是log（1/δ）和1/ε的多项式。空间复杂度与执行路径长度成线性关系3.2APMC架构APMC架构是双重的，如图1所示。第一个组件是APMC验证器，它为给定模型（在反应模块中描述）和给定属性（LTL）生成一个ad-hoc验证器，包括一个样本生成器和一个检查器。第二个模块，APMC部署器，获取此验证器和可用计算资源集，将验证器部署在这组计算机上并收集结果，该结果是模型上公式的满意概率的近似用于近似该值的技术假设在一组有界长度的大量独立样本上验证该公式。我们使用样本的独立性来分配样本的生成和验证部署是按照有界元的生成树执行的树的每个节点运行在单个计算资源上，并在其他可用资源上产生虽然它的父母仍然接受模型APMC编译器性能分布式AdHoc生成与验证码APMC部署ssh可用机器列表生成器和验证器实例生成器和验证器实例24G. Guirado等人/理论计算机科学电子笔记135（2006）19图二. APMC部署方案结果，直到收集的样本数量大于请求的数量（如果它是根），它会生成一个样本并验证其上在每次验证时，更新假样本和真样本的计数器每个节点定期（即在固定的超时上）将其伪样本和真样本的计数器发送给其父节点，并重置它们（除了根节点，它等待计算结束以产生这些数字）。当一个节点从它的一个孩子那里收到这些计数器时，它会聚集这些数字，就好像它产生了验证一样（见图2）。这种部署技术被认为是可扩展的，因为关于给定节点的所有通信的数据的数量和量仅取决于树的arity界。树型拓扑结构的选择，以减少启动时间，这是成比例的树的深度，因此对数的计算资源的数量它还提供对数延迟来聚合根中所有节点的结果这种方法的缺点是，系统可能会过度生成和验证一些样本（这并不排除最终结果的有效性，但可能提供比所要求的更好的近似），直到根声称已经生成了足够的样本，并且树被破坏。这种差异在树的高度上也是线性的，并且与通信超时成比例。至于并行化，该技术为容错提供了一个简单的解决方案：由于每个生成和验证都是独立于其他的，其中一些验证可能会丢失，而不会对结果的质量产生影响因此，如果一个计算节点崩溃，它的子节点会认为计算已经完成并停止运行;它的父节点会检测到它并简单地生成一个新的子树。假定以崩溃进程为根的子树的所有工作进程都丢失了，可以再次使用。G. Guirado等人/理论计算机科学电子笔记135（2006）19253.3执行APMC软件由三个独立的组件组成：解析器、核心库和部署工具。这种设计提供了将引擎（核心库）包含在许多模型检查器中的可能性，就像我们正在做的集成到PRISM工具中一样。解析器是一个简单的lex/yacc程序，它解析PRISM语言的子语言（反应模块[1]），以及LTL公式的简单语言。然后，它调用核心APMC库来生成模型的内部简洁表示（在Reactive Modules文件的大小中是线性的），以及属性的内部简洁表示（在属性文件的大小中是线性的然后，该库将生成ad-hoc生成器和验证器作为ANSI C代码（生成器/验证器是由部署器部署的独立程序）。APMC实现了三种策略来生成这个程序的代码，这些代码与反应模块的同步有关：第一种策略（称为编译时同步）预先计算所有规则的组合，从而构建同步的简洁模型表示，其中每个规则都不同步。这是时间上最有效的策略，但也是最消耗内存的策略。在运行时，生成器简单地评估当前配置上的每个保护，构建可触发规则集在这些可触发的规则之间随机选择一个规则，并触发动作以计算下一个配置。第二种策略（运行时同步）用于处理更大的、高度同步的模型。在那里，警卫的评估与同步的计算一起完成，因此在每个模拟步骤中完成，花费更多的时间来计算可触发规则集，但使用更少的内存。只有当模型引入大量同步并且生成的代码禁止高效编译时，才使用此策略最后一个策略是对第一个策略的改进：对于某些模型，在每一步，大多数规则都是可触发的。在这种情况下，不是首先计算可触发的规则（从而评估配置上的每个保护），而是统一选择规则，如果其保护为真，则触发其动作如果它的守卫为假，则随机选择另一个规则由库产生的代码的主循环包括生成路径（即，一组给定长度的配置），并评估每条路径上的属性（线性时间公式）这个循环的迭代次数是程序的一个参数APMC软件的最后一个组件是部署工具。该工具采用由库产生的代码，在不同的体系结构上编译，并将程序部署在一组计算节点上，这些节点遵循有界元的规则生成树在节点上执行的程序26G. Guirado等人/理论计算机科学电子笔记135（2006）19包括两个部分：I/O部分和计算部分。计算部分由核心库生成，而I/O部分是通用的。这个I/O部分实现了生成树。它处理与子节点和节点的父节点的连接。父连接通过标准输出处理。根据体系结构部分中描述的算法，消息被定期发送到父节点当这个文件描述符关闭时，计算停止，程序退出。Children connec- tions是通过ssh（或rsh）命令使用双管道来处理的。部署工具附带了一组传递给ssh命令的shell脚本这些脚本为新产生的计算节点下载并编译生成的代码，在子节点之间分割可用资源的列表，并在节点上递归地启动编译的程序。这种技术并不假定NFS或其他文件共享系统的存在。目前，我们假设每个节点都提供一个远程shell服务（ssh或rsh），以及autotools、Make和一个C编译器。目前正在进行的工作将只假设C编译器，并将通过分解每种架构的编译来减少所需的编译量，而不是在每台机器上进行编译。4绩效评价实验平台由500个Athlon 3000+工作站组成，具有1Gb的RAM，运行在NetBSD 1.6.1，100Mb以太网网络下。使用的远程shell程序是OpenSSH，带有公钥身份验证。每个worker上的编译器是gcc-2.95.3，带有-03选项。所有的测量都是在用餐哲学家问题上进行的，检查了双重可达性属性。用餐哲学家问题[14]，被很好地研究，使我们能够区分现象之间的工具和那些由于模型本身。由于该模型不包括同步，我们使用最有效的策略“编译时同步”进行所有实验第一组图（图3）描述了由于并行化而导致的时间加速为了获得这些结果，我们在160个用餐哲学家问题上运行APMC[14]，在3.2节描述的二叉树部署之后，越来越多的工人。对于所有这些实验，我们设λ= 10−2，δ = 10−10（即通过实验产生940，000条路径这是这些参数的公共值，并且k= 200。曲线上用一组80个测量点的平均值表示。第一个图3（a）显示了总执行时间作为工作器数量的函数可以看出，正如预期的那样，G. Guirado等人/理论计算机科学电子笔记135（2006）19271248163264128 256数量的机器(a) 时间对工人10,90,80,70,60,50,40,30,20,101 2 4 8 16 32 64128 256机器数量（x）(b) 相对放缓图三. 随机就餐哲学家问题执行时间随着工作器数量的增加而快速减少该图还显示了当超过64名工人时，线性加速度的放缓图3（b）着重于这一现象。x轴表示工人的数量，y轴表示相对减速，由公式yx=t1/（x×tx）给出，其中tx是图3（a）中给定x的时间。使用此度量，值1.0表示完美的可伸缩性，而较小的值表明整个系统的使用率较低可以看到，当使用超过32个工人时，在这个例子中，相对减速高于10%部署阶段非常耗时，从32个工作人员开始与计算时间相比，部署持续时间不可忽略。这种累积的时间消耗在树的深度上是指数的（在工作器的数量上是线性的），尽管如此，每个工作器在开始执行之前最多等待对数时间，这解释了为什么在启动最后一个工作器之前增加工作器是计算结束的数量的改进。图4显示了在256个工作者的集群上使用与图3显然，除了arity 1（一串worker）的情况外，增加树的arity并不能显著提高部署系统的性能。另一方面，增加arity并不妨碍性能，因此正如图3所示，当相对减速变得太大时，增加arity以减少树的深度是有意义的最后一个图5显示了验证3到130人用餐所需的时间。时间10e310e210e4（13300相对放缓(6662，(3367，(1691，(864，(475，(257，(168，(128，28G. Guirado等人/理论计算机科学电子笔记135（2006）19050040030020010001 2 3 4 5 6 7 8 9 10 20树的干燥度图四、根据部署树的arity进行模型检查的时间400300200100050 100 150许多哲学家图五. 针对哲学家哲学家的问题所有验证都是在长度为200的路径上进行的32名工作人员用于验证940，000条路径。本实验的目的是评估代码的生成事实上，由于所有验证都使用相同的路径长度和相同数量的路径，因此时间差异仅归因于生成代码的质量。可以看出，曲线分为三个线性部分。代码的主循环包括迭代模型的所有守卫（这些守卫是程序的函数）。警卫的数量随着哲学家的数量线性增加。因此，很自然地，把所有卫兵都赶过来所需的时间与哲学家的数量成线性关系。曲线呈现三个不同的斜率是不太令人期待的。由于130个哲学家问题生成的代码比3个哲学家问题多占用256Kb的驻留内存，我们怀疑这是由于CPU代码缓存造成的时间时间G. Guirado等人/理论计算机科学电子笔记135（2006）1929无效。为了验证APMC是一个周期窃取验证工具，我们进行了另一个实验，包括EPITA计算机科学学院的所有可用计算机我们在一个由500台计算机组成的平台上验证了160位哲学家用餐的问题，这些计算机同时被其他应用程序使用我们进行了两个实验：第一个实验生成了94万条路径，另一个实验生成了940万条路径。第一个实验用了99秒，第二个实验用了446秒。值得注意的是，虽然第二个实验所需的计算量这是因为在第一次实验中，系统没有足够的时间来利用整个平台。5讨论传统上，模型检测是一种非常昂贵的计算活动。该方法的主要缺点是需要内存来最终验证大型系统。 使用近似技术，我们可以用大量系统执行路径上的简单计算来换取内存成本。这是我们可以通过将样本划分为独立处理的集合来大规模分布过程的点使用这种方法，我们可以使用恒定的内存量来验证非常大的系统（当长度k固定时）。可用于核查的计算能力仅受可用计算机数量的限制然而，实验表明，对于每个系统，都有一个临界数量的机器，在此之后，验证所需的时间可能不会显着减少。这是由于部署方案的不可忽略的成本其他实验表明，增加部署树的arity可以在较小的性能代价下降低深度在树的深度和它的arity之间存在一个权衡。树的深度越大，树的节点之间就不会有通信瓶颈，而树的高度越大，每个节点上的通信负载就越大。然而，由于通信量低，因此可以选择合理的arity而不会损失性能。从经济角度来看，APMC也很有趣。由于APMC在后台运行，占用的内存很少，因此它可以在经典的桌面主机上运行。30G. Guirado等人/理论计算机科学电子笔记135（2006）19chines（实现周期窃取技术），从而避免了昂贵的专用工作站集群的成本引用[1] R. Alzheimer和T.亨辛格Reactive模块。第11届IEEE计算机科学逻辑研讨会论文集（LICS），IEEE计算机协会出版社，第207-218页。一九九六年。[2] S. Ben-David，T. Heyman，O. Grumberg和A.舒斯特可扩展的分布式在线符号模型检查。计算机辅助设计中的[3] H.加拉韦尔河马提斯库和我Smarandache。用于模型检测的并行状态空间构造。Proceedings ofthe 8th International SPIN Workshop on Model Checking of Software SPIN[4] R. Grosu和S. A.斯莫尔卡蒙特卡洛模型检验第11届系统构造与分析会议论文集（TACAS2005）。第2712005年[5] T.埃罗 河 Lassaigne ，F. Magniette 和S. 佩罗 内近 似概 率模 型 检验。Proceedings of FifthInternational VMCAI[6] W.锄头。有界随机变量和的概率不等式。美国统计协会杂志，58：13-30，1963年。[7] C. P. Inggs和H.巴林杰关于模型检验的并行化。 第二届关键系统自动验证研讨会（AVOCS技术报告，伯明翰大学，2002年4月。[8] J. Kemeny，J. Snell和A.纳普 可数马尔可夫链Springer-Verlag，1976.[9] W. J. Knottenbelt和P. G.哈里森大型马尔可夫模型的分布式磁盘解决方案技术。Proc. NSMC[10] M.夸特科夫斯卡河穆罕默德湾Norman和D.帕克马尔可夫模型的符号核外求解方法。并行和分布式模型检测研讨会论文集（PDMC[11] M. 夸特科夫斯卡湾 Norman和D. 帕克 PRISM：概率符号模型。Proc. 第12届计算机性能评估建模技术和工具国际会议（TOOLS'02），第200-204页，LNCS 2324，2002年。[12] L. Lovasz和P. Winkler。未知马尔可夫链中的精确混合时间。电子组合学杂志，1995。[13] D. M. Nicol和G. Ciardo.离散状态空间生成的自动化。J.平行分布Comput. ，47（2）：153-167，1997.[14] A. Pnueli和L.扎克多进程概率协议的验证。分布式计算，第1：53-72页[15] 我的瓦迪概率并发有限状态程序的自动验证。 Proc. 26th Annual Symposium on Foundationsof Computer Science，pp 327-338. 一九八五年[16] H. L. S. Younes和R. G. 西蒙斯 离散事件系统的概率检验. 第14届计算机辅助验证国际会议，LNCS，2404：223-235。2002年。