抽象规则树模型检测及其在系统形式验证中的应用研究——理论计算机科学电子笔记

理论计算机科学电子笔记149（2006）37-48www.elsevier.com/locate/entcs抽象规则树模型检测Ahmed Bouajjani，Peter Habermehl彼得·哈伯梅尔AhmedBouajjani，Peter HabermehlLIAFA，University Paris 7，Case 7014，2，place Jussieu，F-75251 Paris Cedex 05，FranceAdamRogalewicz，Toma′sVojnar3，4FIT，BrnoUniversityofTechnology，Bozetechova2，CZ-61266，Brno，CzechRepublic摘要规则（树）模型检验（RMC）是一种有前途的通用方法，用于形式化验证无限状态系统。它将系统的配置编码为合适的alpha- bet上的单词或树，可能是作为有限单词或树自动机的有限配置集，以及作为有限单词或树转换器检查可达性集，然后计算一个重复的应用程序的传感器上的自动机表示目前已知的一组可达配置。为了便于RMC的终止，已经提出了各种加速方案。其中之一是RMC与抽象-检查-细化范式的结合，ARMC最初只被提出用于词自动机和转换器，因此用于处理具有线性（或易于线性化）结构的系统。在本文中，我们提出了ARMC的一个推广，以处理在许多建模和验证环境中自然出现的树。特别是，我们首先提出了树自动机的抽象，基于折叠它们的状态，具有一个相等的树语言，直到某个有界高度。然后，我们提出了一个抽象的基础上崩溃的状态有一个非空的交集（从而最后，我们展示了几个例子，我们提出的方法给我们非常令人鼓舞的验证结果。关键词：形式验证，无限状态系统，自动机理论，树自动机，常规模型检查，抽象1由法国安全部提供（ACIprojectSecur i t′eInforrmataiquee）。2电子邮件：abou@liafa.jussieu.fr，Peter. liafa.jussieu.fr3由捷克赠款机构项目102/05/H 050、102/03/D211和102/04/0780支助。4电子邮件：rogalew@fit.vutbr.cz，vojnar@fit.vutbr.cz1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.11.01538A. Bouajjani等人/理论计算机科学电子笔记149（2006）371引言常规模型检验[14，4，5]是一种形式化验证无限状态系统的通用方法系统的配置被编码为有限字母表上的有限单词，而转换被编码为单词上的关系。然后，自然地，可以使用词自动机来表示和操纵（无限）配置集，并且使用（{ε}）×（{ε}）上的转换器来表示转换关系。为了验证安全性，可达性分析是通过计算transducers的传递闭包或transducers的迭代自动机的图像来执行的。 终止通常不能保证，因此已经提出了各种加速方法。作为最成功的加速方法之一，同时也作为一种处理表示配置的自动机中状态空间爆炸问题的，抽象正则模型检查（ARMC）[8]最近被引入。 这种通用方法在常规模型检查中使用了众所周知的抽象-检查-细化范式。抽象被定义在表示配置的词自动机上。然后，进行保证终止的抽象可达性分析。对于遇到虚假反例的情况，定义了抽象的适当改进。通过这种方式，计算出一个足够详细的抽象，以回答特定的验证问题。ARMC已经成功地应用于许多不同的系统，如计数器自动机，参数化进程网络和列表程序[7]。为了处理线性（或易于线性化）结构以外的其他结构，已经提出了规则树模型检查[14，6，1，19，2]而不是单词，配置是有限树，而不是单词自动机，树自动机用于表示配置集。然后，树换能器对转换进行建模。像在word case中一样，存在几种用于可达性分析的加速方法。树状结构非常常见，并且在许多建模和验证上下文中自然出现。例如，在参数化树网络的情况下，任意高度的标记树表示网络的配置：每个进程都是树的一个节点，标签是其控制状态。树木也是自然生长的，例如，作为多线程递归程序的配置表示[12，17]，作为堆的表示结构[15]，或者当表示结构化数据时，如XML文档[9]。在本文中，我们扩展了ARMC的框架，从词到树。我们使用自下而上的树自动机和传感器。像在ARMC中一样，我们在自动机的某些有限域中使用抽象定点计算抽象的fix-A. Bouajjani等人/理论计算机科学电子笔记149（2006）3739点计算总是终止并提供可达性集合的过近似。为了实现这一点，我们定义了一种技术，该技术系统地将任何树自动机M映射到一个树自动机MJ，main，使得MJ识别M的语言的超集。 的情况计算的过近似太粗糙，并且是伪计数器-检测到的例子，我们给出了有效的原则，允许抽象被细化，使新的抽象计算不会遇到相同的反例。我们，特别是，提出了两个抽象的树自动机。 与ARMC类似，它们都是基于根据适当的等价关系折叠自动机状态。第一个是基于考虑两个树自动机状态等价，如果它们的树的语言达到一定的固定高度是相等的。第二个抽象由一组正则谓词语言LP定义。我们认为树自动机M的状态q“然后，如果两个状态满足相同的谓词，则它们是等价的。我们已经使用Timbuk [13]树自动机库在原型工具中实现了上述抽象。我们已经在各种参数化树网络协议上使用该工具进行了实验。结果非常令人满意，并且与其他工具相比非常好，这为我们进一步开发该方法提供了很好的基础和动力。2正则树语言和转换器本节简要介绍常规树语言和转换器。可以找到更详细的描述，例如，在[10，11]中。字母表是一组有限的符号。如果存在秩函数ρ：ρ→N，则称ρ为秩。对于每个k∈N，k是所有秩为k的符号的集合。0的符号称为常量。设χ是一个可枚举的称为变量的符号集。T[χ]表示在χ和χ上的项的集合。该集合T []由T确定，并且它的元素被称为grr r roundterms。如果每个变量在t中最多出现一次，则来自T [ χ ]的项t称为线性项。T[χ]中的项可以被看作是树叶被标记为常数和变量，并且具有k个儿子的每个节点被标记为来自k的符号。排序字母表上的自下而上树自动机是元组A=（Q，F，δ），其中Q是有限状态集，F，Q是最终状态集，δ是以下类型的转换集：（i）f（q1，.，qn）→δq，（ii）a→δq，（iii）q→δQJ其中a∈ φ 0，f∈ φ n，q，QJ，q1，.，qn∈Q.注意：下面，我们将自底向上的树自动机简称为树自动机。40A. Bouajjani等人/理论计算机科学电子笔记149（2006）37设t是一个基项。树自动机A在t上的运行定义如下。首先，叶子被标记为状态。 如果一个叶子是一个符号a∈δ0，并且有一个规则a→δq∈δ，则叶子被标记为q。 内部节点若存在规则f（q1，q2，.，qk）→δq∈δ，并且节点的第一个子具有状态标签q1，第二个子具有状态标签q2，.，和最后一一个qk。q→δqJ类型的规则称为ε-步骤，允许我们将状态标签从q改为qJ。如果顶部符号标记有集合中的状态，对于最终状态F，项t被自动机A接受。树自动机A接受的一组基项被称为正则树语言，记为L（A）。设A=（Q，Q，F，δ）是一个树自动机，q∈Q是一个状态，则我们定义状态q-L（A，q）-的由树自动机Aq=（Q，n，{q}，δ）接受的基项的集合语言L≤n（A，q）定义为集合{t ∈ L（A，q）|height（t）≤n}。自下而上树转换器是元组τ=（Q，τ，Δ，F，δ），其中Q是 f是状态的有限集合，F是最终状态的集合，f是输入排名字母表，F是输出排名字母表，并且δ是前一个字母表的转换规则的集合：（i）f（q1（x1）， . . ，qn（xn））→δq（u），u∈T<$J[{x1， . . ，xn}]，(ii) q（x）→δqJ（u），u∈T<$J[{x}]，和（iii） a→δq（u），u∈T<$J当rea∈θ0时，f∈n，x，x1，.，xn∈χ，并且q，QJ，q1，.，qn∈ Q.注：在下文中，我们将自下而上的树型换能器简称为树型换能器。我们总是使用树型传感器，其中<$j =<$J。树转换器τ在基项t上的运行类似于树自动机在该项上的运行。首先，使用（iii）类型的规则。如果一个叶子用符号a标记，并且存在规则a→δq（u）∈δ，则叶子被项u代替，并被状态q标记。 如果一个节点由一个符号标记f，存在规则f（q1（x1），q2（x2），. ，qn（xn））→δq（u）∈ δ，节点的第一个子树的状态标号为q1，第二个子树的状态标号为q2，. . ，并且最后一个qn，则符号f和给定节点的所有子树被替换为到规则的右边，变量为x1，...，xn由相应的左手侧子树代替。状态标签q被分配给新树。类型（ii）的规则称为ε-步。它们允许我们用规则的右手边替换一个q状态标记的树，并分配状态标签。qJ到这个新树，其中规则中的变量x如果树的根被处理并且由来自F的状态标记，则换能器的运行是成功的。树转换器是线性的，如果其规则的所有右侧都是线性的（没有变量出现超过一次）。线性自底向上树变换器类在复合下是封闭的。如果树转换器不修改输入树的结构，而只是改变其节点的标签，则称为结构保留（或重新标记）通过滥用符号，我们认为-A. Bouajjani等人/理论计算机科学电子笔记149（2006）3741δi=0时使传感器灵敏 τ与关系{（t，tJ） ∈T<$×T<$ | t → ∗q (tJ) for有q∈F}。 对于一个集合L和一个关系R×T，我们记R（L）为集合{w ∈ T|<$wJ∈ L：（wJ，w）∈ R}且R−1（L）是集合{w∈T}|<$wJ∈L：（w，wJ）∈R}.如果τ是一个线性树转换器，L是一个正则树语言，那么集合τ（L）和τ−1（L）是正则的，并且是等价可构造的[11，10]。设id<$T<$×T<$是恒等关系，而k是关系的合成我们递归地定义关系τ 0= id，τ i+1= τ τ i和τ = τ ∞τ i。下面，我们假设id<$τ意味着对于所有i≥0，τi <$τi+13抽象规则树模型检测在本节中，我们首先回顾常规树模型检查的概念。然后，我们通过定义树自动机上的几个抽象来介绍抽象正则树模型检测。3.1常规树模型检查正则树模型检查[1，6，14]是正则模型检查[5]对树的推广 系统的配置被编码为一个项（树），一个排名字母表和一组这样的条款作为一个定期树自动机。系统的过渡关系被编码为线性树变换器τ。 我们给出了一个树自动机Init编码的初始状态集。对于安全属性，给出了一组坏状态（由树自动机Bad表示）。然后，基本的验证问题在于决定是否τ（L（Init））L（Bad）=（1）这个问题通常是不可判定的（因为τ（L（Init））的迭代计算不会终止 ） 。 已 经 提 出了 几 种 方 法 [1 ， 2 ， 6] 来 计 算 某 些 情 况 下 的 τ 或 τ （ L（Init））。这些技术都计算精确的集合或关系。我们通过以下方式解决模型检查问题：将 抽 象 正 则 模 型 检 验 方 法 [8] 推 广 到 树 自 动 机 。 该 方 法 计 算 τ （ L（Init））的过近似，其精度刚好足以安全地解决验证问题（1）。3.2抽象规则树模型检测抽象规则树模型检测（ARTMC）将规则树模型检测与自动抽象相结合。ARTMC的主要思想是将抽象正则模型检查[8]一般化为正则树语言。42A. Bouajjani等人/理论计算机科学电子笔记149（2006）37αααααα为此，为词自动机设计的抽象技术必须适应树自动机。我们首先回顾抽象规则模型检查的基本框架（这里直接针对树）。设M是一个排序字母表，M是上所有树自动机的集合，- 是的我们将抽 象 函 数 定 义 为 映 射 α ： M→A ， 其 中A∈M∈M∈L （ M ） <$L （ α（M））.抽象αJ称为抽象α的精化，如果<$M∈M<$：L（αJ（M））<$L（α（M））。给定树转换器τ和抽象α，我们定义映射τα：M→M为<$M∈M<$：τα（M）=τ<$（α（M））其中τ<$（M）是描述语言τ（L（M））。一个抽象α是有限值域，如果集合A是有限的。假设Init是表示初始配置集合的树自动机，Bad是表示坏配置集合的树自动机现在，我们可以迭代地计算序列（τi（Init））i≥0。既然我们假设如果α是无穷的，则存在k≥0使得τk+1（Init）=τk（初始化）。α的定义意味着L（τk（Init））<$τ（L（Init））。这意味α α在有限步数中，我们可以计算可达集τ（L（Init））的过近似。如果L（τk（Init））<$L（Bad）=0，则证明问题（1）为一个问题，答 案 否 则 ， 问 题 （ 1 ） 的 答 案 不 一 定 是 否 定 的 ， 因 为 在 计 算 τ（ L（Init））的过程中，抽象α可能会引入导致L（Bad）的额外行为。让我们研究一下这个案例。假设τ（Init）L（Bad）/=τ，这意味着它是一条简单的双向路径：Init，τα（Init），τ2（Init），···τn−1（Init），τn（Init）（2）α α αsuchthatL（τn（Init））<$L（Bad）/=<$. 我们通过计算来分析这一点集合Xn=L（τn（Init））<$L（Bad），并且对于每个k≥0，Xk=L（τk（Init））<$α ατ−1（Xk+1）. 我们可以这样做：（i）eirX0=L（Init）<$（τ−1）n（Xn）/=∞，这意味着问题（1）有一个否定的答案，或者（ii）有一个k≥0的xk=∞，这意味着由于α太粗糙，所以系统路径（2）实际上是一个虚假的反例在在最后一种情况下，我们需要对过程进行优化。因此，我们的方法是基于抽象模式的定义，允许计算（自动）可精化抽象的家族。3.3基于自动机状态等价下面，我们讨论两种可能的树自动机抽象模式，它们基于树自动机状态等价。首先，树自动机状态被划分成几个等价类的等价关系。然后A. Bouajjani等人/理论计算机科学电子笔记149（2006）3743MMMMMMM抽象函数将来自每个等价类的状态折叠成一个状态。形式上，树自动机状态等价模式E被定义如下：对于每个树自动机M=（Q，F，δ）∈M<$，等价关系<$E<$Q×Q被分配。 则自动机抽象函数αE对应于对于抽象模式E定义为<$M∈M<$：αE（M）=M/<$E。如果αE是无穷的，我们称之为E无穷（即存在有限个等价类）。 我们通过制造“E”来提炼“E” 菲纳。3.4基于有限高度我们现在提出了基于比较自动机状态wrt来定义自动机状态等价模式的可能性他们语言中的某个有界部分。抽象模式Hn是[8]中为词自动机提出的类似模式的推广。这个模式定义树自动机M的两个状态是等价的，如果它们的语言直到给定的高度n是相同的。形式上，对于树自动机M=（Q，F，δ），Hn定义状态等价性作为等价物n使得<$q1，q2∈Q：q1<$nq2优惠L≤n（M，q1）=L≤n（M，q2）.树的最大高度为n的语言是有限的，因此这种抽象是有限范围的。抽象的细化可以通过增加n的值来完成。抽象模式Hn可以以与树自动机的最小化类似的方式实现。在n次迭代之后，仅停止最小化过程的主循环3.5基于谓词语言的抽象接下来，我们介绍一个基于谓词的抽象模式PP，它受到基于谓词的词抽象的启发[8]。设P ={P1，P2，.，Pn}是谓词的集合。每个谓词P∈ P是一个树语言，由树自动机表示。设M=（Q，Q，F，δ）是树自动机，则两个状态q1，q2∈Q等价，如果它们的语言L（M，q1）和L（M，q2）与集合P中的同一谓词子集有非空交集.形式上，对于一个自动机M=（Q，F，δ），PP定义状态等价-alence作为等价物使得<$q1，q2∈Q：q1<$Pq2惠（qP∈ P：L（P）L（M，q1）优惠L（P）优惠L（M，q2））。显然，由于P是有限的，只有有限个子集的P表示给定状态与之有非空交集的谓词，PP是无穷的。 可以通过添加新谓词来44A. Bouajjani等人/理论计算机科学电子笔记149（2006）37MMPM在集合P中。下面的定理表明，在分析第3节中出现的伪反例（回想一下，X k = X k）时，我们可以通过用表示X k +1的树自动机的所有状态的语言来扩展谓词集P来消除伪反例。二、定理3.1设任意两个树自动机M=（QM，M，FM，δM），X=（QX，λ，FX，δX）和Ps的预处理的有限集。t. < $qX∈QX：L（X，qX）=L（P）. 如果L（M）<$L（X）=<$，则L（αPP（M））<$L（X）=我也是。证据 这个证明是文[8]关于词自动机的证明的推广。我们用反证法证明了这个定理。 Sup poseL（αPP（M））<$L（X）<$. Lett∈L（αPP（M））<$L（X）. 当它由αPP（M）所接受时，我们允许它在等于WRT的状态之间执行一定数量的P-在接受t的子树并得到某个q∈QM后，允许M跳到任何qJ∈QM使得q <$PqJ并从那里(with或者没有进一步的跳跃）。设i >0是从L（αP（M））<$L（X）在M中接受一棵树所需的最小跳跃数，TJ是这样一棵树。当我们观察M中tJ的接受度（允许一些跳跃）时，我们可以确定tJ的最大子树，这些子树可以在没有跳跃的情况下被接受-在最坏的情况下，它们只是叶子。让我们选取其中任何一个子树。这样的子树t1是在某个q1中接受，M从q1跳到某个q2，继续接受其余的输入。设t1在某个qX∈QX中可接受.设t1∈L（M，q1），L（M，q1）<$L（P）<$，对于P∈ P，其中L（P）= L（X，qX）. 此外，由于q1pq2，L（M，q2）<$L（P）/= 0. 这存在t2∈L（P）使得t2∈L（M，q2）和t2∈L（X，qX）.然而，这意味着我们从t j得到的树tJJ通过用t 2替换其子树t1而得到，并且t显然长到L（αPP（M））<$L（X）可以在M中接受i− 1个跳跃，这与i是所需的最小跳跃数的假设相矛盾。Q自动机Mwrt的抽象。基于谓词语言PP的状态等价可以被实现为通过谓词标记M的每个状态，其语言与该谓词具有非空交集，然后用等价标记来折叠状态。这里，让我们强调，当细化PP时，没有必要存储每个新引入的谓词对应于Xk+1的状态，然后执行la-分别为它们鸣钟。我们可以只保留Xk+1，然后不只是用Xk+1，而是用它的每个状态来进行标记。此外，这种标记可以通过同时运行M和Xk+1来实现，这对应于所有谓词的有效同时标记A. Bouajjani等人/理论计算机科学电子笔记149（2006）3745包含在Xk+1中。4使用ARTMC的为了能够实际评估所提出的方法的ARTMC，我们已经实现了他们的原型工具。我们的原型工具基于用Ocaml编写的Timbuk库[13]。Timbuk为我们提供了ARTMC中所需的树自动机上的基本操作（如并、交、补等）。然而，我们不得不扩展Timbuk，支持树传感器。我们增加了两个实现的树transducers-a更简单，更有效的结构保持transducers和更复杂的一般换能器。后一种实现方式利用了将树换能器分解为三个不太复杂的换能器，如[11]中所述。对于任何采油树传感器，都可以自动执行此分解。我们已经使用文献[14，3，1，2]中引用的参数化树形网络在几个协议示例上测试了我们的验证方法，其中覆盖所有可能的参数值的必要性导致处理有限状态空间：• 简单令牌协议。令牌在树形网络中从叶子传递到根。我们检查令牌不会消失或复制。• 双向令牌协议。类似于前面的例子，但是我们允许令牌向上和向下传递• 渗滤液方案。处理器的树形网络计算出现在叶节点中的布尔值的对数析取。我们检查计算值是否总是正确的。• 树仲裁协议。一个树形网络被用来实现离开处理器之间的互斥。进入临界区的请求被向上传播，直到找到一个节点，该节点具有允许进入临界区的令牌，或者知道令牌在哪里（因为它将令牌授予了其子节点之一）。具有令牌的节点总是可以向上发送令牌或将其授予其任何子节点。我们检查互斥属性。• 领导人选举协议。一组处理器中的一个将被选为领导者，并且树形网络用于此目的。叶子分为候选人和非候选人。关于候选者存在的信息被向上传播。在随后的向下阶段中，非确定性地选择从根通向候选节点之一的路径，并且因此建立领导者我们检查一下46A. Bouajjani等人/理论计算机科学电子笔记149（2006）37只有一个领导人被选中。上述所有例子都适用于固定结构的树形网络。为了测试我们的方法与非结构保持系统的工作能力，我们考虑了一个简单的广播协议。在该协议中，根节点向所有离开节点发送消息。他们回答，并在向上移动时将答案合并。中间节点可以决定向下重新发送消息并等待新数据。新节点可以在叶子处动态地加入网络，并且也可以在合适的时刻离开网络。我们检查从根到叶子的每条路径上最多有一条活动消息。我们的实验结果总结在表1中。我们使用有限高度抽象和基于谓词的抽象进行了实验。我们既考虑了前向验证，也考虑了后向验证，即从初始状态集开始，检查坏状态是否无法到达，反之亦然。在表中，我们总是呈现这两种方法的更好结果。对于有限高度的抽象，我们考虑初始高度为1（如果需要，可以将其增加1-在表1所示的情况下，这是不必要的）。对于基于谓词的抽象，我们将描述坏状态集的自动机视为唯一的初始谓词（或者更准确地说，通过将其每个状态视为唯一接受的状态，可以从它获得的所有自动机;在表1所示的情况下，当使用这些初始谓词时，没有必要进行细化）。我们还对谓词的空初始集进行了实验-这被证明是Percolate协议的最快选项（在这种情况下需要一个细化）。表1ARTMC实验的一些结果议定书HnPP令牌传递向后：0.08s前向：0.06s双向令牌传递向后：1.0s前向：0.09s渗滤液向后：20.8s前向：2.4s树仲裁器向后：0.31s向后：0.34s领导人选举向后：2.0s向前：1.74秒广播向后：9.1s前向：1.0s请注意，基于谓词的抽象几乎总是比有限高度的抽象更好。这与结果不同的词格不同。对这一现象的解释是我们未来工作的一部分。表1中列出的验证时间是在英特尔A. Bouajjani等人/理论计算机科学电子笔记149（2006）3747Centrino 1.6GHz机器，768MB内存。我们认为这些结果非常令人鼓舞，我们现在正在开发一个基于Mona库的新版本工具。这给我们带来了更好的结果的希望，并期望该工具成功应用于现实生活中的案例研究（包括，例如，验证具有动态链接数据结构的程序5结论我们已经提出了抽象的定期树模型检查抽象定期模型检查的成功方法的概括。特别地，我们基于树自动机在某种意义上的等价状态的抽象，提出了两种树自动机的抽象。其中一个抽象决定哪些状态是等价的，通过比较它们的语言的树的有界高度，而第二个比较的状态wrt。它们的语言是否满足（即不与）具有规则树语言形式的谓词集合。这两种抽象都是自动refinable当一个虚假的反例被发现，并允许一个处理状态空间的过度近似精确到足以验证给定的感兴趣的属性。通过这种方式，代表可达集的自动机中的状态爆炸得到了解决。上面的抽象是受原始ARMC中使用的一些模式的我们已经在原型工具中实现了所提出的方法，并在多个验证示例中对其进行了评估，结果非常令人鼓舞。目前，我们正在基于Mona的树库构建一个新的更精细的工具版本[16]。该工具有望获得更好的结果，并具有成功应用于现实验证问题的高潜力。除了完成新版本的工具外，我们未来的工作包括研究ARTMC的各个应用领域。它们包括，例如，验证具有动态链接数据结构的程序。ARMC已经被证明对于验证带有单选择器链接的动态数据结构的程序是有用的[7]。使用ARTMC可以让我们处理更一般的结构。为了编码具有图形形状的数据结构，我们计划使用在节点中放置一些特殊符号的树来描述树上的其他边。另一个有前途的应用领域是XML操作.事实上，XML文档具有树结构，并且大多数XML解析器都基于树自动机理论--特别是对冲自动机[9]。此外，我们打算将我们的方法用于具有抽象数据结构和加密协议的程序，48A. Bouajjani等人/理论计算机科学电子笔记149（2006）37（注：18）。对于所有这些应用，我们计划研究树自动机和转换器中的编码以及定义应用相关抽象的可能性。引用[1] P.A.阿卜杜拉湾Jonsson，P. Mahata，and J. d'Orso.定期检查树模型。在CAV'02，LNCS 2404的程序施普林格，2002年。[2] P.A. Abdulla，A. Legay，J. d'Orso，and A.雷辛树型传感器的基于仿真的迭代。在TACAS'05的Proc.施普林格，2005年。[3] R.巴尔河Brayton，T. Henzinger，S. Qadeer，S.拉贾马尼符号状态空间探索中的偏序约简。在CAV'97的Proc.Springer，1997年。[4] B. Boigelot和P. Wolper。具有无限但规则状态空间的系统。在CAV'98的Proc.Springer，1998年。[5] A.布阿贾尼湾Jonsson，M. Nilsson和T.图伊里定期模型检查。在CAV'00，LNCS 1855的程序斯普林格，2000年。[6] A. Bouajjani和T.图伊里 外推树变换。 在CAV'02的程序2404.施普林格，2002年。[7] A. Bouajjani，P.Habermehl，P.Moro，T.沃伊纳尔具有动态1-n-链接结构的正则模型检测程序。在TACAS施普林格，2005年。[8] A. Bouajjani，P. Habermehl，and T.沃伊纳尔抽象规则模型检验，在Proc.CAVSpringer，2004.[9] A. Bruggemann-Klein，M. Murata和D.木材. 正规树和正规对冲语言在未排名的字母表：版本1。技术报告HKUST-TCSC-2001-0，香港科技大学，2001。[10] H.Comon，M.多谢河Gilleron，F.雅克马尔，D. Lugiez，S.Tison和M.托马西树自动机技术与应用，2005年，http://www.grappa.univ-lille3.fr/tata[11] J. 恩格尔弗里特自下而上和自上而下树变换的比较，数学系统理论，9：198[12] J·埃斯帕萨语法作为进程。形式和自然计算，LNCS2300，2002。[13] T. Genet. Timbuk，一个树自动机库，2005年。http://www.irisa.fr/lande/genet/timbuk[14] Y. Kesten，O. Maler，M. Marcus，A. Pnueli和E.沙哈尔使用丰富断言语言的符号模型检查。在97年CAV会议上Springer，1997年。[15] N. Klarlund和M.I.施瓦茨巴赫 图表类型。 在Proc. of POPL[16] N. Klarlund和A.莫勒MONA 1.4版用户手册。BRICS，丹麦奥胡斯大学计算机科学系，2001年。[17] M. 你别这样，小维。 Reh'ak，andJ. Str ejapancek. ExtedProces Rewr ite系统：Ex presives和可达性。在2004年的程序Springer，2004.[18] D.蒙尼奥用树自动机抽象密码协议。计算机程序设计科学，第47卷，第2-3期（2003年5月）。[19] A. Pnueli和E.沙哈尔加速参数化树网络的验证。技术报告MCS 02 -12，魏茨曼科学研究所，以色列，2004年。