布尔不动点方程的记忆有效解法及空间复杂性的研究[J].

理论计算机科学电子笔记133（2005）175-191www.elsevier.com/locate/entcs求布尔方程组MisaKeinéanen1，2赫尔辛基理工P.O. Box 5400，FIN-02015 HUT，Finland摘要本文研究布尔不动点方程的记忆有效解法。我们展示了如何利用在解决验证问题时经常遇到的固定点方程系统的某些结构，以大幅提高固定点计算的性能。此外，我们还研究了求解布尔方程组问题的空间复杂性，给出了一个NL-困难的结果。所提出的技术的原型已经实施，并报告了一系列的协议验证基准的实验结果保留字： 算法，布尔方程组，记忆效率，空间复杂度。1介绍许多用于有限状态并发系统的验证工具和算法需要求解固定点方程，例如用于检查行为等价性和模型检查μ-演算的方程[17]。然而，求解一般的不动点方程是一项困难的任务，没有多项式时间算法可以解决这个问题。已知（尽管问题是在NPco−NP[11]中，甚至在UPco−UP中[16]）。1感谢Petteri Kaski进行了宝贵的讨论。Jaco van de Pol对[8，13]中的规范提供了有用的评论。 这项工作得到了芬兰科学院（项目53695），Emil Aaltonen基金会和赫尔辛基计算机科学与工程研究生院的财政支持。2电子邮件地址：mkk@tcs.hut.fi1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.08.064176M. Keinänen/Electronic Notes in Theoretical Computer Science 133（2005）175已经开发了特殊的技术来克服这一点，并且有许多实际相关的固定点方程组，它们确实具有非常有效的算法[1，4，6，11，12，14，19]。但一个遗留的问题是这些技术的内存消耗。工业规模的验证问题通常会导致系统包含数百万个定点方程，这些方程可能会变得太大，无法同时容纳内存。然而，到目前为止，还没有人研究求解定点方程组的空间复杂性，也很少有人注意开发内存高效的求解算法。本文研究了求解布尔方程组的高效记忆技术[1，2，18，20，21，23，26]。布尔方程系统为研究定点计算提供了一个有用的框架，因为µ-演算可以在这种设置中编码（例如，参见[1，5，21，23]）。 我们将提请注意布尔方程系统的一个片段，我们称之为分层方程系统。这些是特定的定点方程系统，其中变量散布在方程中，使得解的计算变得非常简单，并且可以优化为具有存储效率。我们提出了有效的技术来解决这样的系统。主要的新颖性是，我们exploit的特定结构的定点方程，大大提高了内存的使用。我们还研究了一般布尔方程组解的空间复杂性，证明了一个新的NL-困难性结果。这有助于理解求解布尔方程组所需的理论最小空间存储。事实证明，许多具有实际重要性的验证问题可以用布尔方程系统表示，这些布尔方程系统属于分层类。因此，我们的技术的一组应用程序的概述。为了本文的目的，我们还实现了该算法，并用它来解决一系列的协议验证问题。这项技术在这些最初的应用中取得了成功。本文的结构如下。在第2节中，我们将介绍布尔方程系统并解释关键概念。在第3节中，我们将讨论最先进的定点计算技术，并讨论其局限性。在第4节中，我们描述了如何用我们的技术解决分层布尔方程系统，并将这些想法结合到一个单一的有效程序中。在第五节中，我们证明了解不动点方程问题的NL-困难性。在第6节中，我们说明了许多验证问题可以用分层类中的方程组进行编码在第7节中，我们将介绍我们的解决方案技术在协议验证问题中的应用，以及两组基准测试的结果。第8节结束M. Keinänen/Electronic Notes in Theoretical Computer Science 133（2005）1751772布尔方程组我们将在本节中简要介绍布尔方程系统，并定义所需的概念。假设给定一个有限集合X ={x1，...，xn}的布尔变量和X中变量的线性序。然后，布尔方程系统定义如下。定义2.1布尔方程系统E是一个有序的标记定点方程E={σixi=αi}1≤i≤n其中σi∈{ν，μ}，xi∈ X，且αi=opi X其中opi∈{，}且X<$X。通常，假设方程的所有左边变量都是不同的。方程的顺序很重要，我们保持变量和它们的索引的顺序同步。我们假设一个空的disjunc- tion写为false，一个空的conjunction写为true。我们通常用字母来代表空布尔方程系统。我们说一个变量xi依赖于变量x j，如果方程σ ixi= α i的右边α i包含一个对x j的引用，或者包含一个对变量x k的引用，使得x k依赖于x j。布尔方程系统的语义为每个系统提供了唯一确定的解。接下来，我们将介绍语义 为此，我们首先需要引入一些符号。设O=（{0， 1}，，）是真值的两点格溶液将相对于环境v：X →O给出布尔方程系统中所有变量的意义让[]表示空环境，[xi：=a]将a赋值给xi的环境。对于具有不相交可变域的两个不同环境v和vJ，vvJ表示它们的并集。因此，例如[][xi：=a]=[xi：=a]=[xi：=a][]和[xi：=a][xj：=b]=[xj：=b][xi：=a]。右侧αi的含义定义很简单：[[ {x1，x2，. x n}]]v =[[ {x1，x2，. x n}]]v ={v（x1），v（x2），.， v（xn）}{v（x1），v（x2），.， v（xn）}然后，布尔方程组的解定义如下（类似的定义见例如：[2、14、21、23、26]）。定义2.2布尔方程组E的解[E]v相对于178M. Keinänen/Electronic Notes in Theoretical Computer Science 133（2005）175环境V归纳地定义为：[[]]v=[][[(σi xi=αi）E]]v=（[E]]v[xi：=a]）[xi：=a]哪里⎧好的[[αi]]（v[xi：=u]（[[E]]v[xi：=u]））如果σi=µa=0vu. [[αi]]（v[xi：=u]（[[E]]v[xi：=u]））如果σi=ν注意在上面的定义中，σi u.αi（u）表示函数αi在格O上的极值σ不动点。3解决方案技术和局限性在[21，5]中，有一些有用的原理可以求解布尔方程组（参见[21]中的引理6.2和引理6.3，或[5]中的命题1.4.7）。由于我们的证明和技术基本上是基于这些性质，我们在这里陈述它们。引理3.1设E1和E2为布尔方程组，σ x = α为定点方程。 设αJ与α完全相同，只是当σ=ν时，α中所有出现的x都用true代替，当σ =μ时，用false代替。则E1（σx =α）E2和E1（σx =αJ）E2有相同的解.引理3.2设E1，E2和E3是布尔方程组.设σ1x1=α，σ1x1= αJ和σ2x2= β是不动点方程，其中αJ与α完全相同，只是x2的所有出现都用下式代替β。然后和有相同的解决方案。E1（σ1x1=α）E2（σ2x2=β）E3E1（σ1x1=αJ）E2（σ2x2=β）E3这些引理允许用非常类似于线性代数中高斯消去法的方法来求解固定点方程。 一般来说，这种方法不太适合求解大型方程组，因为它的指数时间最坏情况的复杂性（见例如。[21]）。用于固定点计算的最先进算法通常仅在底层系统的交替深度中是指数的，如[1，20]中的算法。M. Keinänen/Electronic Notes in Theoretical Computer Science 133（2005）175179此外，有许多类的方程系统，其中存在非常有效的多项式时间算法，例如见[1，4，6，11，12，14]。然而，一个仍然存在的问题是这些算法的内存消耗.由于显式状态模型检验中的状态爆炸问题，即使相对简单的验证问题也可能导致系统具有数百万个固定点方程，这些方程可能变得天文数字大小。由于固定点计算的典型方法依赖于方程组的标准表示[2]，因此所有方程都需要同时保存也就是说，当以图形的形式显式存储固定点方程时（如[1，4，6，11，12，14，20，26]），内存通常会被浪费，因为在固定点计算终止时，内存既保存了方程的图形解码，又保存了所有变量的解的表示。相反，我们希望在不求助于方程的标准表示的情况下确定给定定点方程组的解，并且更喜欢以最小化数据结构的构造和检查的方式找到解。在下一节中，我们将提请注意一类有限的布尔定点方程组，它允许以节省内存的方式计算它们的解。也就是说，我们确定了一类系统，其解决方案可以找到，而不诉诸于标准表示解码方程系统。这是通过对变量如何散布在方程中引入限制来实现的。然后，我们将表明，事先知道系统是这样的形式，允许每个方程只使用一位存储，这使得类从实用的角度来看很有吸引力。4基于分层的为了获得一个快速，记忆效率高的解决方案技术布尔方程组，我们引入分层的概念。这个概念可以追溯到[3，9]，并且在Datasheet的上下文中是众所周知的。最近，这一概念在[24]中被相继采用，但在布尔方程的设置中，这一限制似乎是新的。为了表达布尔方程系统中的分层，我们定义了一个函数秩：X →{1，2，. }，它为每个变量分配一个秩数。基于这样的映射，方程系统中的分层定义如下。定义4.1设E是布尔方程组E={σi xi=αi}1≤i≤n。我们称系统E相对于映射秩分层：X → {1，2，.，n}180M. Keinänen/Electronic Notes in Theoretical Computer Science 133（2005）175我的(i) 映射秩是双射的，并且(ii) 对所有的1≤i≤n，xi只依赖于变量xj∈ X，且秩（xj）≤rank（xi）.布尔方程系统被分层的优点是其解的计算变得非常简单，并且可以被优化为具有存储效率。本文提出了一种简单而有效的求解这种布尔方程组的方法我们的技术的现金价值的一部分是，它很容易实现，以提高内存消耗，而不增加运行时开销。我们的算法是基于这样的观察，即一个分层布尔方程系统的所有方程都可以一次求解一个，从左边变量秩最低的方程开始。更准确地说，我们的算法基于以下结果。引理4.2设E={σ i x i= α i}1≤i≤n是一个按r.t.分层的系统。秩：X → {1，2，.，n}。 设σ i x i= α i是E的方程，其中op i=.则以下是等价的：(i) xi的解为0(ii) <$xj∈αi使得：(a) σi=μ且xj=xi;或(b) rank（xj） 1.我们构造一系列方程：µx1=µx2={xi：（1，i）∈E}{xi：（2，i）∈E}.µxn−1=.{xi：（n−1，i）∈E}v xn={xn}然后直接验证布尔方程系统的结果实例的解使得x1具有值1 i，并且G中存在从节点1到节点n的路径。此外，从G到不动点方程的构造显然是对数空间缩减。Q注意，在上面的证明中构造的布尔方程系统是析取的，并且没有符号不同的相互依赖的变量，即，所得到的系统是无选择的。因此，求解布尔方程组的问题仍然是NL-困难的，即使是对于析取的、无交替的系统.6应用定点分析技术可用于解决各种验证问题。该方法的总体思路可概括如下。一般程序包括首先从验证问题生成固定点等式，然后使用M. Keinänen/Electronic Notes in Theoretical Computer Science 133（2005）175185合适求解器。这两个阶段显然是相互独立的，但事先知道验证问题会导致分层方程系统，可以调整求解器，例如第4节中讨论的。现在我们给出一些验证问题的例子，这些问题可以被编码为分层布尔方程系统，因此可以用我们的技术有效地解决。6.1模型检测非循环标记转移系统上模态微演算的模型检验问题归结为计算分层布尔方程系统的解的任务。在[22]中讨论了各种重要的应用领域，例如，运行时监控和跟踪分析。使用标准的翻译，所有应用于任何非循环转换系统的µ-演算公式都会导致分层布尔方程系统。定理6.1如果标号转移系统是非循环的，并且使用[5，21]中 的 编 码 ，则μ -演算模型检验问题表示为布尔方程系统是分层的。一旦我们意识到这一点，我们就得到了一种用于非循环模型上的全μ-演算逻辑的模型检查技术，它在最坏情况下的时间复杂度方面比[22]中的技术有稍微好的估计。如果应用于非循环模型上的μ-演算的模型检查，我们的方法避免了令人不快的公式大小的二次爆炸然而，[22]中的算法的优点之一是它适用于一种需求驱动的方式，这似乎并不容易实现与我们的做法。考虑到我们的分辨率算法是全局的，而不是[22]的局部方法此外，对于不包含定点运算符的µ-calculus的语法片段，我们有以下内容：定理6.2如果采用文[ 5，23 ]中的编码，则Hennessy-Milner逻辑模型检验问题表示为布尔方程组是分层的。6.2等价性/前序检查除了它们在模型检验中的效用之外，分层布尔方程系统也出现在等价性和前序检验的上下文中。例如，给定两个标号迁移系统，只要其中至少有一个是非循环的，则与强互模拟及其预序有关的布尔方程系统186M. Keinänen/Electronic Notes in Theoretical Computer Science 133（2005）175变得有层次。实际上，如在[23]中所观察到的，在非循环标记转移系统上的强双模拟的编码这导致以下结果。定理6.3如果标号转移系统是非循环的并且使用[ 18 ]中的编码，则模拟等价和互模拟等价作为布尔方程系统的表示是分层的。7实验结果也许，比较布尔方程系统求解器实现效率的最佳方法在本节中，我们提供了来自实际应用的方程系统基准的初始实验结果。为了评估我们的算法的实际性能，我们已经实现了它在C编程语言。所有测试都是在1.0Ghz AMD Athlon上完成的，该系统运行Linux，主内存充足。报告的时间是求解器运行3次找到解的平均时间，由/usr/bin/time命令报告。作为基准测试，我们使用来自[8]的协议模型，使用µCRL-工具集实例化[7]，并转换为布尔方程系统。第一个验证问题包括对一系列规模不断增加的分布式领导者选举协议模型的微演算公式第二系列的实验处理的问题，检查模拟等价性之间的领导选举协议和它的抽象7.1模型检验DKR领导选举协议简而言之，Dolev-Klawe-Rodeh（DKR）领导人选举协议[10]由连接在环中的n个政党组成。 这些政党交换信息，在有限数量的信息中，具有最高身份的一方通知其他人成为领导者。该协议在[13]中建模，我们需要检查的期望的安全属性是 此规格表示为 下面的µ-演算公式（1）(1)V X. （[true] X[leader]φ）其中子公式φ是（2）：(2)是的。（[true]Y[leader]false）公式（1）在所有协议模型上都是全局正确的。M. Keinänen/Electronic Notes in Theoretical Computer Science 133（2005）175187⎪基准工具时间（秒）记忆（B）DKR（5）cbess 0的情况。0142 232|：|:斯贝斯0的情况。016 9327 192（%）（0）(16（4）中国（6）cbess 0的情况。05210 088|：|:斯贝斯0的情况。0431 63636 714（%）（80.0）(15（1）DKR（7）cbess 0的情况。241 054 536|：|:斯贝斯0的情况。21146 052190 618（%）(87（5）(13（8）DKR（8）cbess 0的情况。802 115 304|：|:斯贝斯0的情况。70425 388632 284（%）(87（5）(20（1）DKR（9）cbess四、1716 537 664|：|:斯贝斯3 .第三章。641 943 4283 162 712（%）(87（3）（11，8）图二.布尔方程系统求解器在模型检验基准数据上的总求解时间和内存消耗。上述验证问题可以直接形式化为布尔方程系统，促使我们将其编码如下：v xs=xsj⎫公司简介⎬sJ∈ n（t，188M. Keinänen/Electronic Notes in Theoretical Computer Science 133（2005）175|s−→ s}{s |s −→ss）SJ∈ <$（l，s）S∈S⎪ν ys=法尔塞河公司简介sJ∈ <$（l，s）sJ∈ <$（t，s）这里，n（l，s）：={sJ领导人J且n（t，s）：=JiJ和i∈ A}。乍一看，这些方程似乎不是一个分层的布尔方程，系统，但由于从[13]中的高级规范实例化的具体标记转移系统是非循环的，所有方程都将变得分层。然后，我们评估了我们的算法的性能，通过测量解决方案的时间和比较内存使用的另一个布尔方程系统求解器M. Keinänen/Electronic Notes in Theoretical Computer Science 133（2005）175189（14）。虽然算法从[14]（见图。[14]中的1）被设计用于求解可能包含交替固定点的系统，它保证对分层布尔系统表现出线性时间性能。这两种算法之间的本质区别在于，来自[14]的算法依赖于用于解码方程组的标准表示[2]，这允许进行公平的比较。结果在图2中给出，其中列为：• 基准：具有n个政党的DKR（n）DKR领导人选举协议模型，以及|E|对应于验证问题的布尔方程系统的大小。• 工具：cbess来自[14]的合取布尔方程系统的求解器;sbess图1中的分层布尔方程系统求解器;行（%）显示获得的性能改进;括号中的数字表示新算法的性能测量值占[14]中算法性能的百分比• 时间（秒）：求解方程组所需的时间（秒）。• Mem（B）：求解方程组所需的内存字节数根据实验结果，可以得出以下结论。我们的算法在时间上优于[14]中的算法。改进的程度范围高达约20%的适度加速。此外，我们得到相当大的减少内存消耗时，我们的算法被用来代替[14]。 与[14]中的技术相比，使用图1中的求解器总是增加内存节省，高达约88%。这一结果是由于我们的算法利用了布尔方程系统的特定分层结构，以避免存储所有方程。它不是用标准表示法[2]来表示方程组，而是在内存中只保存一个涉及到的变量的解的一位。7.2模拟检查DKR领导选举协议第二个应用程序，我们考虑处理的问题，模拟检查的DKR领导选举协议。第二个实验将每个领导选举协议LTS模模拟关系与一个更抽象的LTS进行比较，验证了简化的LTS是对具体协议LTS的正确抽象。我们使用[18]中的编码来表示具体和抽象LTS之间的模拟等价性。因此，相应的布尔方程系统的所有方程都将分层，因为LTS190M. Keinänen/Electronic Notes in Theoretical Computer Science 133（2005）175基准工具时间（秒）记忆（B）DKR（5）cbess 0的情况。0124 580|：|:斯贝斯0的情况。0014 2323 553（%）（0）（57，9）中国（6）cbess 0的情况。03120 860|：|:斯贝斯0的情况。0173 45618 359（%）（三十三，三）(60（8）DKR（7）cbess 0的情况。11600 292|：|:斯贝斯0的情况。09381 26495 311（%）(81（8） (63（5）DKR（8）cbess 0的情况。351 902 628|：|:斯贝斯0的情况。301 264 596316 144（%）(85（7） (66（5）DKR（9）cbess1 .一、709 220 524|：|:斯贝斯1 .一、496 325 4441 581 356（%）(87（6） (68（6）图三.布尔方程系统求解器在模拟检查基准数据上的总求解时间和内存消耗。在[13]中从高级规范实例化的是非循环的。对于每个实验，图中的表格图3显示了使用图1和[14]中的算法获得的测量值2）的情况。从第二个例子中得出的结论是，在所有实验中，内存使用都得到了M. Keinänen/Electronic Notes in Theoretical Computer Science 133（2005）175191实质性的改善;减少了大约58%。8结论本文提出了一种计算限制分层布尔方程组解的方法。我们的方法包括一个快速，内存效率的过程，只需要一个单一的通过任何192M. Keinänen/Electronic Notes in Theoretical Computer Science 133（2005）175给定的分层布尔方程系统。我们证明了我们的技术的正确性和复杂性。此外，我们还研究了求解布尔方程组的空间复杂性。我们证明了求解布尔方程组的空间复杂度仍然是NL-困难的，即使是对于相对简单的一类定点方程。此外，我们已经证明，分层布尔方程系统提供了一个合适的框架来表达有限状态并发系统上的许多验证问题，例如μ-演算的模型检查以及非循环模型上的我们已经证明了我们的新算法的性能，使用领导者选举协议验证的例子。我们的技术的实施已被证明是有效的和可扩展的。基准测试显示，显著节省了内存，并略微缩短了求解时间。引用[1] H.R.安徒生模型检查和布尔图。理论计算机科学，126：3[2] H.R.安德森湾维尔高文使用不动点反演的行为关系和模态断言的有效检查。在Proceedings ofConf. on Computer Aided Verification，Lecture Notes on Computer Science 939，pages 142[3] K. Apt，H. Blair和A.沃克声明式编程的理论。 演绎数据库和逻辑编程的基础，第89-149页[4] A. Arnold 和P. Crubille 。一 种求解 过渡系统 上不动 点方程 的线性 时间算法 。InformationProcessing Letters，29：57[5] A. Arnold和D.尼温斯基微微积分的基础知识。逻辑与数学基础研究，第146卷，爱思唯尔，2001年。[6] G. Bhat和R.克里夫兰有效的局部模型检查，用于模态微演算的片段。在Proceedings of theInternational Conference on Tools and Algorithms for the Construction and Analysis ofSystems，Lecture Notes in Computer Science 1055，pages 107[7] S. 布洛姆，W. Fokkink，J.F. 格鲁特岛 van Langevelde，B. Lisser和J. van de Pol. µCRL：用于分析代数规范的工具集。在Proceedings of Conf. on Computer Aided Verification，LectureNotes in Computer Science 2102，pages 250[8] S. Blom和J. van de Pol.通过证明连续性来减少状态空间。 在Proceedings of Conf. on ComputerAided Verification，Lecture Notes on Computer Science 2404，pages 596[9] A. Chandra 和 D. 哈 雷 尔 关 系 数 据 库 的 可 计 算 查 询 。 Journal of Computer and SystemSciences，21（2）：156[10] D. Dolew，M. Klawe和M.罗德一个O（n log n）时间复杂度的算法。Journal of Algorithms，3（3）：245[11] E.A.爱默生角Jutla和A.P. Sistla。 关于μ演算片段的模型检验。 第五届计算机辅助验证国际会议论文集，计算机科学讲义697，第385-396页，Springer Verlag，1993年M. Keinänen/Electronic Notes in Theoretical Computer Science 133（2005）175193[12] E.A.爱默生角Jutla和A.P. Sistla。关于μ-演算及其片段的模型检验。理论计算机科学，258：491[13] L. Fredlund，J.F. Groote和H.科弗在进程代数中的领导者选举协议的形式验证。理论计算机科学，177：459[14] J.F. 我的爷爷和奶奶。 好的。 求解D是具有交替不动点的约束/共约束BooleanEquaton系统。在 Proceedings of the 10th International Conference on Tools and Algorithms for theConstruction and Analysis of Systems，Lecture Notes in Computer Science 2988，pages436[15] N. Jones，Y. Lien和W. 激光 不确定性日志空间的新问题完成。Mathematical Systems Theory，10：1-17，1976.[16] M.尤金斯基在对等博弈中，决定赢家的是UP-U-UP。Information Processing Letters，68：119[17] D.浩善关于命题μ-演算的结果。理论计算机科学，27：333-354，1983。[18] K.拉森有效的局部正确性检查。在Proceedings of Conf. on Computer Aided Verification，Lecture Notes on Computer Science 663，pages 30[19] X. Liu和S.A.斯莫尔卡最小不动点的简单线性时间算法。在Proceedings of the 26th InternationalConference on Automata ， Languages ， and Programming ， Lecture Notes in ComputerScience 1443，pages 53[20] X. Liu，C.R. Ramakrishnan和S.A.斯莫尔卡交错不动点的完全局部有效计算。 第四届国际工具会议论文集和用于系统的构造和分析的算法，计算机科学讲义1384，第5-19页，SpringerVerlag，1998。[21] A.疯了使用布尔方程系统验证模态特性。博士论文，慕尼黑工业大学，1997年。[22] R.马提斯库非循环标号迁移系统模态Mu演算的局部模型检验。在Proceedings of the 8thInternational Conference on Tools and Algorithms for the Construction and Analysis ofSystems，Lecture Notes in Computer Science 2280，pages 281[23] R.马提斯库一个通用的在飞行中求解器交替自由布尔方程系统。在Proceedings of the 9thInternational Conference on Tools and Algorithms for the Construction and Analysis ofSystems，Lecture Notes in Computer Science 2619，pages 81[24] F. Nielson，H. Nielson，H.孙，M。布赫霍尔茨河Hansen，H. Pilegaard和H. 赛德尔 简洁的求解器套件。在Proceedings of the 10th Conference on Tools and Algorithms for the Constructionand Analysis of Systems，Lecture Notes in Computer Science 2988，pages 251[25] C.帕帕迪米特里乌计算复杂性。Addison-Wesley，1994年。[26] B. Vergauwen和J. Lewi。单个和交替布尔方程组的有效局部正确性检验。在Proceedings of the21st Intern