基于正则语言的模型检查方法

理论计算机科学电子札记138（2005）21-36www.elsevier.com/locate/entcs基于正则语言Peter Habermehl彼得·哈伯梅尔1，2LIAFA，University Paris 7，Case 7014，2，place Jussieu，F-75251 Paris Cedex 05，FranceToma'svosVojnar3，4FIT，BrnoUniversityofTechnology，Bozetechova2，CZ-61266，Brno，CzechRepublic摘要常规模型检查是一种用于验证有限状态系统的方法，该方法基于将其配置编码为有限字母表上的单词，将配置集编码为有限自动机，并将转换编码为有限转换器。我们介绍了一种新的通用方法，定期模型检查的基础上推理的正规语言。该方法建立在这样的观察基础上，即对于其行为可以使用长度保持传感器建模的无限状态系统，有一个有限的计算来获得直到一定长度n的所有可达配置。这些配置是给定系统的可达配置的（正）样本，而长度为n的所有其他单词都是负样本。 然后，正则语言的推理方法可以 用于将样本推广到完整的可达性集（或其过度近似）。 我们已经实现了我们的方法在一个原型工具，这表明我们的方法是有竞争力的 一些具体的例子。此外，与所有其他现有的常规模型检查方法相比，对于具有可达配置的常规集合的所有系统，一般都保证终止。该方法同样适用于处理可达关系而不是可达集。保留字： 正则模型检验，正则语言1由法国安全部提供（ACIprojectSecur i t′eIn formatiquee）。2电子邮件：Peter. liafa.jussieu.fr3由捷克赠款机构支助（项目GA CR 102/04/0780和GA CR 102/03/D211）。4 电子邮件地址：vojnar@fit.vutbr.cz1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.01.04422P. Habermehl，T.Vojnar/Electronic Notes in Theoretical Computer Science 138（2005）211介绍常规模型检查[13，6]是一种很有前途的方法，用于无限状态系统的自动验证。常规模型检查的主要优点是其高度自动化，以及许多不同类型的系统-例如下推系统，（有损）FIFO通道系统，带计数器的系统，或参数化和动态进程网络-可以以统一的方式建模和验证。 常规的模型检查是基于这样的思想：将系统的配置编码为有限字母表上的单词，并将转换作为将配置映射到配置的有限状态转换器。然后，有限自动机可以自然地用于表示和管理（潜在地无限）配置集，并且可达性分析可以通过计算转换器的传递闭包[12，8，3，4]或通过转换器的迭代自动机的图像[6，18]来执行-取决于处理可达性关系或可达性集是否是首选。 然后可以通过将计算的可达性集合或可达性关系与描述系统的不期望状态或状态变化的集合或关系（再次由有限自动机或转换器编码）进行比较来检查被验证的系统的正确性。为了便于终止常规模型检查，这通常是不保证的，因为所解决的问题是不可判定的，已经提出了各种加速方法它们包括，例如，加宽[6，18]，通过组成trans-ducers [12，3]或自动机的抽象[5]，基于其创建历史的自动机状态的崩溃。这些方法允许定期模型检查在许多实际示例上终止，并且有时确保可以在给定框架中建模的系统的子类的完整性（例如，具有所谓的有界局部深度或简单过渡关系的系统[12]）。本文介绍了一种新的基于正则语言推理的正则模型检验的一般方法，它扩展了文[11]的工作（相关工作见下文）。该方法的动机是观察到，对于其行为可以使用长度保持传感器建模的无限状态系统，有一个有限的计算来获得所有可达的配置达到一定的长度。这些配置可以被认为是给定系统的可达配置的样本。然后，可以使用已经开发的用于正则语言推理的方法来泛化样本，目的是获得完整的可达集或它的过度近似，其精确到足以证明感兴趣的属性（如果它成立）。在这项工作中，我们专注于使用Trakhtenbrot-Barzdin算法[19]作为推理算法，但我们也简要地提到了我们尝试过的一些其他方法。P. Habermehl，T.Vojnar/Electronic Notes in Theoretical Computer Science 138（2005）2123实验表明，该方法具有良好的性能.同时，与所有其他现有的常规模型检查方法相比，对于可达配置集是常规的所有系统（包括，例如，有损信道系统和下推系统）。类似的结果，然后可以得到处理可达关系，而不是可达集太。从上面可以清楚地看出，我们主要关注可以使用长度保持换能器编码的系统。然而，即使对于验证非长度保持系统的安全特性，处理长度保持传感器也是足够的。在这种情况下，编码配置的字可以预先扩展有特殊的空白符号，以便每当插入新的有用符号时消耗。此外，委员会认为，如我们所示，我们的方法也可以扩展到处理非长度保持换能器。然而，我们的完备性结果并不成立（尽管在实践中，该方法仍然表现良好）。我们已经实现了该方法，并测试了一些例子的不同系统，包括参数网络的进程，下推系统，系统计数器，系统与有损队列，和一个系统的链表作为一个代表的系统与递归数据结构。实验表明，我们的方法是非常有效的，其结果大多与[5]的结果相当，[5 ]是该领域已知的最快的方法之一，但（与我们的方法不同）尚未知道完整性结果。相关工作。使用正则语言推理进行正则模型检查的想法已经在[11]中使用，然而，它主要只针对参数化环，并且计算循环是不同的，需要对所用系统的转换进行一定的手动分类。此外，[11]的作者还没有实现他们的方法。最近出现了[21]另一项基于正则语言推理的验证工作，专门用于验证具有FIFO通道的系统的安全属性纸的计划。 我们首先介绍自组织理论和常规模型检测领域的基本概念。然后，我们描述了用于正则语言推理的Trakhtenbrot-Barzdin算法，并提出了一种使用定期进行模型检查。最后，我们讨论了我们所做的实验（包括我们尝试作为Trakhtenbrot-Barzdin算法的替代方案的一些算法）并得出结论。24P. Habermehl，T.Vojnar/Electronic Notes in Theoretical Computer Science 138（2005）21є−→−→−−→i=0时2自动机、传感器和常规模型检测基础有限自动机是一个5元组M=（Q，，δ，q0，F），其中Q是一组有限状态，是一个有限字母表，δQ××Q是一组转换，q0∈Q是一个初始状态，FQ是一组最终状态。 M是确定性的，如果<$q∈Q，a∈<$q最多存在一个qJ，且（q，a，qJ）∈δ. M的转移关系→Q××Q被定义为满足以下条件的最小关系：（1）n∈Q：q−→q，（2）if（q，a，qJ）∈δ，thenq−→a qJ，and（3）ifq−→w qJ和qJ−→aqJJ，thenq−w→a qJJ. 从状态q∈Q到M的语言识别is定义dyL（M，q）={w|<$qJ∈F：q−→wqJ}。语言L（M）是等于L（M，q0）。如果一个集合L是正则的，则存在一个有限自动机使得L=L（M）。我们还定义了一种语言的词达到一定的长度：L≤n={w∈L||W| ≤n}，L≤n（M，q）={w∈L（M，q）||W| ≤n}，且n≤n={w∈n||W| ≤ n}。我们定义一个自动机M=（Q，Q，δ，q0，F）的深度，记为dM，它是从初始state，i到Me. dM=maxq∈Qminw∈q0−→wq|W|. 我们是一家人M的两个状态q，qJ∈Q是k-不可区分的，记为q<$kqJ，如果L≤k（M，q）=L≤k（M，q，J）.然后，我们定义了下式的可验证度ρM：M是最小k，使得M的任意两个状态q，qJ是k-可区分的，即，q/kqJ。设是一个有限的字母表，且={}。一个有限的传感器，是一个五元组τ=（Q，我 们 称有限换能器为保长换能器，如果δQ×××Q（即如果它的跃迁不包含）。 过渡关系→Q×××Q被定义为满足以下条件的最小关系：（1）q， q对每个q∈Q，（2）若（q，a，b，QJ）∈δ，则qa，bqJ，以及（3）如果qw，uqJ和甲乙丙−→q瓦山，则q−−→q. 然后，通过滥用符号，我们确定一个换能器，τ与关系{（w，u）|<$qJ∈F：q导线u qJ}。 我们称一个关系为正则关系0−−→如果它能被某些传感器识别的话。 对于一个集合L和一个关系R×，我们用R（L）表示集合{w ∈ |<$wJ∈L：（wJ，w）∈R}.设id为恒等关系，id为关系的合成。我们递归地定义关系式τ0= id，τ i+1= ττ i，τ= τ∞τ i。下面，我们假设idτ。这意味着对于所有i≥0，τi <$τi+1常规的模型检查可以用于处理复杂的安全性以及活性属性。然而，在本文中，我们集中于验证可达性。毕竟，更复杂的验证任务通常被简化为可达性验证（正如我们稍后在我们QJJJJJP. Habermehl，T.Vojnar/Electronic Notes in Theoretical Computer Science 138（2005）2125实验）。为了在常规的模型检查框架中验证可达性，有两种基本的方法.首先，给定一个系统，其转换关系被建模为转换器τ，初始配置的规则集合Init由有限自动机描述，并且“坏”配置的集合[001 pdf 1st-31 files]数字τ（Init）（或其过度近似），然后检查是否τ（Init）Bad=。问题2.1给定正则集Init和Bad以及有限变换器τ，τ（Init）Bad=hold？其次，我们可以尝试计算转换关系τ的自反和传递闭包τ。然后，我们可以使用τ来解决问题2.1。或者，我们也可以使用换能器τBad来描述不良性质。表示不希望能够从一种配置转换到另一种配置，并检查是否ττBad=τ（假设传感器保持长度不变）。问题2.2给定保长有限换能器τ和τBad，ττ坏=保持？上述两种方法各有优缺点。计算τ通常比仅计算τ（Init）更困难。 的确，有些情况下，τ（Init）是正则的，而τ不是。 另一方面，使用τe可以允许检查否则将更难或不可能检查的属性（例如，检查输入输出对应关系，诸如链表、队列等的各种无界结构的特定元素）。26P. Habermehl，T.Vojnar/Electronic Notes in Theoretical Computer Science 138（2005）21N，N，N，NNN n不不不(a) InitN、TT、NT，T(b) 坏N，N，N，N在叱(c) τN，N，N，NN、T(d) τBad(e) τ∗NN(f) τ（Init）图1.一、用于简单令牌传递的常规模型检查的自动机和转换器为了说明所描述的概念和稍后我们的方法，我们在图1中给出了出现在简单令牌传递协议的常规模型检查中的基本自动机和转换器。该协议假定沿着节点的参数数量的序列从左到右传递单个令牌-图1（c）中示出了包括身份关系的转移关系。最初，令牌位于最左边的节点：图1（a）。图1（b）中的坏自动机说，永远不应该少于或多于一个令牌。图1（d）中的转换器τBad表示令牌永远不应该向左传递。 可达性关系和可达性集合然后分别在图1（e）和1（f）在提出我们基于正则语言推理的新正则模型检查方法之前，主要针对处理长度保持转换器，我们注意到处理此类转换器对于非长度保持系统的安全性验证没有限制（另见[12]）。这是因为对于有限次运行，我们总是可以替换添加和重新-通过重写预先添加到初始配置中的特殊空白符号来移动符号。更准确地说，我们可以在τ的每个状态（如果使用τ Bad，也可以在τ Bad的每个状态）上添加标记为，的自循环，用，a转换替换每个，a，转换，用a，one替换每个a，转换，并在Init和Bad的自动机的每个状态上添加标记为的自循环。T、NN、TN、TT，T在叱T，TT、N、T，在叱T，T不P. Habermehl，T.Vojnar/Electronic Notes in Theoretical Computer Science 138（2005）21273正则语言的完备训练集推理正则语言的推理是一个非常活跃的研究领域（参见。[19、16、14、9]）。基本上，问题是从某些单词（或已知不属于该语言的单词）推断出一种语言所提出的算法中使用的一个重要概念是训练集（或样本）。训练集T=（T+，T−）是一对两个不相交的集合T+，T−，其中T+包含正例（要推断的语言中的单词），T−包含负例。一个训练集T=（T+，T−）称为n-完备的，如果T+<$T−=<$≤n。对于从训练集进行正则语言推理，本 文 研 究 了 其 中 ， 在 这 项 工 作 中 ， 我 们 主 要 集 中 在 使 用 所 谓 的Trakhtenbrot-Barzdin算法（简称TB算法）[19]，该算法适用于n-完全训练集，正如我们下面所示，可以在常规模型检查的情况对于长度保持换能器，模型检查问题2.1可以被看作是语言推理问题，其方式如下：我们想要计算（或至少近似）针对某个给定长度保持换能器τ和正则集合Init的集合τ（Init）。 由于τ是长度保持的，所以集合τ（Init≤n）对于每个n都是有限的，并且可以通过有限次迭代来计算。”（注：《说文解字》）。此外，每个长度小于或等于n的字不在τ（Init≤n）中，也不能在τ（Init）中。因此，集合τ（Init≤n）和τ≤n\τ（Init≤n）可以看作是我们想要推断的语言τ（Init）的正例和反例的更准确地说它们包含了给定单词的所有语言达到一定长度，从而形成n-完全训练集。随着n的增加，我们得到了越来越多的语言τ（Init）的正面和负面例子--训练集正在增长。因此，如果τ（Init）是正则的，我们最终（当然我们不知道什么时候）将获得一个足够大的训练集T [19]，并且TB算法将允许我们推断从T. 如果τ（Init）不是正则的，仍然可能得到足以证明利息性质的过度近似。同样的方法也可以用来尝试通过考虑字母的字母对并计算限于长度小于或等于n的单词的τ来推断长度保持换能器的关系τ。3.1Trakhtenbrot-Barzdin算法为了详细描述TB算法及其在常规模型检查中的使用，我们需要更多的定义。DFA A被称为与训练集tT=（T+， T−）ifT+<$L（A）anddL（A）<$T −=<$T一致。A训练setT=28P. Habermehl，T.Vojnar/Electronic Notes in Theoretical Computer Science 138（2005）21（T+，T-）是n-完全wrt。a DFA A，如果T+= L≤n（A）。给定一个n-完备训练集T=（T+，T-），我们称一个确定性有限自动机AT=（Q，Q，δ，q0，F）为T的预树自动机，如果L（A）=T+，AT具有以下形式一棵树，不包含任何节点与空语言（提供T+/=T）。我们现在描述Trakhtenbrot-Barzdin算法的一个稍微修改的版本，它计算一个推断的DFA（也称为目标自动机），具有与给定的n-完全训练集一致的最小数量的状态设T=（T+，T-）是一个n-完备训练集，AT是确定性训练集T.显然，A T的状态必须对应于对象AT的状态，因为我们都被AT所接受。然而，A T的几个不同状态可以对应于AT的同一状态。因此，如果这不会导致长度短于或等于n的字被接受，则A_T的最佳想法是使A_T的两个状态尽管AT不接受它。AT中的两个状态q和qJ可以安全地塌陷，如果它们是相容的，即如果它们是k-不可区分的（q<$kqJ），其中k是从q和qJ开始的子树的长度的最小值。设succ是一个函数，它将AT中的每个状态与一个广度优先排序的继承者联系起来。该算法通过识别兼容状态来修改AT算法1输入：AT，初始状态为q0q1：=q0;而在A-Tdo中存在q1的后继者public intfindDuplicate（intfindDuplicate）;q2：=q0;当q1/=q2且不相容（q1，q2）时，q2：=succ（q2）;od如果q1/=q2且相容（q1，q2），则让从father（q1）到q1的过渡指向q2，从AT中删除q1及其所有子项;od输出：修改后的自动机AT请注意，原始算法[19]使用完整的输入树（每个内部节点都有一个对应于每个字母的子节点）。在我们的设置中，这是不必要的，因为我们只考虑语言，而不是自动机的输出行为。该算法的复杂度为O（mn2），其中m是AT的大小，n是目标自动机的大小.在图2和图3中，我们给出P. Habermehl，T.Vojnar/Electronic Notes in Theoretical Computer Science 138（2005）2129*N不*不NNN不*不N*NN不不NN图二. 2-完备训练集与TB算法TB算法的不同阶段在2-完全训练集上运行，τ（Init）和我们运行示例的τ的3-完备集。每个阶段的两个崩溃的兼容状态标记为“0”。注意，在第一种情况下，τ（Init）完全是算法的结果，而在另 一种情况下，结果是τ的过度近似。我们有以下定理[19]。定理 3.1 设T是一个 n-完备训 练集。 算法 1用最小数量的与T一 致的stateconsence t来计算D F A T。注意，可能有几个不同的DFA，它们具有与T一致的最小数量的状态-TB算法的输出只是其中之一如果训练集的所有单词都来自某个最小确定性自动机A，那么如果n相对于自动机的结构足够大，则TB算法保证从n-完全训练集自动机A的可重构度r定义为r=d+ρ+1，其中d是深度，ρ是可重构度。然后我们有下面的定理[19]。定理3.2给定一个可重构度为r的极小DFA A和一个训练集Tr-完备wrt。A，算法1计算A（直到同构）。如果A有n个状态，那么在最坏的情况下，d=ρ=n− 1，r= 2n −1。1. 因此，完整的训练集必须包含指数（以n为单位）很多话。幸运的是，平均而言[19，14]，r要小得多，因为可以证明d的平均值是Clog| Σ|（n）其中C是取决于ρ的常数，ρ = log| Σ|log2（n）。这意味着平均而言，与自动机的大小相比，可重构程度r较小，并且仅需要小的完整训练集（n中的多项式）来重建它。30P. Habermehl，T.Vojnar/Electronic Notes in Theoretical Computer Science 138（2005）21在叱*在叱T，TT、N在叱在叱T，TT，TT、NN，NN，TN，NN，NT，TN，T在T，TN，T在叱在叱T，TN，NT，*在叱*在叱T，TT、N在叱在叱T，TT、N在叱N，NN，T在叱T，T*N，NT，TN，T在T，TN，T在叱在叱T，TN，NT，在叱*在叱T，TT、N在叱在叱在在叱T，TT，TT、NN，NN，TN，N*N，NT，TN，TN，NT，TN，TN，N，N，NT，TN，NT，在叱在叱T，TT、N在叱在叱在在叱T，TT、NN，NN，TT，T在叱T，TN，NT，TN，T在T，TN，TN，N，N，NT，TN，NT，*在叱T，TT、N*在叱T，TT、NN，NN，T在叱T，TN，NT，TN，TN，NT，TN，TN，N，N，NT，TN，NT，在叱在叱T，TT、N*在叱T，TT、NN，NN，T在叱T，TN，NT，TN，T*N，NT，TN，TN，N，N，NT，TN，NT，图三. 一个3-完备训练集和TB算法4模型检测算法在这一节中，我们描述了我们的模型检测算法的基础上推理的正规语言。我们从算法的基本版本开始，然后对该算法进行一些修改和扩展4.1基本模型检测算法我们的算法的思想是计算越来越大的来自语言τ（Init）的完整训练集，从它们推断自动机，并测试这个推断的自动机是否是不变的充足率以证明财产 作为推理算法，原则上可以使用基于文献中提出的正例和反例的任何 推 理 算 法 （ 例 如 ， RPNI [16 ， 14] ） 。在 本 文 中 ， 我 们 使 用Trakhtenbrot-Barzdin al-P. Habermehl，T.Vojnar/Electronic Notes in Theoretical Computer Science 138（2005）2131上面讨论了出租，因为它与完整的训练集一起工作，并且如果给定足够大的训练集，则保证输出原始自动机。然而，下面我们以一般的方式描述我们的模型检查算法。算法2输入：长度保持换能器τ，初始配置的规则集合Init和一组常规的坏配置Bad i：= 1;/*i也可以不同地初始化。**/重复C：=τ（Init≤i）;C：= i≤i\C;如果Bad=C/=B，则输出：违反属性A：=inference（C，C）; i：=i+1;直到τ（L（A））<$L（A）和Init<$L（A）和L（A）<$Bad=<$;输出：属性满足当我们在算法2中使用被描述为算法1的TB算法版本进行推理时，对inference（C，C）的调用调用了算法1，并将C的前缀树自动机作为输入。因此，C的计算是不必要的。在我们的运行示例中，为了验证概率τ（Init）Bad=，算法在i = 2时停止（推断出的不变量正好是τ（Init）），并且对于概率τB ad=，算法在i=3时最佳，并且具有τ的更新（见图12）。3）。注意，要计算τ（Init≤i），可以重用τ（Init≤i−1），只计算大小为i的可达配置。 算法尝试更大，更大的训练集，直到它终止，因为它要么找到了感兴趣的属性的反例，要么找到了包含初始状态且不与Bad集相交的不变量。测试初始化（A）是必要的，因为对于小型i，则生成的示例可能无法重建Init。一个替代方法是设置iwrt的初始值。Init，但根据我们的经验，这并不总是最好的选择。如果τ（Init）是正则的，算法总是终止。定理4.1设τ是一个保长变换，且是Init和Bad两个正则集。 如果τ（Init）是正则的，那么算法2和算法1用作推理算法总是终止。32P. Habermehl，T.Vojnar/Electronic Notes in Theoretical Computer Science 138（2005）21我的律师。如果τ（Init）Bad，则存在saw或dw∈τ（Init）Bad有一定的大小由于τ是保长的，所以w∈τ（Init≤n），算法在n次迭代后终止. 由于定理3.2，该算法在至多r（阶）之后停止。τ（Init））步骤的可重构性Q请注意，在属性已验证的情况下终止算法意味着推断出了一个精确到足以证明该属性的不变量总的来说我们不能检查我们是否已经推断出精确的可达性集合τn（Init）。这很清楚，例如，对于有损信道系统，已知τ（Init）是正则的[7，2]，但不可计算[1，15]。根据定理4.1，我们轻松获得以下内容。推论4.2模型检验问题2.1是可判定的，如果τ（Init）是正则的。上述情况并不令人惊讶，因为我们可以为这个问题给出两个半决策过程：一个寻找越来越大的反例，另一个枚举所有正则语言并检查不变量（如[17]中对FIFO通道系统的解释）。我们的算法提供了一个聪明的方法来枚举正则语言的候选不变。最后，不用详细讨论，很明显，我们也可以用与上述非常相似的方式来推论4.3模型检验问题2.2是可判定的，如果τ正则。4.2基本算法的几点改进和推广算法2也可以很容易地修改为处理非长度保持变换器τ：当我们计算定点τ（Init）时，我们总是在每一步之后与可达配置相交，其中τ≤n。这样，定点计算将始终终止。然而，训练集并不保证变得完整因此，模型检查算法的终止通常不被保证，即使对于常规τ（Init）也是如此。然而，根据我们的实践经验，该方法仍然表现出良好的各种具体的例子。此外，算法2所基于的算法1不是在前缀树自动机上运行，而是可以直接在最小确定性自动机上运行，这在实践中通常是计算C：=τ（Init≤i）的结果。因为它不包含任何循环，所以这种最小确定性自动机具有DAG的形式。处理一个通过记住树的深度i和到达树的步骤数，P. Habermehl，T.Vojnar/Electronic Notes in Theoretical Computer Science 138（2005）2133节点Q1.这两个值的差异可以用来推断应该考虑接受q1和q2的 这一步是必要的，因为前缀树自动机的几个不同深度的状态（对应于不同的传入路径）可以合并为单个DAG状态，并且要考虑的长度不能仅从状态本身推导出来。5实验我们已经使用FSA库[20]在YAP Prolog中编写的原型工具中实现了本文中提出的想法。5作为常规模型检查广泛适用，我们将该工具应用于下文所述的各种不同的验证任务。此外，我们还用几种受启发的方法替换了模型检查方案中的TB推断算法，[5]我们将在本节末尾简要报告5.1使用TB算法这些实验与[5]中更详细介绍的实验相似。它们包括参数系统的验证（以位 理想 化的 参 数Bakery ， Burns ， Dijkstra 和 Szymanski 互 斥算 法的 形式），一个简单的下推系统，用几个相互递归的过程来模拟程序（来自[10]的递归控制示例），交替位协议作为具有（有损）队列的系统的代表，一个Petri网，用动态出现和消失的过程来模拟读写器问题，可以被认为是具有无界计数器的系统的一个例子（其值以一元并行编码），以及一个用于反转线性列表的过程，作为具有无界递归数据结构的系统的代表。简化的Bakery互斥算法以几种方式进行建模：使用参数数量的进程和由表示配置的单词中的适当进程的位置编码的票证值，以及使用有限数量的进程（3到5个），其中票证由显式计数器建模，其值以二进制（如NDD）或一元并行编码。我们主要考虑了可以直接使用可达性验证来处理的不变性属性的验证。然而，我们也尝试处理一些更复杂的性质。在下推示例中，我们检查了对过程调用顺序的一些约束，这是一个处理更复杂的安全属性的示例-转换5Prolog被选为一个快速，但仍然相对有效的原型开发环境。34P. Habermehl，T.Vojnar/Electronic Notes in Theoretical Computer Science 138（2005）21对于可达性问题，我们用系统的模型手工构造相应的安全自动机。我们还在面包店的例子中验证了社区的活跃性。在这种情况下，我们已经手动组合了适当的Buchi自动机，其中系统被验证。 我们已经大多认为是正确的系统，但我们也运行的工具，在一个错误的版本的考虑系统之一，即读者/作家的例子，我们省略了一个Petri网弧。我们主要是在处理可达性集的层面上工作，但在反向列表的例子中，我们也处理了由转换器表示的可达性关系（使用可达性集计算，我们检查了过程输出列表，但使用可达性关系限制到从初始状态，即idInit初始状态，我们检查输出列表是输入列表的反转。） 最后，在实验中，我们尝试和反向验证-即从初始状态或“坏”状态开始。实验结果总结于表1中。对于每一个实验，我们都给出了最佳结果.我们说它是否在向前或向后验证范围内，以及样本中单词的初始长度是多少 （ con sid edvalu eswere ： 1 ， |QBad| ， 2|QBad| 、 |QBad|/2 ， |QInit| ，2|QInit|、和|QInit|/2）。当我们将这些结果与[5]的方法进行比较时（其中在这个领域中，我们看到他们通常会慢一点，可比性在一种情况下（ABP示例），推理方法甚至比[5]中的方法更快。这样的结果是非常积极的考虑到没有终止的保证是已知的方法[5]。最后，在表1的rg列中，我们给出了生成有限样本所花费的时间百分比，这表明我们的方法的这一部分的处理在未来的优化中值得特别关注5.2使用TB算法以外的其他推理方法在一系列额外的实验中，我们用[5]启发的几种算法代替了模型检查模式中TB算法的使用特别地，我们试图通过折叠这些自动机的任何状态来概括由有限自动机表示的所获得的样本，这些自动或者，把所有的状态都看作是最终的）。虽然这些算法的使用结果大多比TB算法的使用慢，但也有一些情况（例如，面包房公共活动或伯恩斯实验），他们的速度快了三倍受此启发，未来，我们计划基于模型检查模式的通用性进行更多的实验，该模式允许我们插入各种P. Habermehl，T.Vojnar/Electronic Notes in Theoretical Computer Science 138（2005）2135表1基于正则语言实验最佳设置T[sec]rg[%]面包店Bw，|QBad|0.0350面包房通讯丽芙Fw，2 |Q初始化|0.3690面包柜3P体重，2|QBad|8.6970面包柜4PFw，|QBad|14392面包店5P一元Fw，2 |Q初始化|22945ABP体重，2|QBad|0.0350烧伤Fw，2 |Q初始化|0.7798DijkstraFw，|QBad|/2个1.1692PDSBw，|QBad|0.0463Petri网/Read. Wr.Fw，|QBad|/2个32390Favorite PN/Rd. Wr.Fw，2 |Q初始化|1.4854SzymanskiFw，|QBad|0.7694Rev. 列出Fw，|Q初始化|1.6490Rev. 列表/Transd.Fw，|Q初始化|/2个40.569推理算法6结论本文介绍了一种基于正则语言推理的正则模型检测方法。 该方法迭代地计算更多，从代表所有可达配置的越来越大的样本中推断出的τ（Init）或τ的配置），其长度达到递增地增加的特定界限。当达到坏的配置或当推断出τ（Init）或τ的安全过近似时对于长度保持的换能器，该方法对所有具有规则τ（Init）或τ的系统都是完备的. 这是与其他方法相比的一大优势。在同时，实验结果也表明了该方法的有效性。我们的模型检测算法是通用的，因为每一个推理算法的工作与积极和消极的例子可以使用。在未来，我们计划尝试其他推理算法[16，14]，并在我们的框架中比较它们的性能。 对RPNI 2[9]这可能会很有趣。当提供新的正面及负面例子时，该等假设乃基于对推断假设的细化。它们可以很容易地在我们的框架中使用，因为我们计36P. Habermehl，T.Vojnar/Electronic Notes in Theoretical Computer Science 138（2005）21算越来越长的配置。进一步的优化可以是使用专用的有限状态模型检查器来计算有限长度的可达配置集P. Habermehl，T.Vojnar/Electronic Notes in Theoretical Computer Science 138（2005）2137很明显。引用[1] Abdulla，P.，L. Boasson和A. Bouajjani，E. Lossy Queue Languages，in：Proceedings ofICALP[2] Abdulla，P.，A. Bouajjani和B.杨文生，无限制、有损耗的先进先出通道系统的动态分析，载于：CAV'98会议录[3] Abdulla，P.，J. d'Orso，B. Jonsson和M. Nilsson，定期模型检查的算法改进，在：CAV'03会议记录[4] Boigelot，B.，A. Legay和P.Wolper，大型迭代换能器，在：Proceedings CAV[5] Bouajjani，A.，P. Habermehl和T.Vojnar，Abstract Regular Model Checking，in：Proceedings of CAV[6] Bouajjani，A.，B. Jonsson，M.Nilsson和T.陈文辉，模型检验，载于：中国科学技术出版社，2000年[7] 好吧好吧G 、杨A. Fi n kelandS. P. I yer，Unreli ableChannelsareEasiertoVerifythanPerfectChannels，Information and Computation 124（1996），pp. 20比31[8] Dams，D.，Y. Lakhnech和M.Ste Escheren，迭代传感器，在：Proceedings CAV2102（2001）。[9] Dupont，P.，增量规则推理，在：语法推理：从句子中学习语法，LNAI1147，1996，pp.222-237.[10] Esparza，J.，D. Hansel，P. Rossmanith和S.徐文，模型检验下推系统的有效算法，见：《CAV'00学报》[11] 弗里堡湖和H.奥尔森，可达集参数化环作为正规语言，在：INFINITY workshop，Electronic Notes in Theoretical Computer Science9（1997）。[12] 琼森湾和M. Nilsson，Transitive Closures of Regular Relations for Nonlinear Finite StateSystems，in：Proceedings of TACAS[13] Kesten，Y.，O. Maler，M. Marcus，A. Pnueli和E. Shahar，Symbolic Model Checking withRich Assertional Languages，Theoretical Computer Science256（2001）.[14] Lang，K. J.，随机DFAProceedings of the 5th ACM Workshop on Computational Learning Theory（1992），pp.45比52[15] 迈尔河，巴西-地Undecidable Problems in Unreliable Computations，in：Latin AmericanTheoretical Informatics，2000，pp. 377-386.[16] Oncina，J.和P. Garcia，在多项式更新时间内推断正则语言，模式识别和图像分析，1992年，第100页。49比61[17] Pachl，J.，Protocol Description and Analysis Based on a State Transition Model with ChannelExpressions，1987，Protocol Verification，Specification，and Testing VII[18] Touili，T.，定期模型检查的扩展技术，理论计算机科学电子笔记50（2001）。[19] 特拉赫滕布罗特湾A.和Y. A.张文生，有限自动机：行为与综合，北京：机械工业出版社，1999.[20] van Noord，G.， FSA 6.2 （2004），URL：http://odur.let.rug.nl/~vannoord/Fsa/。[21] Vardhan，A.，K. Sen，M. Viswanathan和G. Agha，学习验证安全属性，在：ICFEM'04会议记录